Require Import ZArith.
Require Import List.
Require Import util.
Require Import machine_int.
Import MachineInt.
Require Import machine_int_spec.
Require Import state.
Require Import mips.

(*
 * state-modifying insns of MIPS assembly (i.e., w.o. branching instruction)
 *)

Inductive cmd0 : Set :=
  | skip0 : cmd0
  | add0 : gp_reg -> gp_reg -> gp_reg -> cmd0
  | addi0 : gp_reg -> gp_reg -> immediate -> cmd0
  | addiu0 : gp_reg -> gp_reg -> immediate -> cmd0
  | addu0 : gp_reg -> gp_reg -> gp_reg -> cmd0
  | cmd_and0 : gp_reg -> gp_reg -> word -> cmd0
  | lw0 : gp_reg -> immediate (*index*) -> gp_reg (*base*) -> cmd0
  | lwxs0 : gp_reg -> gp_reg (*index*) -> gp_reg (*base*)-> cmd0
  | maddu0 : gp_reg -> gp_reg -> cmd0
  | mflhxu0 : gp_reg -> cmd0
  | mflo0 : gp_reg -> cmd0
  | mfhi0 : gp_reg -> cmd0
  | mtlo0 : gp_reg -> cmd0
  | mthi0 : gp_reg -> cmd0
  | msubu0 : gp_reg -> gp_reg -> cmd0
  | multu0 : gp_reg -> gp_reg -> cmd0
  | nor0 : gp_reg -> gp_reg -> gp_reg -> cmd0
  | sll0: gp_reg -> gp_reg -> shifta -> cmd0
  | sltu0 : gp_reg -> gp_reg -> gp_reg -> cmd0
  | sw0 : gp_reg -> immediate (*index*) -> gp_reg (*base*) -> cmd0.


Reserved Notation "s -- c --> t" (at level 82, no associativity).

Open Local Scope Z_scope.

Inductive exec0 : option state -> cmd0 -> option state -> Prop :=
  | exec0_skip0 : forall s, Some s -- skip0 --> Some s

  | exec0_addi0 : forall s1 s2 m h rt rs vrs imm,
    gpr.lookup rs s1 = vrs ->
    - 2^^31 <= s2Z vrs + s2Z (sign_extend_16_32 imm) < 2^^31 ->
    Some (s1,s2,m,h) -- addi0 rt rs imm --> Some (gpr.update rt (vrs (+) sign_extend_16_32 imm) s1, s2, m,h)

  | exec0_addiu0 : forall s1 s2 m h rt rs vrs imm,
    gpr.lookup rs s1 = vrs ->
    Some (s1,s2,m,h) -- addiu0 rt rs imm --> Some (gpr.update rt (vrs (+) sign_extend_16_32 imm) s1, s2, m,h)  

  | exec0_add0 : forall s1 s2 vrt vrs m h rd rs rt,
    gpr.lookup rs s1 = vrs ->
    gpr.lookup rt s1 = vrt ->
    - 2^^ 31 <= s2Z vrt + s2Z vrs < 2^^31 ->
    Some (s1,s2,m,h) -- add0 rd rs rt --> Some (gpr.update rd (vrs (+) vrt) s1, s2, m, h)

  | exec0_addu0 : forall s1 s2 vrt vrs m h rd rs rt,
    gpr.lookup rt s1 = vrt ->
    gpr.lookup rs s1 = vrs ->
    Some (s1,s2,m,h) -- addu0 rd rs rt --> Some (gpr.update rd (vrs (+) vrt) s1, s2, m, h)
    
  | exec0_and0 : forall s1 s2 vrt m h rs rt num,  
    gpr.lookup rt s1 = vrt ->
    Some (s1, s2,m,h) -- cmd_and0 rs rt num --> Some (gpr.update rs (int_and vrt num) s1,s2,m,h)
    
  | exec0_lw0 : forall s1 s2 m h rt offset base vbase l z,
    gpr.lookup base s1 = vbase ->
    u2Z (vbase (+) sign_extend_16_32 offset) = 4 * Z_of_nat l -> 
    heap.lookup l h = Some z -> 
    Some (s1,s2,m,h) -- lw0 rt offset base --> Some (gpr.update rt z s1,s2,m,h)
    
  | exec0_lw0_error : forall s1 s2 m h rt offset base vbase,
    gpr.lookup base s1 = vbase ->
    ~(exists l, u2Z (vbase (+) sign_extend_16_32 offset) = 4 * Z_of_nat l /\
      exists z, heap.lookup l h = Some z)->
    Some (s1,s2,m,h) -- lw0 rt offset base --> None

  | exec0_lwxs0 : forall s1 s2 (m:multiplier.m) h rt index vindex base vbase l z,
    gpr.lookup base s1 = vbase ->
    gpr.lookup index s1 = vindex ->
    u2Z (vbase (+) shl 2 vindex) = 4 * Z_of_nat l ->
    heap.lookup l h = Some z -> 
    Some (s1,s2,m,h) -- lwxs0 rt index base --> Some (gpr.update rt z s1,s2,m,h)
    
  | exec0_lwxs0_error : forall s1 s2 (m:multiplier.m) h rt index vindex base vbase,
    gpr.lookup base s1 = vbase ->
    gpr.lookup index s1 = vindex ->
    ~(exists l, u2Z (vbase (+) shl 2 vindex) = 4 * Z_of_nat l /\  exists z,  heap.lookup l h = Some z) ->
    Some (s1,s2,m,h) -- lwxs0 rt index base --> None

  | exec0_maddu0 : forall s1 s2 (m:multiplier.m) h rs vrs rt vrt,
    gpr.lookup rt s1 = vrt ->
    gpr.lookup rs s1 = vrs ->
    Some (s1,s2,m,h) -- maddu0 rs rt --> Some (s1,s2,multiplier.maddu_op (umul vrs vrt) m,h)
    
  | exec0_mflhxu0 : forall s1 s2 m h rd,
    Some (s1,s2,m,h) -- mflhxu0 rd --> Some (gpr.update rd (multiplier.lo m) s1,s2,multiplier.mflhxu_op m,h)

  | exec0_mfhi0 : forall s1 s2 m h rd,
    Some (s1,s2,m,h) -- mfhi0 rd --> Some (gpr.update rd (multiplier.hi m) s1,s2,m,h)

  | exec0_mflo0 : forall s1 s2 m h rd,
    Some (s1,s2,m,h) -- mflo0 rd --> Some (gpr.update rd (multiplier.lo m) s1,s2,m,h)

  | exec0_mthi0 : forall s1 s2 m h rs vrs,
    gpr.lookup rs s1 = vrs ->
    Some (s1,s2,m,h) -- mthi0 rs --> Some (s1,s2,multiplier.mthi_op vrs m,h)

  | exec0_mtlo0 : forall s1 s2 m h rs vrs,
    gpr.lookup rs s1 = vrs ->
    Some (s1,s2,m,h) -- mtlo0 rs --> Some (s1,s2,multiplier.mtlo_op vrs m,h)

  | exec0_msubu0 : forall s1 s2 (m:multiplier.m) h rs vrs rt vrt,
    gpr.lookup rt s1 = vrt ->
    gpr.lookup rs s1 = vrs ->
    Some (s1,s2,m,h) -- msubu0 rs rt --> Some (s1,s2,(multiplier.msubu_op (umul vrs vrt) m),h)

  | exec0_multu0 : forall s1 s2 m h rs vrs rt vrt,
    gpr.lookup rt s1 = vrt ->
    gpr.lookup rs s1 = vrs ->
    Some (s1,s2,m,h) -- multu0 rs rt --> Some (s1,s2,multiplier.multu_op (umul vrs vrt) m,h)

  | exec0_nor0 : forall rd rs rt vrs vrt s1 s2 m h,
    gpr.lookup rs s1 = vrs ->     
    gpr.lookup rt s1 = vrt ->     
    Some (s1,s2,m,h) -- nor0 rd rs rt --> Some (gpr.update rd (int_not (int_or vrs vrt)) s1,s2,m,h)


  | exec0_sll0 : forall s1 s2 m h rx ry sa,
    Some (s1,s2,m,h) -- sll0 rx ry sa --> Some (gpr.update rx (shl (nat_of_Z (u2Z sa)) (gpr.lookup ry s1)) s1,s2,m,h)


  | exec0_sltu0 : forall s1 s2 m h rd rs rt flag,
    flag = (if (Zlt_bool (u2Z (gpr.lookup rs s1)) (u2Z (gpr.lookup rt s1))) then one32 else zero32) ->
    Some (s1,s2,m,h) -- sltu0 rd rs rt --> Some (gpr.update rd flag s1,s2,m,h)

  | exec0_sw0 : forall s1 s2 (m:multiplier.m) h rt vrt offset base vbase l,
    gpr.lookup base s1 = vbase ->
    gpr.lookup rt s1 = vrt ->
    u2Z (vbase (+) sign_extend_16_32 offset) = 4 * Z_of_nat l -> 
    (exists z, heap.lookup l h = Some z) -> 
    Some (s1,s2,m,h) -- sw0 rt offset base --> Some (s1,s2,m,heap.update l vrt h)

  | exec0_sw0_err : forall s1 s2 (m:multiplier.m) h rt vrt offset base vbase,
    gpr.lookup base s1 = vbase ->
    gpr.lookup rt s1 = vrt ->
    ~(exists l, u2Z (vbase (+) sign_extend_16_32 offset) = 4 * Z_of_nat l /\
      exists z, heap.lookup l h = Some z) ->
    Some (s1,s2,m,h) -- sw0 rt offset base --> None

where "s -- c --> t" := (exec0 s c t) : mips0_scope.

Close Local Scope Z_scope.

(*
 * branching insns of MIPS assembly
 *)

Definition label := nat.

Inductive branch : Set :=
  | jmp : label -> branch
  | beq : gp_reg -> gp_reg -> label -> branch
  | bltz : gp_reg -> label -> branch.

Reserved Notation "n '|>' s '>>' c '>>' t" (at level 82, no associativity).

Inductive exec_branch (max:nat) : branch -> nat * option state -> nat * option state -> Prop :=
  | exec_jmp : forall pc st j,
    max >= j ->
    max |> (pc, Some st) >> jmp j >> (j, Some st)

  | exec_jmp_err : forall pc st j,
    max < j ->
    max |> (pc, Some st) >> jmp j >> (j, None) 
    
  | exec_beq_true : forall pc s s' m h r1 r2 j,
    max >= j ->    
    gpr.lookup r1 s = gpr.lookup r2 s ->
    max |> (pc, Some (s,s',m,h)) >> beq r1 r2 j >> (j, Some (s,s',m,h))

  | exec_beq_false : forall pc s s' m h r1 r2 j,
    max >= j ->    
    gpr.lookup r1 s <> gpr.lookup r2 s ->
    max |> (pc, Some (s,s',m,h)) >> beq r1 r2 j >> (pc+1, Some (s,s',m,h))

  | exec_beq_err : forall pc st r1 r2 j,
    max < j ->    
    max |> (pc, Some st) >> beq r1 r2 j >> (j, None)

  | exec_bltz_true : forall pc s s' m h r1 j,
    max >= j ->    
    (s2Z (gpr.lookup r1 s) < 0)%Z ->
    max |> (pc, Some (s,s',m,h)) >> bltz r1 j >> (j, Some (s,s',m,h))

  | exec_bltz_false : forall pc s s' m h r1 j,
    max >= j ->    
    (s2Z (gpr.lookup r1 s) >= 0)%Z ->
    max |> (pc, Some (s,s',m,h)) >> bltz r1 j >> (pc+1, Some (s,s',m,h))

  | exec_bltz_err : forall pc st r1 j,
    max < j ->    
    max |> (pc, Some st) >> bltz r1 j >> (j, None)

where "n '|>' s '>>' c '>>' t" := (exec_branch n c s t) : mips0_scope.

(*
 * MIPS assembly
 *)

Inductive insn : Set :=
  | cmd_insn : cmd0 -> insn
  | branch_insn : branch -> insn
  | no_insn : insn.

Definition prog := list insn.

Definition Nth (i:nat) (p:prog) : insn := nth i p no_insn.

Reserved Notation "p ||-- s --> t" (at level 70, no associativity).

Open Local Scope mips0_scope.

Inductive exec_asm (prg:prog) : nat * option state -> nat * option state -> Prop :=
  | exec_asm_refl : forall st pc,
    prg ||-- (pc, st) --> (pc, st)

  | exec_asm_trans : forall pc pc' pc'' st st' st'',
    prg ||-- (pc, st) --> (pc', st') -> prg ||-- (pc', st') --> (pc'', st'') ->
    prg ||-- (pc, st) --> (pc'', st'')

  | exec_asm_cmd0 : forall pc c st pc' st', 
    Nth pc prg = cmd_insn c ->
    Some st -- c --> Some st' ->
    pc' = pc + 1 ->
    prg ||-- (pc, Some st) --> (pc', Some st')

  | exec_asm_cmd0_err : forall pc c st,
    Nth pc prg = cmd_insn c ->
    Some st -- c --> None ->
    prg ||-- (pc, Some st) --> (pc, None)

  | exec_asm_branch : forall pc j st pc' st',
    Nth pc prg = branch_insn j ->
    length prg |> (pc, Some st) >> j >> (pc', st') ->
    prg ||-- (pc, Some st) --> (pc', st')

  | exec_asm_branch_err : forall pc j st pc',
    Nth pc prg = branch_insn j ->
    length prg |> (pc, Some st) >> j >> (pc', None) ->
    prg ||-- (pc, Some st) --> (pc, None)

where "p ||-- s --> t" := (exec_asm p s t) : mips0_scope.

(*
 * properties of exec_asm
 *) 

Lemma exec_asm_none : forall p s s', 
  p ||-- s --> s' ->
    forall pc st pc' st',
      s = (pc, st) -> 
      s' = (pc', st') -> 
      st = None ->
      st' = None.
  do 4 intro.
  induction H; intros.
  inversion H; clear H; subst pc0 st0.
  inversion H0; clear H0; subst pc' st'.
  assumption.
  injection H1; clear H1; intros; subst pc0 st0.
  injection H2; clear H2; intros; subst pc'0 st'0.
  eapply IHexec_asm2.
  intuition.
  intuition.
  eapply IHexec_asm1.
  intuition.
  intuition.
  auto.
  inversion H2; subst st0; discriminate.
  inversion H2; subst st0; discriminate.
  inversion H2; subst st0; discriminate.
  inversion H2; subst st0; discriminate.
Qed.

Lemma nth_prog_no_insn: forall p index,
  nth index p no_insn <> no_insn ->
  index < length p.
  induction p; simpl; intros.
  destruct index; tauto.
  destruct index.
  apply lt_O_Sn.
  apply lt_n_S.
  apply IHp; auto.
Qed.

Lemma exec_branch_extend_prog : forall j (p:prog) pc st pc' st',
  length p |> (pc, Some st) >> j >> (pc', Some st') ->
    forall n,
      length p + n |> (pc, Some st) >> j >> (pc', Some st').
  intros.
  inversion_clear H; constructor; try omega||auto.
Qed.

Lemma exec_asm_extend_prog' : forall p s s',
  p ||-- s --> s' ->
    forall pc st pc' st' p',
      s = (pc, Some st) ->
      s' = (pc', Some st') ->
      p ++ p' ||-- (pc, Some st) --> (pc', Some st').
  do 4 intro.
  induction H; intros.

  inversion H; inversion H0.
  subst pc0 pc'.
  rewrite H3 in H5; injection H5; clear H5; intros; subst st0.
  constructor.

  destruct st'.
  inversion H1; inversion H2; clear H1 H2.
  subst pc'' pc st'' st.
  eapply exec_asm_trans with (pc' := pc') (st' := Some s).
  eapply IHexec_asm1; auto.
  eapply IHexec_asm2; auto.
  
  inversion H1; inversion H2; clear H1 H2.
  subst pc'' pc st'' st.
  assert (Some st'0 = None).
  eapply exec_asm_none.
  apply H0.
  intuition.
  intuition.
  reflexivity.
  discriminate.
  
  inversion H2; inversion H3; clear H2 H3.
  subst pc0 st0 pc'0 st'0.
  eapply exec_asm_cmd0; auto.
  unfold Nth.
  rewrite <- nth_beyond.
  apply H.
  apply nth_prog_no_insn.
  intro.
  unfold Nth in H.
  rewrite H in H2.
  discriminate.
  assumption.

  inversion H2.

  inversion H1; inversion H2; clear H1 H2.
  subst pc0 st0 pc'0 st'.
  apply exec_asm_branch with (j := j).  
  unfold Nth.
  rewrite <- nth_beyond.
  assumption.
  apply nth_prog_no_insn.
  intro.
  unfold Nth in H.
  rewrite H in H1.
  discriminate.
  rewrite length_app.
  eapply exec_branch_extend_prog.
  assumption.
  
  inversion H2.
Qed.

Lemma exec_asm_extend_prog : forall p pc st pc' st',
  length p = pc' ->
  p ||-- (pc, Some st) --> (pc', Some st') ->
    forall p',
      p ++ p' ||-- (pc, Some st) --> (pc', Some st').
  intros.
  eapply exec_asm_extend_prog'.
  apply H0.
  auto.
  auto.
Qed.

(*
 * translator
 *)  

Open Local Scope mips_scope.

Fixpoint translate (lbl:nat) (c:cmd) {struct c} : prog := 
  match c with 
    | skip 		=> cmd_insn skip0 :: nil
    | add r1 r2 r3 	=> cmd_insn (add0 r1 r2 r3) :: nil
    | addi r1 r2 i 	=> cmd_insn (addi0 r1 r2 i) :: nil
    | addiu r1 r2 i 	=> cmd_insn (addiu0 r1 r2 i) :: nil
    | addu r1 r2 r3 	=> cmd_insn (addu0 r1 r2 r3) :: nil
    | cmd_and r1 r2 w 	=> cmd_insn (cmd_and0 r1 r2 w) :: nil
    | lw r1 i r2 	=> cmd_insn (lw0 r1 i r2) :: nil
    | lwxs r1 r2 r3 	=> cmd_insn (lwxs0 r1 r2 r3) ::nil
    | maddu r1 r2 	=> cmd_insn (maddu0 r1 r2) :: nil
    | mflhxu r	 	=> cmd_insn (mflhxu0 r) :: nil
    | mflo r 		=> cmd_insn (mflo0 r) :: nil
    | mfhi r 		=> cmd_insn (mfhi0 r) :: nil
    | mtlo r 		=> cmd_insn (mtlo0 r) :: nil
    | mthi r 		=> cmd_insn (mthi0 r) :: nil
    | msubu r1 r2 	=> cmd_insn (msubu0 r1 r2) :: nil
    | multu r1 r2 	=> cmd_insn (multu0 r1 r2) :: nil
    | nor r1 r2 r3 	=> cmd_insn (nor0 r1 r2 r3) :: nil
    | sll r1 r2 r3 	=> cmd_insn (sll0 r1 r2 r3) :: nil
    | sltu r1 r2 r3 	=> cmd_insn (sltu0 r1 r2 r3) :: nil
    | sw r1 i r2 	=> cmd_insn (sw0 r1 i r2) :: nil
    | seq c1 c2 => 
      let prg1 := translate lbl c1 in 
        let prg2 := translate (lbl + length prg1) c2 in
          prg1 ++ prg2
    | ifte_beq r1, r2 thendo c1 elsedo c2 => 
      let prg1 := translate (lbl + 1) c2 in 
        let prg2 := translate (lbl + length prg1 + 2) c1 in
          branch_insn (beq r1 r2 (lbl + length prg1 + 2)) :: prg1 ++ 
          branch_insn (jmp (lbl + length prg1 + length prg2 + 2)) :: prg2
    | while_bne r1 r2 c =>
      let prg1 := translate (lbl + 1) c in 
        branch_insn (beq r1 r2 (lbl + length prg1 + 2)) :: prg1 ++ 
	branch_insn (jmp lbl) :: nil
    | ifte_bltz r1 thendo c1 elsedo c2 => 
      let prg1 := translate (lbl + 1) c2 in 
        let prg2 := translate (lbl + length prg1 + 2) c1 in
          branch_insn (bltz r1 (lbl + length prg1 + 2)) :: prg1 ++ 
          branch_insn (jmp (lbl + length prg1 + length prg2 + 2)) :: prg2
  end.

(*
Require Import mont.

Eval compute in (translate 0%nat (montgomery k alpha x y z m int_ ext X_ Y_ M_ Z_ one gpr_zero quot C t s)).

Definition mont_bin := (translate 0%nat (montgomery k alpha x y z m int_ ext X_ Y_ M_ Z_ one gpr_zero quot C t s)).

*)

(*Recursive Extraction mont_bin.*)

(*
 * correctness of the translator
 *)

Lemma translate_correct': forall c n c',
  translate n c  = c' ->
  forall st st',
    exec (Some st) c (Some st') ->
    forall prg, 
      length prg = n ->
      forall m,
	m = n + length c' ->
	prg ++ c' ||-- (n, Some st) --> (m, Some st').

  induction c; intros.

  Ltac tmp_cmd H H0 H1 H2 :=
    inversion_clear H0;
    simpl in H; subst c'; 
    simpl in H2;
    eapply exec_asm_cmd0; 
    [unfold Nth; rewrite nth_app; rewrite H1; [rewrite <-minus_n_n; simpl; reflexivity | constructor] | 
     econstructor; auto | 
     simpl; omega].

  (* case skip *)

  tmp_cmd H H0 H1 H2.

  (* case add *)

  tmp_cmd H H0 H1 H2.

  (* case addi *)

  tmp_cmd H H0 H1 H2.

  (* case addiu *)

  tmp_cmd H H0 H1 H2.

  (* case addu *)

  tmp_cmd H H0 H1 H2.

  (* case cmd_and *)

  tmp_cmd H H0 H1 H2.

  (* case lw *)

  tmp_cmd H H0 H1 H2.
  rewrite H3.
  apply H4.
  auto.
  
  (* case lwxs *)

  tmp_cmd H H0 H1 H2.
  rewrite H3.
  rewrite H4.
  apply H5.
  auto.

  (* case maddu *)

  tmp_cmd H H0 H1 H2.

  (* case mflhxu *)

  tmp_cmd H H0 H1 H2.

  (* case mflo *)

  tmp_cmd H H0 H1 H2.

  (* case mfhi *)

  tmp_cmd H H0 H1 H2.

  (* case mtlo *)

  tmp_cmd H H0 H1 H2.

  (* case mthi *)

  tmp_cmd H H0 H1 H2.

  (* case msubu *)

  tmp_cmd H H0 H1 H2.

  (* case multu *)

  tmp_cmd H H0 H1 H2.

  (* case nor *)

  tmp_cmd H H0 H1 H2.

  (* case sll *)

  tmp_cmd H H0 H1 H2.

  (* case sltu *)

  tmp_cmd H H0 H1 H2.

  (* case sw *)

  tmp_cmd H H0 H1 H2.
  rewrite H3.
  assumption.

  (* case c1;c2 *)

  simpl in H.
  inversion_clear H0.
  destruct s'.
  apply exec_asm_trans with (pc' := n + length (translate n c1)) (st' := Some s).
  rewrite <-H.
  cutrewrite ( prg ++ translate n c1 ++ translate (n + length (translate n c1)) c2 =
    (prg ++ translate n c1) ++ translate (n + length (translate n c1)) c2 ).
  apply exec_asm_extend_prog.
  rewrite length_app.
  rewrite H1; reflexivity.
  eapply IHc1; auto.
  repeat rewrite app_ass; auto.
  rewrite <-H.
  cutrewrite ( prg ++ translate n c1 ++ translate (n + length (translate n c1)) c2 =
    (prg ++ translate n c1) ++ translate (n + length (translate n c1)) c2 ).
  eapply IHc2; auto.
  rewrite length_app.
  omega.
  rewrite <-H in H2.
  rewrite length_app in H2.
  omega.
  repeat rewrite app_ass; auto.
  generalize (from_none _ _ H4); intros; discriminate.

  (* case ifte_beq *)

  simpl in H.
  inversion_clear H0.

  (* case true *)

  apply exec_asm_trans with (pc' := n + length (translate (n + 1) c2) + 2) (st' := Some (s1, s2, m0, h)).
  apply exec_asm_branch with (beq g g0 (n + length (translate (n + 1) c2) + 2)).
  unfold Nth; rewrite nth_app.
  rewrite H1.
  rewrite <-minus_n_n.
  rewrite <-H; simpl.
  auto.
  omega.
  apply exec_beq_true; auto.
  rewrite length_app.
  rewrite <-H.
  simpl.
  rewrite length_app.
  simpl.
  omega.
  rewrite <-H.
  cutrewrite ( prg ++
   branch_insn (beq g g0 (n + length (translate (n + 1) c2) + 2))
   :: translate (n + 1) c2 ++
      branch_insn
        (jmp
           (n + length (translate (n + 1) c2) +
            length (translate (n + length (translate (n + 1) c2) + 2) c1) + 2))
      :: translate (n + length (translate (n + 1) c2) + 2) c1 =
      (prg ++
   branch_insn (beq g g0 (n + length (translate (n + 1) c2) + 2))
   :: translate (n + 1) c2 ++
      branch_insn
        (jmp
           (n + length (translate (n + 1) c2) +
            length (translate (n + length (translate (n + 1) c2) + 2) c1) + 2)) :: nil)
      ++ translate (n + length (translate (n + 1) c2) + 2) c1).
  eapply IHc1; auto.
  rewrite length_app.
  simpl.
  rewrite length_app.
  simpl.
  omega.
  rewrite H2.
  rewrite <-H.
  simpl.
  rewrite length_app.
  simpl.
  omega.
  repeat rewrite app_ass; simpl; auto.
  repeat rewrite app_ass; simpl; auto.

  (* case false *)

  apply exec_asm_trans with (pc' := n + 1) (st' := Some (s1, s2, m0, h)).
  eapply exec_asm_branch with (beq g g0 (n + length (translate (n + 1) c2) + 2)).
  unfold Nth; rewrite nth_app.
  rewrite <-H1.
  rewrite <-minus_n_n.
  rewrite <-H.
  simpl.
  rewrite H1.
  reflexivity.
  omega.
  apply exec_beq_false; auto.
  rewrite length_app.
  rewrite <-H.
  simpl.
  rewrite length_app.
  simpl.
  omega.
  rewrite <-H.
  cutrewrite (  prg ++
   branch_insn (beq g g0 (n + length (translate (n + 1) c2) + 2))
   :: translate (n + 1) c2 ++
      branch_insn
        (jmp
           (n + length (translate (n + 1) c2) +
            length (translate (n + length (translate (n + 1) c2) + 2) c1) + 2))
      :: translate (n + length (translate (n + 1) c2) + 2) c1 =
       ((prg ++
   branch_insn (beq g g0 (n + length (translate (n + 1) c2) + 2)) :: nil) ++ translate (n + 1) c2) ++
      (branch_insn
        (jmp
           (n + length (translate (n + 1) c2) +
            length (translate (n + length (translate (n + 1) c2) + 2) c1) + 2))
      :: translate (n + length (translate (n + 1) c2) + 2) c1)).
  apply exec_asm_trans with (pc' := n + 1 + length (translate (n + 1) c2)) (st' := Some st').
  apply exec_asm_extend_prog.
  repeat rewrite length_app.
  simpl.
  omega.
  eapply IHc2; auto.
  rewrite length_app.
  simpl.
  omega.
  eapply exec_asm_branch.
  unfold Nth.
  rewrite nth_app.
  assert (n + 1 + length (translate (n + 1) c2) - length
    ((prg ++ branch_insn (beq g g0 (n + length (translate (n + 1) c2) + 2)) :: nil) ++ translate (n + 1) c2) = 0).
  repeat rewrite length_app.
  simpl.
  omega.
  rewrite H0; clear H0.
  simpl.
  reflexivity.
  repeat rewrite length_app.
  simpl.
  omega.
  assert ( n + length (translate (n + 1) c2) + length (translate (n + length (translate (n + 1) c2) + 2) c1) + 2 = m ).
  rewrite H2; rewrite <-H; simpl.
  repeat rewrite length_app.
  simpl.
  omega.
  rewrite H0; clear H0.
  apply exec_jmp; auto.
  repeat rewrite length_app; simpl.
  rewrite H2; rewrite <-H; simpl.
  repeat rewrite length_app; simpl.
  omega.
  repeat rewrite app_ass.
  reflexivity.

  (* case ifte_bltz *)

  simpl in H.
  inversion_clear H0.

  (* case true *)

  apply exec_asm_trans with (pc' := n + length (translate (n + 1) c2) + 2) (st' := Some (s1, s2, m0, h)).
  apply exec_asm_branch with (j := bltz g (n + length (translate (n + 1) c2) + 2)).
  unfold Nth; rewrite nth_app.
  rewrite H1.
  rewrite <-minus_n_n.
  rewrite <-H; simpl.
  reflexivity.
  omega.
  apply exec_bltz_true; auto.
  rewrite length_app.
  rewrite H1; rewrite <-H2; simpl.
  rewrite <-H in H2; simpl in H2.
  rewrite length_app in H2.
  simpl in H2.
  omega.
  rewrite <-H.
  cutrewrite ( prg ++
   branch_insn (bltz g (n + length (translate (n + 1) c2) + 2))
   :: translate (n + 1) c2 ++
      branch_insn
        (jmp
           (n + length (translate (n + 1) c2) +
            length (translate (n + length (translate (n + 1) c2) + 2) c1) + 2))
      :: translate (n + length (translate (n + 1) c2) + 2) c1 =
      (prg ++
   branch_insn (bltz g (n + length (translate (n + 1) c2) + 2))
   :: translate (n + 1) c2 ++
      branch_insn
        (jmp
           (n + length (translate (n + 1) c2) +
            length (translate (n + length (translate (n + 1) c2) + 2) c1) + 2)) :: nil)
      ++ translate (n + length (translate (n + 1) c2) + 2) c1).
  eapply IHc1; auto.
  repeat rewrite length_app; simpl.
  repeat rewrite length_app; simpl.
  omega.
  rewrite H2; rewrite <-H; simpl.
  repeat rewrite length_app; simpl.
  omega.
  repeat rewrite app_ass; simpl.
  repeat rewrite app_ass; simpl.
  reflexivity.

  (* case false *)

  apply exec_asm_trans with (pc' := n + 1) (st' := Some (s1, s2, m0, h)).
  eapply exec_asm_branch with (bltz g (n + length (translate (n + 1) c2) + 2)).
  unfold Nth; rewrite nth_app.
  rewrite <-H1.
  rewrite <-minus_n_n.
  rewrite <-H.
  simpl.
  rewrite H1.
  reflexivity.
  omega.
  apply exec_bltz_false; auto.
  rewrite length_app.
  rewrite <-H.
  repeat rewrite length_app; simpl.
  repeat rewrite length_app; simpl.
  omega.
  rewrite <-H.
  cutrewrite (  prg ++
   branch_insn (bltz g (n + length (translate (n + 1) c2) + 2))
   :: translate (n + 1) c2 ++
      branch_insn
        (jmp
           (n + length (translate (n + 1) c2) +
            length (translate (n + length (translate (n + 1) c2) + 2) c1) + 2))
      :: translate (n + length (translate (n + 1) c2) + 2) c1 =
       ((prg ++
   branch_insn (bltz g (n + length (translate (n + 1) c2) + 2)) :: nil) ++ translate (n + 1) c2) ++
      (branch_insn
        (jmp
           (n + length (translate (n + 1) c2) +
            length (translate (n + length (translate (n + 1) c2) + 2) c1) + 2))
      :: translate (n + length (translate (n + 1) c2) + 2) c1)).
  apply exec_asm_trans with (pc' := n + 1 + length (translate (n+1) c2)) (st' := Some st').
  apply exec_asm_extend_prog.
  repeat rewrite length_app; simpl.
  omega.
  eapply IHc2; auto.
  repeat rewrite length_app; simpl.
  omega.
  eapply exec_asm_branch.
  unfold Nth; rewrite nth_app.
  assert ((n + 1 + length (translate (n + 1) c2) -
      length
        ((prg ++
          branch_insn (bltz g (n + length (translate (n + 1) c2) + 2))
          :: nil) ++ translate (n + 1) c2)) = 0).
  repeat rewrite length_app; simpl.
  omega.
  rewrite H0; clear H0.
  simpl.
  reflexivity.
  repeat rewrite length_app; simpl.
  omega.
  assert ( (n + length (translate (n + 1) c2) +
      length (translate (n + length (translate (n + 1) c2) + 2) c1) + 2) = m ).
  rewrite H2; rewrite <-H; simpl.
  repeat rewrite length_app.
  simpl.
  omega.
  rewrite H0; clear H0.
  apply exec_jmp.
  repeat rewrite length_app; simpl.
  rewrite H2; rewrite <-H; simpl.
  repeat rewrite length_app; simpl.
  omega.
  repeat rewrite app_ass.
  reflexivity.

  (* case while_bne *)

  generalize IHc prg c' H H1 m H2.
  clear IHc prg c' H H1 m H2.

  assert (exists d, d = Some st).
  exists (Some st); auto.
  assert (exists d, d = Some st').
  exists (Some st'); auto.
  assert (exists d, d = while_bne g g0 c).
  exists (while_bne g g0 c); auto.
  inversion_clear H as [ST].
  inversion_clear H1 as [ST'].
  inversion_clear H2 as [C].
  rewrite <- H3 in H0.
  rewrite <- H in H0.
  rewrite <- H1 in H0.
  generalize g g0 c st st' H3 H H1.
  clear g g0 c st st' H3 H H1.

  induction H0; intros; try discriminate.

  (* case true (r1 <> r2) *)

  subst s''; inversion_clear H3.
  clear IHexec1.
  destruct s'.
  injection H1; clear H1; intros; subst c0 r1 r2.
  simpl in H2.

  apply exec_asm_trans with (pc' := length (prg ++ (translate (length prg + 1) c)) + 1) (st' := Some s).

  apply exec_asm_trans with (pc' := length prg + 1) (st' := Some (s1,s2,m,h)).

  (* test d'entree dans la boucle *)

  clear IHexec2 H0_0.
  rewrite <- H2.
  eapply exec_asm_branch.
  unfold Nth; rewrite nth_app.
  rewrite H4.
  rewrite <-minus_n_n.
  simpl.
  reflexivity.
  omega.
  rewrite H4.
  eapply exec_beq_false.
  repeat rewrite length_app; simpl.
  repeat rewrite length_app; simpl.
  omega.
  simpl in H.
  intro; apply H.
  rewrite H0; reflexivity.

  (* body de la loop *)

  clear IHexec2 H0_0.
  rewrite <- H2.
  cutrewrite ( prg ++
   branch_insn (beq g g0 (n + length (translate (n + 1) c) + 2))
   :: translate (n + 1) c ++ branch_insn (jmp n) :: nil =
   ((prg ++
   branch_insn (beq g g0 (n + length (translate (n + 1) c) + 2))::nil)
   ++ translate (n + 1) c) ++ (branch_insn (jmp n) :: nil) ).
  apply exec_asm_extend_prog.
  repeat rewrite length_app; simpl.
  rewrite H4.
  omega.
  eapply IHc; auto.
  rewrite H4.
  auto.
  repeat rewrite length_app; simpl.
  auto.
  repeat rewrite length_app; simpl.
  rewrite H4.
  omega.
  repeat rewrite app_ass.
  reflexivity.

  (* le jump qui permet de retourner en debut de boucle *)

  apply exec_asm_trans with (pc' := length prg) (st' := Some s).
  clear IHexec2 H0_0 IHc.
  rewrite <- H2.
  eapply exec_asm_branch.
  unfold Nth; rewrite nth_app.
  cutrewrite ( 
    (branch_insn (beq g g0 (n + length (translate (n + 1) c) + 2))
      :: translate (n + 1) c ++ branch_insn (jmp n) :: nil) =
    (branch_insn (beq g g0 (n + length (translate (n + 1) c) + 2)) :: nil)
      ++ (translate (n + 1) c ++ branch_insn (jmp n) :: nil) 
  ).
  rewrite nth_app.
  simpl.
  rewrite nth_app.
  cutrewrite (length (prg ++ translate (length prg + 1) c) + 1 - length prg - 1 -
      length (translate (n + 1) c) = 0).
  simpl.
  reflexivity.
  rewrite H4.
  rewrite length_app.
  omega.
  rewrite length_app.
  rewrite H4.
  omega.
  rewrite length_app.
  simpl.
  omega.
  repeat rewrite app_ass; reflexivity.
  rewrite length_app.
  omega.
  rewrite H4.
  eapply exec_jmp.
  repeat rewrite length_app; simpl.
  repeat rewrite length_app; simpl.
  omega.
  
  (* inductive case *)

  rewrite H4.
  eapply IHexec2; auto.
  generalize (from_none _ _ H0_0); intros; discriminate.
  
  (* false *)  
  
  inversion_clear H3; inversion_clear H0.
  injection H1; clear H1; intros; subst g g0 c0.
  eapply exec_asm_branch.
  unfold Nth; rewrite nth_app.
  rewrite H4.
  rewrite <-minus_n_n.
  rewrite <- H2.
  simpl.
  reflexivity.
  omega.
  cutrewrite (m0 = n + length (translate (n + 1) c) + 2).
  eapply exec_beq_true.
  rewrite length_app.
  rewrite <-H2.
  simpl.
  rewrite length_app.
  simpl.
  omega.
  apply u2Z_injection; auto.
  rewrite H5; simpl in H2; rewrite <-H2; simpl.
  rewrite length_app.
  simpl.
  omega.
Qed.

Lemma translate_correct : forall c st prg c' st',
  translate (length prg) c = c' ->
  exec (Some st) c (Some st') ->
  prg ++ c' ||-- (length prg, Some st) --> (length prg + length c', Some st').
  intros.
  eapply translate_correct'; auto.
  apply H.
  auto.
Qed.

(*Lemma semax_sound : forall P Q c,
  {{ P }} c {{ Q }} -> forall prg c',
    translate (length prg) c = c' ->
    forall s1 s2 m h,
      P s1 s2 m h ->
      forall s1' s2' m' h',
	prg ++ c' ||-- (length prg, Some (s1,s2,m,h)) --> (length prg + length c', Some (s1',s2',m',h')) ->
	  Q s1' s2' m' h'.
intros.
generalize (semax_sound _ _ _ H); intro X.
red in X.
generalize (X s1 s2 m h); clear X; intro X.
inversion_clear X as [X1 X2].
apply (X2 s1' s2' m' h' H1).
Abort.*)