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

Require Import List Arith Omega.

Require Import utils pos vec.
Require Import subcode sss compiler_correction.
Require Import list_bool.
Require Import bsm_defs.
Require Import mm_defs mm_utils.

Set Implicit Arguments.

(** ** BSM recues to MM *)

Tactic Notation "rew" "length" := autorewrite with length_db.

Local Notation "e #> x" := (vec_pos e x).
Local Notation "e [ v / x ]" := (vec_change e x v).

Local Notation "I '/BSM/' s -1> t" := (bsm_sss I s t) (at level 70, no associativity).
Local Notation "P '/BSM/' s -+> t" := (sss_progress (@bsm_sss _) P s t) (at level 70, no associativity).
Local Notation "P '/BSM/' s ->> t" := (sss_compute (@bsm_sss _) P s t) (at level 70, no associativity).
Local Notation "P '/BSM/' s ~~> t" := (sss_output (@bsm_sss _) P s t) (at level 70, no associativity).
Local Notation "P '/BSM/' s ↓" := (sss_terminates (@bsm_sss _) P s)(at level 70, no associativity).

Local Notation "P '/MM/' s -+> t" := (sss_progress (@mm_sss _) P s t) (at level 70, no associativity).
Local Notation "P '/MM/' s ->> t" := (sss_compute (@mm_sss _) P s t) (at level 70, no associativity).
Local Notation "P '/MM/' s '~~>' t" := (sss_output (@mm_sss _) P s t) (at level 70, no associativity).
Local Notation "P '/MM/' s ↓" := (sss_terminates (@mm_sss _) P s)(at level 70, no associativity).

Section simulator.

  Ltac dest x y := destruct (pos_eq_dec x y) as [ | ]; [ subst x | ]; rew vec.

  Variables (m : nat).
  
  (** each stack of the BSM corresponds to a (unique) register in the MM 
      and there are extra registers: tmp1, tmp2 which must have value 0 at start 
      they might change value during a simulated BSM instruction but when
      the instruction is finished, their values are back to 0 

      This is expressed in the below bsm_state_enc invariant
  *)
  
  Let n := 2+m.
  Let tmp1 : pos n := pos0.
  Let tmp2 : pos n := pos1.
  Let reg p: pos n := pos_nxt (pos_nxt p).
   
  Let Hv12 : tmp1 <> tmp2.             Proof. discriminate. Qed.
(* Goal: forall p : pos m, not (@eq (pos n) (reg p) tmp2) *)
  Let Hvr1 : forall p, reg p <> tmp1.  Proof. discriminate. Qed.
(* Goal: forall p : pos m, not (@eq (pos n) (reg p) tmp2) *)
  Let Hvr2 : forall p, reg p <> tmp2.  Proof. discriminate. Qed.
  
  Let Hreg : forall p q, reg p = reg q -> p = q.
  Proof. intros; do 2 apply pos_nxt_inj; apply H. Qed. 

  Definition bsm_state_enc (v : vec (list bool) m) w := 
            w#>tmp1 = 0
         /\ w#>tmp2 = 0
         /\ forall p, w#>(reg p) = stack_enc (v#>p).

  (* i is the position in the source code *)

  Definition bsm_instr_compile lnk i ii :=
    match ii with
      | PUSH s Zero => mm_push_Zero (reg s) tmp1 tmp2 (lnk i)
      | PUSH s One  => mm_push_One  (reg s) tmp1 tmp2 (lnk i)
      | POP  s j k  => mm_pop (reg s) tmp1 tmp2 (lnk i) (lnk j) (lnk (1+i)) (lnk k)
    end.

  Definition bsm_instr_compile_length (ii : bsm_instr m) :=
    match ii with 
      | PUSH _ Zero => 7
      | PUSH _ One  => 8
      | POP  _ _ _  => 16
    end.

  Fact bsm_instr_compile_length_eq lnk i ii : length (bsm_instr_compile lnk i ii) = bsm_instr_compile_length ii.
  Proof. destruct ii as [ | ? [] ]; simpl; auto. Qed.
    
  Fact bsm_instr_compile_length_geq ii : 1 <= bsm_instr_compile_length ii.
  Proof. destruct ii as [ | ? [] ]; simpl; auto; omega. Qed.

  Hint Resolve bsm_instr_compile_length_eq bsm_instr_compile_length_geq.

  (* This main soundness lemma per simulated instruction *)

  Lemma bsm_instr_compile_sound : instruction_compiler_sound bsm_instr_compile (@bsm_sss _) (@mm_sss _) bsm_state_enc.
  Proof.
(* Goal: @instruction_compiler_sound (bsm_instr m) (mm_instr n) bsm_instr_compile (vec (list bool) m) (vec nat n) (@bsm_sss m) (@mm_sss n) bsm_state_enc *)
    intros lnk I i1 v1 i2 v2 w1 H; revert H w1.
(* Goal: forall (_ : @bsm_sss m I (@pair nat (vec (list bool) m) i1 v1) (@pair nat (vec (list bool) m) i2 v2)) (w1 : vec nat n) (_ : @eq nat (lnk (Init.Nat.add (S O) i1)) (Init.Nat.add (@length (mm_instr n) (bsm_instr_compile lnk i1 I)) (lnk i1))) (_ : bsm_state_enc v1 w1), @ex (vec nat n) (fun w2 : vec nat n => and (@sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (lnk i1) (bsm_instr_compile lnk i1 I)) (@pair nat (vec nat n) (lnk i1) w1) (@pair nat (vec nat n) (lnk i2) w2)) (bsm_state_enc v2 w2)) *)
    change v1 with (snd (i1,v1)) at 2.
(* Goal: forall (_ : @bsm_sss m I (@pair nat (vec (list bool) m) i1 v1) (@pair nat (vec (list bool) m) i2 v2)) (w1 : vec nat n) (_ : @eq nat (lnk (Init.Nat.add (S O) i1)) (Init.Nat.add (@length (mm_instr n) (bsm_instr_compile lnk i1 I)) (lnk i1))) (_ : bsm_state_enc (@snd nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1)) w1), @ex (vec nat n) (fun w2 : vec nat n => and (@sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (lnk i1) (bsm_instr_compile lnk i1 I)) (@pair nat (vec nat n) (lnk i1) w1) (@pair nat (vec nat n) (lnk i2) w2)) (bsm_state_enc v2 w2)) *)
    change i1 with (fst (i1,v1)) at 2 3 4 6 7 8.
(* Goal: forall (_ : @bsm_sss m I (@pair nat (vec (list bool) m) i1 v1) (@pair nat (vec (list bool) m) i2 v2)) (w1 : vec nat n) (_ : @eq nat (lnk (Init.Nat.add (S O) (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1)))) (Init.Nat.add (@length (mm_instr n) (bsm_instr_compile lnk (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1)) I)) (lnk (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1))))) (_ : bsm_state_enc (@snd nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1)) w1), @ex (vec nat n) (fun w2 : vec nat n => and (@sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (lnk (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1))) (bsm_instr_compile lnk (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1)) I)) (@pair nat (vec nat n) (lnk (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1))) w1) (@pair nat (vec nat n) (lnk i2) w2)) (bsm_state_enc v2 w2)) *)
    change v2 with (snd (i2,v2)) at 2.
(* Goal: forall (_ : @bsm_sss m I (@pair nat (vec (list bool) m) i1 v1) (@pair nat (vec (list bool) m) i2 v2)) (w1 : vec nat n) (_ : @eq nat (lnk (Init.Nat.add (S O) (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1)))) (Init.Nat.add (@length (mm_instr n) (bsm_instr_compile lnk (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1)) I)) (lnk (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1))))) (_ : bsm_state_enc (@snd nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1)) w1), @ex (vec nat n) (fun w2 : vec nat n => and (@sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (lnk (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1))) (bsm_instr_compile lnk (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1)) I)) (@pair nat (vec nat n) (lnk (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1))) w1) (@pair nat (vec nat n) (lnk i2) w2)) (bsm_state_enc (@snd nat (vec (list bool) m) (@pair nat (vec (list bool) m) i2 v2)) w2)) *)
    change i2 with (fst (i2,v2)) at 2.
(* Goal: forall (_ : @bsm_sss m I (@pair nat (vec (list bool) m) i1 v1) (@pair nat (vec (list bool) m) i2 v2)) (w1 : vec nat n) (_ : @eq nat (lnk (Init.Nat.add (S O) (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1)))) (Init.Nat.add (@length (mm_instr n) (bsm_instr_compile lnk (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1)) I)) (lnk (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1))))) (_ : bsm_state_enc (@snd nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1)) w1), @ex (vec nat n) (fun w2 : vec nat n => and (@sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (lnk (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1))) (bsm_instr_compile lnk (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1)) I)) (@pair nat (vec nat n) (lnk (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i1 v1))) w1) (@pair nat (vec nat n) (lnk (@fst nat (vec (list bool) m) (@pair nat (vec (list bool) m) i2 v2))) w2)) (bsm_state_enc (@snd nat (vec (list bool) m) (@pair nat (vec (list bool) m) i2 v2)) w2)) *)
    generalize (i1,v1) (i2,v2); clear i1 v1 i2 v2.
    induction 1 as    [ i p j k v Hv
                      | i p j k v ll Hll 
                      | i p j k v ll Hll
                      | i p [] v
                      ]; simpl; intros w1 H0 H; generalize H; intros (H1 & H2 & H3).

    + exists w1; split; auto.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (lnk i) (@mm_pop n (reg p) tmp1 tmp2 (lnk i) (lnk j) (lnk (S i)) (lnk k))) (@pair nat (vec nat n) (lnk i) w1) (@pair nat (vec nat n) (lnk k) w1) *)
      apply mm_pop_void_progress; auto.
(* Goal: @eq nat (@vec_pos nat n w1 (reg p)) (stack_enc (@nil bool)) *)
      rewrite H3, Hv; auto.

    + exists (w1[(stack_enc ll)/reg p]); repeat split; auto; rew vec.
      * apply mm_pop_Zero_progress; auto.
(* Goal: @eq nat (@vec_pos nat n w1 (reg p)) (stack_enc (@cons bool true ll)) *)
        rewrite H3, Hll; auto.
      * intros q; dest p q.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n w1 (reg p) (stack_enc (@cons bool false (@vec_pos (list bool) m v p)))) (reg q)) (stack_enc (@vec_pos (list bool) m v q)) *)
        assert (reg p <> reg q); rew vec.
    
    + exists (w1[(stack_enc ll)/reg p]); repeat split; auto; rew vec.
      * apply mm_pop_One_progress; auto.
(* Goal: @eq nat (@vec_pos nat n w1 (reg p)) (stack_enc (@cons bool true ll)) *)
        rewrite H3, Hll; auto.
      * intros q; dest p q.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n w1 (reg p) (stack_enc (@cons bool false (@vec_pos (list bool) m v p)))) (reg q)) (stack_enc (@vec_pos (list bool) m v q)) *)
        assert (reg p <> reg q); rew vec.
   
    + exists (w1[(stack_enc (One::v#>p))/reg p]); repeat split; auto; rew vec.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (lnk i) (@mm_push_One n (reg p) tmp1 tmp2 (lnk i))) (@pair nat (vec nat n) (lnk i) w1) (@pair nat (vec nat n) (lnk (S i)) (@vec_change nat n w1 (reg p) (stack_enc (@cons bool true (@vec_pos (list bool) m v p))))) *)
(* Goal: forall p0 : pos m, @eq nat (@vec_pos nat n (@vec_change nat n w1 (reg p) (stack_enc (@cons bool true (@vec_pos (list bool) m v p)))) (reg p0)) (stack_enc (@vec_pos (list bool) m (@vec_change (list bool) m v p (@cons bool true (@vec_pos (list bool) m v p))) p0)) *)
      rewrite H0; apply mm_push_One_progress; auto.
(* Goal: forall p0 : pos m, @eq nat (@vec_pos nat n (@vec_change nat n w1 (reg p) (stack_enc (@cons bool false (@vec_pos (list bool) m v p)))) (reg p0)) (stack_enc (@vec_pos (list bool) m (@vec_change (list bool) m v p (@cons bool false (@vec_pos (list bool) m v p))) p0)) *)
      intros q; dest p q.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n w1 (reg p) (stack_enc (@cons bool false (@vec_pos (list bool) m v p)))) (reg q)) (stack_enc (@vec_pos (list bool) m v q)) *)
      assert (reg p <> reg q); rew vec.

    + exists (w1[(stack_enc (Zero::v#>p))/reg p]); repeat split; auto; rew vec.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (lnk i) (@mm_push_Zero n (reg p) tmp1 tmp2 (lnk i))) (@pair nat (vec nat n) (lnk i) w1) (@pair nat (vec nat n) (lnk (S i)) (@vec_change nat n w1 (reg p) (stack_enc (@cons bool false (@vec_pos (list bool) m v p))))) *)
(* Goal: forall p0 : pos m, @eq nat (@vec_pos nat n (@vec_change nat n w1 (reg p) (stack_enc (@cons bool false (@vec_pos (list bool) m v p)))) (reg p0)) (stack_enc (@vec_pos (list bool) m (@vec_change (list bool) m v p (@cons bool false (@vec_pos (list bool) m v p))) p0)) *)
      rewrite H0; apply mm_push_Zero_progress; auto.
(* Goal: forall p0 : pos m, @eq nat (@vec_pos nat n (@vec_change nat n w1 (reg p) (stack_enc (@cons bool false (@vec_pos (list bool) m v p)))) (reg p0)) (stack_enc (@vec_pos (list bool) m (@vec_change (list bool) m v p (@cons bool false (@vec_pos (list bool) m v p))) p0)) *)
      intros q; dest p q.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n w1 (reg p) (stack_enc (@cons bool false (@vec_pos (list bool) m v p)))) (reg q)) (stack_enc (@vec_pos (list bool) m v q)) *)
      assert (reg p <> reg q); rew vec.
  Qed.

  Hint Resolve bsm_instr_compile_sound.

  Section bsm_sim.

    Variable (iP : nat) (cP : list (bsm_instr m)).

    Let lnk_Q_pair := @gen_compiler_correction _ _ _ _ bsm_instr_compile_length_eq _ _ _ _  (@bsm_sss_total' _)
                     (@mm_sss_fun _) _ bsm_instr_compile_sound (iP,cP) 1. 

    Let lnk := projT1 lnk_Q_pair.
    Let Q := proj1_sig (projT2 lnk_Q_pair).

    Let Hlnk : fst Q = 1 /\ lnk iP = 1 /\ forall i, out_code i (iP,cP) -> lnk i = code_end Q.
    Proof.
(* Goal: and (@eq nat (@fst nat (list (mm_instr n)) Q) (S O)) (and (@eq nat (lnk iP) (S O)) (forall (i : nat) (_ : @out_code (bsm_instr m) i (@pair nat (list (bsm_instr m)) iP cP)), @eq nat (lnk i) (@code_end (mm_instr n) Q))) *)
      repeat split; apply (proj2_sig (projT2 lnk_Q_pair)).
    Qed.

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

    Let HQ1 : forall i1 v1 w1 i2 v2, v1 ⋈ w1 /\ (iP,cP) /BSM/ (i1,v1) ~~> (i2,v2)     
                    -> exists w2,    v2 ⋈ w2 /\ Q /MM/ (lnk i1,w1) ~~> (lnk i2,w2).
    Proof. apply (proj2_sig (projT2 lnk_Q_pair)). Qed.

    Let HQ2 : forall i1 v1 w1 j2 w2, v1 ⋈ w1 /\ Q /MM/ (lnk i1,w1) ~~> (j2,w2) 
                    -> exists i2 v2, v2 ⋈ w2 /\ (iP,cP) /BSM/ (i1,v1) ~~> (i2,v2) /\ j2 = lnk i2.
    Proof. apply (proj2_sig (projT2 lnk_Q_pair)). Qed.

    Variable v : vec (list bool) m. 

    Let w := 0##0##vec_map stack_enc v.

    Let w_prop : bsm_state_enc v w.
    Proof.
(* Goal: bsm_state_enc v w *)
      red; unfold w, tmp1, tmp2; repeat split; rew vec.
(* Goal: forall p : pos m, @eq nat (@vec_pos nat n (@vec_cons nat (S m) O (@vec_cons nat m O (@vec_map (list bool) nat stack_enc m v))) (reg p)) (stack_enc (@vec_pos (list bool) m v p)) *)
      intros p; unfold reg; simpl. 
(* Goal: @eq nat (@vec_pos nat m (@vec_map (list bool) nat stack_enc m v) p) (stack_enc (@vec_pos (list bool) m v p)) *)
      rewrite vec_pos_map; trivial.
    Qed. 

    (** (iQ,cQ) simulates termination of (iP,cP) while ensuring tmp1 and tmp2 stay void when it terminates *)

    Let Q_spec1 : (iP,cP) /BSM/ (iP,v) ↓ -> exists w', Q /MM/ (1,w) ~~> (code_end Q, w') /\ w'#>tmp1 = 0 /\ w'#>tmp2 = 0.
    Proof.
(* Goal: forall _ : @sss_terminates (bsm_instr m) (vec (list bool) m) (@bsm_sss m) (@pair nat (list (bsm_instr m)) iP cP) (@pair nat (vec (list bool) m) iP v), @ex (vec nat n) (fun w' : vec nat n => and (@sss_output (mm_instr n) (vec nat n) (@mm_sss n) Q (@pair nat (vec nat (S (S m))) (S O) w) (@pair nat (vec nat n) (@code_end (mm_instr n) Q) w')) (and (@eq nat (@vec_pos nat n w' tmp1) O) (@eq nat (@vec_pos nat n w' tmp2) O))) *)
      intros ((i1,v1) & H1).
(* Goal: @ex (vec nat n) (fun w' : vec nat n => and (@sss_output (mm_instr n) (vec nat n) (@mm_sss n) Q (@pair nat (vec nat (S (S m))) (S O) w) (@pair nat (vec nat n) (@code_end (mm_instr n) Q) w')) (and (@eq nat (@vec_pos nat n w' tmp1) O) (@eq nat (@vec_pos nat n w' tmp2) O))) *)
      destruct HQ1 with (1 := conj w_prop H1) as (w' & H2 & H3).
(* Goal: @ex (vec nat n) (fun w' : vec nat n => and (@sss_output (mm_instr n) (vec nat n) (@mm_sss n) Q (@pair nat (vec nat (S (S m))) (S O) w) (@pair nat (vec nat n) (@code_end (mm_instr n) Q) w')) (and (@eq nat (@vec_pos nat n w' tmp1) O) (@eq nat (@vec_pos nat n w' tmp2) O))) *)
      rewrite <- (proj2 (proj2 Hlnk) i1), <- (proj1 (proj2 Hlnk)).
      * exists w'; split; auto; red in H2; tauto.
      * apply H1.
    Qed.

    Let Q_spec2 : Q /MM/ (1,w) ↓ -> (iP,cP) /BSM/ (iP,v) ↓.
    Proof.
(* Goal: forall _ : @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) Q (@pair nat (vec nat (S (S m))) (S O) w), @sss_terminates (bsm_instr m) (vec (list bool) m) (@bsm_sss m) (@pair nat (list (bsm_instr m)) iP cP) (@pair nat (vec (list bool) m) iP v) *)
      intros ((j,w2) & H1).
(* Goal: @sss_terminates (bsm_instr m) (vec (list bool) m) (@bsm_sss m) (@pair nat (list (bsm_instr m)) iP cP) (@pair nat (vec (list bool) m) iP v) *)
      rewrite <- (proj1 (proj2 Hlnk)) in H1.
(* Goal: @sss_terminates (bsm_instr m) (vec (list bool) m) (@bsm_sss m) (@pair nat (list (bsm_instr m)) iP cP) (@pair nat (vec (list bool) m) iP v) *)
      destruct HQ2 with (1 := conj w_prop H1) as (i2 & v2 & H2 & H3 & _).
(* Goal: @sss_terminates (bsm_instr m) (vec (list bool) m) (@bsm_sss m) (@pair nat (list (bsm_instr m)) iP cP) (@pair nat (vec (list bool) m) iP v) *)
      exists (i2,v2); auto.
    Qed.

    Definition bsm_mm_sim := snd Q.

    Theorem bsm_mm_sim_spec : (iP,cP) /BSM/ (iP,v) ↓ <-> (1,bsm_mm_sim) /MM/ (1,w) ↓.
    Proof.
(* Goal: iff (@sss_terminates (bsm_instr m) (vec (list bool) m) (@bsm_sss m) (@pair nat (list (bsm_instr m)) iP cP) (@pair nat (vec (list bool) m) iP v)) (@sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) bsm_mm_sim) (@pair nat (vec nat (S (S m))) (S O) w)) *)
      rewrite <- (proj1 Hlnk) at 1.
(* Goal: iff (@sss_terminates (bsm_instr m) (vec (list bool) m) (@bsm_sss m) (@pair nat (list (bsm_instr m)) iP cP) (@pair nat (vec (list bool) m) iP v)) (@sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (@fst nat (list (mm_instr n)) Q) bsm_mm_sim) (@pair nat (vec nat (S (S m))) (S O) w)) *)
      rewrite <- surjective_pairing.
(* Goal: iff (@sss_terminates (bsm_instr m) (vec (list bool) m) (@bsm_sss m) (@pair nat (list (bsm_instr m)) iP cP) (@pair nat (vec (list bool) m) iP v)) (@sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) Q (@pair nat (vec nat (S (S m))) (S O) w)) *)
      split; auto.
(* Goal: forall _ : @sss_terminates (bsm_instr m) (vec (list bool) m) (@bsm_sss m) (@pair nat (list (bsm_instr m)) iP cP) (@pair nat (vec (list bool) m) iP v), @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) Q (@pair nat (vec nat (S (S m))) (S O) w) *)
      intros H.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) Q (@pair nat (vec nat (S (S m))) (S O) w) *)
      destruct (Q_spec1 H) as (w' & H1 & _).
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) Q (@pair nat (vec nat (S (S m))) (S O) w) *)
      exists (code_end Q, w'); auto.
    Qed.

    Let iE := code_end Q.

    (** We complete (iQ,cQ) with some code nullifying all variables except tmp1 & tmp2 *)

    Let cN := mm_nullify tmp1 iE (map (fun p => pos_nxt (pos_nxt p)) (pos_list m)).
    Let cE := cN ++ DEC tmp1 0 :: nil.
  
    Let E_spec w' : w'#>tmp1 = 0 -> w'#>tmp2 = 0 -> (iE,cE) /MM/ (iE,w') -+> (0,vec_zero).
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n w' tmp1) O) (_ : @eq nat (@vec_pos nat n w' tmp2) O), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) iE cE) (@pair nat (vec nat n) iE w') (@pair nat (vec nat n) O (@vec_zero n)) *)
      intros H1 H2.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) iE cE) (@pair nat (vec nat n) iE w') (@pair nat (vec nat n) O (@vec_zero n)) *)
      unfold cE.
      apply sss_compute_progress_trans with (length cN+iE,vec_zero).
      + apply subcode_sss_compute with (P := (iE,cN)); auto.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) iE cN) (@pair nat (vec nat n) iE w') (@pair nat (vec nat n) (Init.Nat.add (@length (mm_instr n) cN) iE) (@vec_zero n)) *)
        apply mm_nullify_compute; auto.
        * intros p Hp.
(* Goal: @eq nat (@vec_pos nat n (@vec_zero n) p) O *)
          apply in_map_iff in Hp.
(* Goal: forall p : pos m, not (@eq (pos n) (reg p) tmp2) *)
          destruct Hp as (x & H3 & H4); subst; discriminate.
        * intros p Hp.
(* Goal: @eq nat (@vec_pos nat n (@vec_zero n) p) O *)
          apply in_map_iff in Hp.
(* Goal: @eq nat (@vec_pos nat n (@vec_zero n) p) O *)
          destruct Hp as (x & H3 & H4); subst; apply vec_zero_spec.
        * intros p Hp.
          unfold n, tmp1, tmp2 in *; simpl in p.
(* Goal: @eq nat (@vec_pos nat (Init.Nat.add (S (S O)) m) (@vec_zero (Init.Nat.add (S (S O)) m)) (@pos_nxt (S m) p)) (@vec_pos nat (Init.Nat.add (S (S O)) m) w' (@pos_nxt (S m) p)) *)
          pos_inv p; auto.
(* Goal: @eq nat (@vec_pos nat (Init.Nat.add (S (S O)) m) (@vec_zero (Init.Nat.add (S (S O)) m)) (@pos_nxt (S m) p)) (@vec_pos nat (Init.Nat.add (S (S O)) m) w' (@pos_nxt (S m) p)) *)
          pos_inv p; auto.
(* Goal: iff (@sss_terminates (bsm_instr m) (vec (list bool) m) (@bsm_sss m) (@pair nat (list (bsm_instr m)) iP cP) (@pair nat (vec (list bool) m) iP v)) (@sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) Q (@pair nat (vec nat (S (S m))) (S O) w)) *)
          destruct Hp; apply in_map_iff; exists p; split; auto.
(* Goal: @In (pos m) p (pos_list m) *)
          apply pos_list_prop.
      + apply subcode_sss_progress with (P := (length cN+iE,DEC tmp1 0::nil)); auto.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (Init.Nat.add (@length (mm_instr n) cN) iE) (@cons (mm_instr n) (@mm_dec n tmp1 O) (@nil (mm_instr n)))) (@pair nat (vec nat n) (Init.Nat.add (@length (mm_instr n) cN) iE) (@vec_zero n)) (@pair nat (vec nat n) O (@vec_zero n)) *)
        mm sss DEC 0 with tmp1 0.
(* Goal: @subcode (mm_instr n) (@pair nat (list (mm_instr n)) (Init.Nat.add (@length (mm_instr n) cN) iE) (@cons (mm_instr n) (@mm_dec n tmp1 O) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) (Init.Nat.add (@length (mm_instr n) cN) iE) (@cons (mm_instr n) (@mm_dec n tmp1 O) (@nil (mm_instr n)))) *)
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (Init.Nat.add (@length (mm_instr n) cN) iE) (@cons (mm_instr n) (@mm_dec n tmp1 O) (@nil (mm_instr n)))) (@pair nat (vec nat n) O (@vec_zero n)) (@pair nat (vec nat n) O (@vec_zero n)) *)
        apply subcode_refl.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (Init.Nat.add (@length (mm_instr n) cN) iE) (@cons (mm_instr n) (@mm_dec n tmp1 O) (@nil (mm_instr n)))) (@pair nat (vec nat n) O (@vec_zero n)) (@pair nat (vec nat n) O (@vec_zero n)) *)
        mm sss stop.
    Qed.
  
    Definition bsm_mm := snd Q ++ cE.
  
    Let cQ_sim : Q <sc (1,bsm_mm).
    Proof.
(* Goal: @subcode (mm_instr n) Q (@pair nat (list (mm_instr n)) (S O) bsm_mm) *)
      unfold bsm_mm; destruct Q as (iQ,cQ); simpl in Hlnk.
(* Goal: @subcode (mm_instr n) (@pair nat (list (mm_instr n)) iQ cQ) (@pair nat (list (mm_instr n)) (S O) (@app (mm_instr n) (@snd nat (list (mm_instr n)) (@pair nat (list (mm_instr n)) iQ cQ)) cE)) *)
      simpl snd; rewrite (proj1 Hlnk); auto.
    Qed.
  
    Let cE_sim : (iE,cE) <sc (1,bsm_mm).
    Proof.
(* Goal: @subcode (mm_instr n) (@pair nat (list (mm_instr n)) iE cE) (@pair nat (list (mm_instr n)) (S O) bsm_mm) *)
      unfold iE, bsm_mm; subcode_tac; solve list eq.
(* Goal: @eq nat (Init.Nat.add (@fst nat (list (mm_instr n)) Q) (@length (mm_instr n) (@snd nat (list (mm_instr n)) Q))) (S (@length (mm_instr n) (let (_, y) := Q in y))) *)
      rewrite (proj1 Hlnk); auto.
    Qed.

    (** (1,bsm_sim) is a simulator for (iP,cP) *)
  
    Theorem bsm_mm_spec : (iP,cP) /BSM/ (iP,v) ↓ <-> (1,bsm_mm) /MM/ (1,w) ~~> (0,vec_zero).
    Proof.
      split.
      * intros H1.
        apply Q_spec1 in H1.
        destruct H1 as (w' & (H1 & H0) & H2 & H3).
        split.
        2: simpl; omega.
        apply sss_compute_trans with (st2 := (iE,w')).
        revert H1; apply subcode_sss_compute; auto.
        apply sss_progress_compute.
        generalize (E_spec _ H2 H3); apply subcode_sss_progress; auto.
      * intros H1.
        apply Q_spec2.
        apply subcode_sss_terminates with (1 := cQ_sim).
        exists (0,vec_zero); auto.
    Qed.

  End bsm_sim.

End simulator.

Theorem bsm_mm_compiler_1 n i (P : list (bsm_instr n)) :
  { Q : list (mm_instr (2+n)) | forall v, (i,P) /BSM/ (i,v) ↓ <-> (1,Q) /MM/ (1,0##0##vec_map stack_enc v) ↓ }.
Proof. exists (bsm_mm_sim i P); apply bsm_mm_sim_spec. Qed.

Theorem bsm_mm_compiler_2 n i (P : list (bsm_instr n)) :
  { Q : list (mm_instr (2+n)) | forall v, (i,P) /BSM/ (i,v) ↓ <-> (1,Q) /MM/ (1,0##0##vec_map stack_enc v) ~~> (0,vec_zero) }.
Proof. exists (bsm_mm i P); apply bsm_mm_spec. Qed.
