include "RTLabs/syntax.ma".
include "RTL/RTL_paolo.ma".
include "common/AssocList.ma".
include "common/FrontEndOps.ma".
include "common/Graphs.ma".
include "joint/TranslateUtils_paolo.ma".
include "utilities/lists.ma".
include alias "ASM/BitVector.ma".
include alias "arithmetics/nat.ma".


definition size_of_sig_type ≝
  λsig.
  match sig with
  [ ASTint isize sign ⇒
    let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
      isize' ÷ (nat_of_bitvector ? int_size)
  | ASTfloat _ ⇒ ? (* dpm: not implemented *)
  | ASTptr rgn ⇒ nat_of_bitvector ? ptr_size
  ].
  cases not_implemented;
qed.

inductive register_type: Type[0] ≝
  | register_int: register → register_type
  | register_ptr: register → register → register_type.

definition local_env ≝ identifier_map RegisterTag (list register).

definition local_env_typed :
  list (register × typ) → local_env → Prop ≝
  λl,env.All ?
    (λp.let 〈r, ty〉 ≝ p in ∃regs.lookup … env r = Some ? regs ∧
                                 |regs| = size_of_sig_type ty) l.

definition find_local_env ≝ λr.λlenv : local_env.
  λprf : r ∈ lenv.opt_safe … (lookup … lenv r) ?.
lapply (in_map_domain … lenv r)
>prf * #x #lookup_eq >lookup_eq % #ABS destruct(ABS)
qed.

lemma find_local_env_elim : ∀P : list register → Prop.∀r. ∀lenv: local_env.∀prf.
  (∀x.lookup … lenv r = Some ? x → P x) → P (find_local_env r lenv prf).
#P#r#lenv#prf #H
change with (P (opt_safe ???))
@opt_safe_elim assumption
qed.

definition find_local_env_arg ≝
  λr,lenv,prf. map … Reg (find_local_env r lenv prf).

let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
  match n with
  [ O ⇒ 〈[],runiverse〉
  | S n' ⇒
     let 〈r,runiverse〉 ≝ fresh … runiverse in
     let 〈res,runiverse〉 ≝ register_freshes runiverse n' in
      〈r::res,runiverse〉 ].

definition initialize_local_env_internal ≝
  λlenv_runiverse : local_env × ?.
  λr_sig.
  let 〈lenv,runiverse〉 ≝ lenv_runiverse in
  let 〈r, sig〉 ≝ r_sig in
  let size ≝ size_of_sig_type sig in
  let 〈rs,runiverse〉 ≝ register_freshes runiverse size in
    〈add … lenv r rs,runiverse〉.

definition initialize_local_env ≝
  λruniverse.
  λregisters.
  λresult.
  let registers ≝ 
    match result with
    [ None ⇒ registers
    | Some rt ⇒ rt :: registers
    ]
  in
    foldl … initialize_local_env_internal 〈empty_map …,runiverse〉 registers.

definition map_list_local_env_internal ≝
  λlenv,res,r_sig. res @ (find_local_env (pi1 … r_sig) lenv (pi2 … r_sig)).
    
definition map_list_local_env ≝
  λlenv,regs. foldl … (map_list_local_env_internal lenv) [ ] regs.

definition make_addr ≝
  λA.
  λlst: list A.
  λprf: 2 = length A lst.
  match lst return λx. 2 = |x| → A × A with
  [ nil ⇒ λlst_nil_prf. ⊥
  | cons hd tl ⇒ λprf.
    match tl return λx. 1 = |x| → A × A with
    [ nil ⇒ λtl_nil_prf. ⊥
    | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
    ] ?
  ] prf.
  [1: normalize in lst_nil_prf;
      destruct(lst_nil_prf)
  |2: normalize in prf;
      @injective_S
      assumption
  |3: normalize in tl_nil_prf;
      destruct(tl_nil_prf)
  ]
qed.

definition find_and_addr ≝
  λr,lenv,prf. make_addr ? (find_local_env r lenv prf).

definition rtl_args ≝
  λlenv,regs_list. flatten … (map … (λr.find_local_env_arg (pi1 … r) lenv (pi2 … r)) regs_list).

definition split_into_bytes:
  ∀size. ∀int: bvint size. Σbytes: list Byte. |bytes| = size_intsize size ≝ 
λsize.
 match size return λsize.∀int: bvint size. Σbytes. |bytes| = size_intsize size with
  [ I8 ⇒ λint. ? | I16 ⇒ λint. ? | I32 ⇒ λint. ? ].
[ %[@[int]] //
| %[@(let 〈h,l〉 ≝ vsplit ? 8 … int in [l;h])] cases (vsplit ????) normalize //
| %[@(let 〈h1,l〉 ≝ vsplit ? 8 … int in
      let 〈h2,l〉 ≝ vsplit ? 8 … l in
      let 〈h3,l〉 ≝ vsplit ? 8 … l in
       [l;h3;h2;h1])]
  cases (vsplit ????) #h1 #l normalize
  cases (vsplit ????) #h2 #l normalize
  cases (vsplit ????) // ]
qed.

definition translate_op:
  ∀globals. Op2 →
  ∀dests : list register.
  ∀srcrs1 : list rtl_argument.
  ∀srcrs2 : list rtl_argument.
  |dests| = |srcrs1| → |srcrs1| = |srcrs2| →
  list (rtl_step globals)
   ≝
  λglobals: list ident.
  λop.
  λdestrs.
  λsrcrs1.
  λsrcrs2.
  λprf1,prf2.
  let f_add ≝ OP2 rtl_params globals in
  let res : list (rtl_step globals) ≝
    map3 ???? (f_add op) destrs srcrs1 srcrs2 ?? in
  (* first, clear carry if op relies on it *)
  match op with
  [ Addc ⇒ [CLEAR_CARRY ??]
  | Sub ⇒ [CLEAR_CARRY ??]
  | _ ⇒ [ ]
  ] @ 
  match op with
  (* if adding, we use a first Add op, that clear the carry, and then Addc's *)
  [ Add ⇒
    match destrs return λx.|destrs| = |x| → list (rtl_step globals) with
    [ nil ⇒ λeq_destrs.[ ]
    | cons destr destrs' ⇒ λeq_destrs.
      match srcrs1 return λy.|srcrs1| = |y| → list (rtl_step globals) with
      [ nil ⇒ λeq_srcrs1.⊥
      | cons srcr1 srcrs1' ⇒ λeq_srcrs1.
        match srcrs2 return λz.|srcrs2| = |z| → list (rtl_step globals) with
        [ nil ⇒ λeq_srcrs2.⊥
        | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
          f_add Add destr srcr1 srcr2 ::
          map3 ???? (f_add Addc) destrs' srcrs1' srcrs2' ??
        ] (refl …)
      ] (refl …)
    ] (refl …)
  | _ ⇒ res
  ].
  [5,6: assumption
  |1: >prf1 in eq_destrs; >eq_srcrs1 normalize //
  |2: >prf2 in eq_srcrs1; >eq_srcrs2 normalize //
  |3: >prf2 in eq_srcrs1; >eq_srcrs2 normalize #H destruct(H)
  |4: >prf1 in eq_destrs; >eq_srcrs1 normalize #H destruct(H)
qed.

let rec nat_to_args (size : nat) (k : nat) on size : Σl : list rtl_argument.|l| = size ≝
match size with
[ O ⇒ [ ]
| S size' ⇒
  match nat_to_args size' (k ÷ 8) with
  [ mk_Sig res prf ⇒
    imm_nat k :: res
  ]
]. normalize // qed.

definition size_of_cst ≝ λcst.match cst with
  [ Ointconst size _ ⇒ size_intsize size
  | Ofloatconst float ⇒ ? (* not implemented *)
  | _ ⇒ 2
  ].
  cases not_implemented qed.

definition cst_well_defd : list ident → constant → Prop ≝ λglobals,cst.
  match cst with
  [ Oaddrsymbol id offset ⇒ member id (eq_identifier ?) globals
  | _ ⇒ True
  ].

definition translate_cst :
  ∀globals: list ident.
  ∀cst_sig: Σcst : constant.cst_well_defd globals cst.
  ∀destrs: list register.
  |destrs| = size_of_cst cst_sig → list (rtl_step globals)
 ≝
  λglobals,cst_sig,destrs,prf.
  match cst_sig return λy.cst_sig = y → list (rtl_step globals) with
  [ mk_Sig cst cst_good ⇒ λeqcst_sig.
    match cst return λx.cst = x → list (rtl_step globals)
    with
    [ Ointconst size const ⇒ λeqcst.
      match split_into_bytes size const with
      [ mk_Sig bytes bytes_length_proof ⇒
        map2 … (λr.λb : Byte.r ← (b : rtl_argument)) destrs bytes ?
      ]
    | Ofloatconst float ⇒ λ_.⊥
    | Oaddrsymbol id offset ⇒ λeqcst.
      let 〈r1, r2〉 ≝ make_addr … destrs ? in
      [ADDRESS rtl_params globals id ? r1 r2]
    | Oaddrstack offset ⇒ λeqcst.
      let 〈r1, r2〉 ≝ make_addr … destrs ? in
      [(rtl_st_ext_stack_address r1 r2 : rtl_step globals)]
    ] (refl …)
  ] (refl …).
  [2: cases not_implemented
  |3: >eqcst in cst_good; //]
  >eqcst_sig in prf;
  >eqcst whd in ⊢ (???% → ?); #prf
  [1: >bytes_length_proof
      >prf //]
  //
  qed.

  
definition translate_move :
  ∀globals.
  ∀destrs: list register.
  ∀srcrs: list rtl_argument.
  |destrs| = |srcrs| → list (rtl_step globals) ≝ 
  λglobals,destrs,srcrs,length_eq.
  map2 … (λdst,src.dst ← src) destrs srcrs length_eq.

let rec make
  (A: Type[0]) (elt: A) (n: nat) on n ≝
  match n with
  [ O ⇒ [ ]
  | S n' ⇒ elt :: make A elt n'
  ].
  
lemma make_length:
  ∀A: Type[0].
  ∀elt: A.
  ∀n: nat.
    n = length ? (make A elt n).
  #A #ELT #N
  elim N
  [ normalize %
  | #N #IH
    normalize <IH %
  ]
qed.

definition sign_mask : ∀globals.register → register → list (rtl_step globals) ≝
    (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that:
       byte in destr if srcr is: neg   |  pos
       destr ← srcr | 127       11...1 | 01...1
       destr ← destr <rot< 1    1...11 | 1...10
       destr ← INC destr        0....0 | 1....1
       destr ← CPL destr        1....1 | 0....0
     *)
  λglobals,destr,srcr.
  [destr ← srcr .Or. 127 ;
   destr ← .Rl. destr ;
   destr ← .Inc. destr ;
   destr ← .Cmpl. destr ].
   
definition translate_cast_signed :
  ∀globals : list ident.
  list register → register → bind_list register (rtl_step globals) ≝
  λglobals,destrs,srcr.
  ν tmp in
  (sign_mask ? tmp srcr @
  translate_move ? destrs (make ? (Reg tmp) (|destrs|)) (make_length …)).
 
definition translate_cast_unsigned :
  ∀globals : list ident.
  list register → list (rtl_step globals) ≝
  λglobals,destrs.
  match nat_to_args (|destrs|) 0 with
  [ mk_Sig res prf ⇒ translate_move ? destrs res ?].
  // qed.

theorem length_map : ∀A,B.∀f:A→B.∀l : list A.|map … f l| = |l|.
#A#B#f #l elim l normalize // qed.

(* using size of lists as size of ints *)
definition translate_cast :
  ∀globals: list ident.
  signedness → list register → list register →
    bind_list register (rtl_step globals) ≝
  λglobals,src_sign,destrs,srcrs.
  match srcrs
  return λy. y = srcrs → bind_list register (rtl_step globals)
  with
  [ nil ⇒ λ_.translate_cast_unsigned ? destrs (* srcrs = [ ] ⇒ we fill with 0 *)
  | _ ⇒ λeq_srcrs.
    match reduce_strong ? ? destrs srcrs with
    [ mk_Sig crl len_proof ⇒
      (* move prefix of srcrs in destrs *)
      translate_move ? (\fst (\fst crl)) (map … Reg (\fst (\snd crl))) ? @@
      match \snd (\snd crl) return λ_.bind_list ?? with
      [ nil ⇒
        match src_sign return λ_.bind_list register (rtl_step globals) with
        [ Unsigned ⇒ translate_cast_unsigned ? (\snd (\fst crl))
        | Signed ⇒
          translate_cast_signed ? (\snd (\fst crl)) (last_safe ? srcrs ?)
        ]
      | _ ⇒ [ ] (* nothing to do if |srcrs| > |destrs| *)
      ]
    ]
  ] (refl …).
  [ >len_proof >length_map @refl
  | <eq_srcrs normalize //
  ] qed.
  
definition translate_notint :
  ∀globals : list ident.
  ∀destrs : list register.
  ∀srcrs_arg : list register.
  |destrs| = |srcrs_arg| → list (rtl_step globals) ≝
  λglobals, destrs, srcrs, prf.
  map2 ??? (OP1 rtl_params globals Cmpl) destrs srcrs prf.

definition translate_negint : ∀globals.? → ? → ? → bind_list register (rtl_step globals) ≝
  λglobals: list ident.
  λdestrs: list register.
  λsrcrs: list register.
  λprf: |destrs| = |srcrs|. (* assert in caml code *)
  translate_notint … destrs srcrs prf @
  match nat_to_args (|destrs|) 1 with
  [ mk_Sig res prf' ⇒
    translate_op ? Add destrs (map … Reg destrs) res ??
  ].
// qed.

definition translate_notbool:
  ∀globals : list ident.
  list register → list register →
    bind_list register (rtl_step globals) ≝
  λglobals,destrs,srcrs.
  match destrs with
  [ nil ⇒ [ ]
  | cons destr destrs' ⇒
    translate_cast_unsigned ? destrs' @@ (* fill destrs' with 0 *)
    match srcrs with
    [ nil ⇒ [destr ← 0]
    | cons srcr srcrs' ⇒
      let f : register → rtl_step globals ≝
        λr. destr ← destr .Or. r in
      (destr ← srcr) ::: ? ]].
      map ?? f srcrs' @@
      (* now destr is non-null iff srcrs was non-null *)
      CLEAR_CARRY ? ? ::
      (* many uses of 0, better not use immediates *)
      ν tmp in
      [tmp ← 0 ;
       destr ← tmp .Sub. tmp ;
       (* now carry bit is set iff destr was non-null *)
       destr ← tmp .Addc. tmp]
     ]
   ].

definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? →
  bind_list register unit (rtl_step globals) ≝
  λglobals.
  λty, ty'.
  λop1: unary_operation ty ty'.
  λdestrs: list register.
  λsrcrs: list register.
  λprf1: |destrs| = size_of_sig_type ty'.
  λprf2: |srcrs| = size_of_sig_type ty.
  match op1
  return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' →
    bind_list register unit (rtl_step globals) with
  [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2.
    translate_cast globals src_sign destrs srcrs
  | Onegint sz sg ⇒ λeq1,eq2.
    translate_negint globals destrs srcrs ?
  | Onotbool _ _ _ _ ⇒ λeq1,eq2.
    translate_notbool globals destrs srcrs
  | Onotint sz sg ⇒ λeq1,eq2.
    translate_notint globals destrs srcrs ?
  | Optrofint sz sg r ⇒ λeq1,eq2.
    translate_cast globals Unsigned destrs srcrs
  | Ointofptr sz sg r ⇒ λeq1,eq2.
    translate_cast globals Unsigned destrs srcrs
  | Oid t ⇒ λeq1,eq2.
      translate_move globals destrs (map … Reg srcrs) ?
  | _ ⇒ λeq1,eq2.? (* float operations implemented in runtime *)
  ] (refl …) (refl …).
  [3,4,5,6,7,8,9:  cases not_implemented
  |*: destruct >prf1 >prf2 //
  ]
qed.

include alias "arithmetics/nat.ma".

let rec range_strong_internal (start : ℕ) (count : ℕ)
  (* Paolo: no notation to avoid ambiguity *)
  on count : list (Σn : ℕ.lt n (plus start count)) ≝
match count return λx.count = x → list (Σn : ℕ. n < start + count)
  with
[ O ⇒ λ_.[ ]
| S count' ⇒ λEQ.
  let f : (Σn : ℕ. lt n (S start + count')) → Σn : ℕ. lt n (start + count) ≝
    λsig.match sig with [mk_Sig n prf ⇒ n] in
  start :: map … f (range_strong_internal (S start) count')
] (refl …).
destruct(EQ) // qed.

definition range_strong : ∀end : ℕ. list (Σn.n<end) ≝
  λend.range_strong_internal 0 end.

definition translate_mul_i :
  ∀globals.
  register → register →
  (* size of destination and sources *)
  ∀n : ℕ.
  (* the temporary destination, with a dummy register at the end *)
  ∀tmp_destrs_dummy : list register.
  ∀srcrs1,srcrs2 : list rtl_argument.
  |tmp_destrs_dummy| = S n →
  n = |srcrs1| →
  |srcrs1| = |srcrs2| →
  (* the position of the least significant byte of the result we compute at
     this stage (goes from 0 to n in the main function) *)
  ∀k : ℕ.
  lt k n →
  (* the position of the byte in the first source we will use in this stage.
     the position in the other source will be k - i *)
  (Σi.i<S k) →
  (* the accumulator *)
  list (rtl_step globals) →
    list (rtl_step globals) ≝
  λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2,
    tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc.
  (* the following will expand to
     a, b ← srcrs1[i] * srcrs2[k-i]
     tmp_destrs_dummy[k]   ← tmp_destrs_dummy[k] + a
     tmp_destrs_dummy[k+1] ← tmp_destrs_dummy[k+1] + b + C
     tmp_destrs_dummy[k+2] ← tmp_destrs_dummy[k+2] + 0 + C
     ...
     tmp_destrs_dummy[n]   ← tmp_destrs_dummy[n] + 0 + C
     ( all calculations on tmp_destrs_dummy[n] will be eliminated with
     liveness analysis) *)
  match i_sig with
    [ mk_Sig i i_prf ⇒
      (* we pad the result of a byte multiplication with zeros in order
         for the bit to be carried. Redundant calculations will be eliminated
         by constant propagation. *)
      let args : list rtl_argument ≝
        [Reg a;Reg b] @ make ? (Imm (zero …)) (n - 1 - k) in
      let tmp_destrs_view : list register ≝
        ltl ? tmp_destrs_dummy k in
      ❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k - i) srcrs2 ?) ::
      translate_op … Add tmp_destrs_view (map … Reg tmp_destrs_view) args ?? @
      acc
    ].
[ @lt_plus_to_minus [ @le_S_S_to_le assumption | <srcrs2_prf <srcrs1_prf
  whd >(plus_n_O (S k)) @le_plus // ]
| <srcrs1_prf
  @(transitive_le … i_prf k_prf)
| >length_map //
| >length_map
  >length_ltl
  >tmp_destrs_dummy_prf >length_append
  <make_length
  normalize in ⊢ (???(?%?));
  >plus_minus_commutative
    [2: @le_plus_to_minus_r <plus_n_Sm <plus_n_O assumption]
  cut (S n = 2 + (n - 1))
    [2: #EQ >EQ //]
  >plus_minus_commutative
    [2: @(transitive_le … k_prf) //]
  @sym_eq
  @plus_to_minus
  <plus_n_Sm
  //
] qed.

definition translate_mul : ∀globals.?→?→?→?→?→bind_list register unit (rtl_step globals) ≝
λglobals : list ident.
λdestrs : list register.
λsrcrs1 : list rtl_argument.
λsrcrs2 : list rtl_argument.
λsrcrs1_prf : |destrs| = |srcrs1|.
λsrcrs2_prf : |srcrs1| = |srcrs2|.
(* needed fresh registers *)
νa in
νb in
(* temporary registers for the result are created, so to avoid overwriting
   sources *)
νν tmp_destrs × |destrs| with tmp_destrs_prf in
νdummy in
(* the step calculating all products with least significant byte going in the
   k-th position of the result *)
let translate_mul_k : (Σk.k<|destrs|) → list (rtl_step globals) →
  list (rtl_step globals) ≝
  λk_sig,acc.match k_sig with
  [ mk_Sig k k_prf ⇒
    foldr … (translate_mul_i ? a b (|destrs|)
      (tmp_destrs @ [dummy]) srcrs1 srcrs2
      ? srcrs1_prf srcrs2_prf k k_prf) acc (range_strong (S k))
  ] in
(* initializing tmp_destrs to zero
   dummy is intentionally uninitialized *)
translate_cast_unsigned … tmp_destrs @
(* the main body, roughly:
   for k in 0 ... n-1 do
     for i in 0 ... k do
       translate_mul_i … k … i *)
foldr … translate_mul_k [ ] (range_strong (|destrs|)) @ 
(* epilogue: saving the result *)
translate_move … destrs (map … Reg tmp_destrs) ?.
[ >length_map >tmp_destrs_prf //
| >length_append <plus_n_Sm <plus_n_O //
]
qed.

definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→
    bind_list register unit (rtl_step globals) ≝
  λglobals: list ident.
  λdiv_not_mod: bool.
  λdestrs: list register.
  λsrcrs1: list rtl_argument.
  λsrcrs2: list rtl_argument.
  λsrcrs1_prf : |destrs| = |srcrs1|.
  λsrcrs2_prf : |srcrs1| = |srcrs2|.
  let return_type ≝ bind_list register unit (rtl_step globals) in
  match destrs return λx.x = destrs → return_type with
  [ nil ⇒ λ_.[ ]
  | cons destr destrs' ⇒ λeq_destrs.
    match destrs' with
    [ nil ⇒
      match srcrs1 return λx.x = srcrs1 → return_type  with
      [ nil ⇒ λeq_srcrs1.⊥
      | cons srcr1 srcrs1' ⇒ λeq_srcrs1.
        match srcrs2 return λx.x = srcrs2 → return_type  with
        [ nil ⇒ λeq_srcrs2.⊥
        | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
          νdummy in
          let 〈destr1, destr2〉 ≝
            if div_not_mod then 〈destr, dummy〉 else 〈dummy, destr〉 in
          [❮destr1, destr2❯ ← srcr1 .DivuModu. srcr2]
        ] (refl …)
      ] (refl …)
    | _ ⇒ ? (* not implemented *)
    ]
  ] (refl …).
[3: elim not_implemented]
destruct normalize in srcrs1_prf; normalize in srcrs2_prf; destruct qed.

(* Paolo: to be moved elsewhere *)
let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (f : A→B→C→C) (init : C) (l1 : list A) (l2 : list B)
  (prf : |l1| = |l2|) on l1 : C ≝
  match l1 return λx.x = l1 → C with 
  [ nil ⇒ λ_.init
  | cons a l1' ⇒ λeq_l1.
    match l2 return λy.y = l2 → C with
    [ nil ⇒ λeq_l2.⊥
    | cons b l2' ⇒ λeq_l2.
      f a b (foldr2 A B C f init l1' l2' ?)
    ] (refl …)
  ] (refl …).
destruct normalize in prf;  [destruct|//]
qed.

definition translate_ne: ∀globals: list ident.?→?→?→?→?→bind_list register unit (rtl_step globals) ≝
  λglobals: list ident.
  λdestrs: list register.
  λsrcrs1: list rtl_argument.
  λsrcrs2: list rtl_argument.
  λsrcrs1_prf : |destrs| = |srcrs1|.
  λsrcrs2_prf : |srcrs1| = |srcrs2|.
  let return_type ≝ bind_list register unit (rtl_step globals) in
  match destrs return λx.x = destrs → return_type with
  [ nil ⇒ λ_.[ ]
  | cons destr destrs' ⇒ λeq_destrs.
    match srcrs1 return λy.y = srcrs1 → return_type with
    [ nil ⇒ λeq_srcrs1.⊥
    | cons srcr1 srcrs1' ⇒ λeq_srcrs1.
      match srcrs2 return λz.z = srcrs2 → return_type with
      [ nil ⇒ λeq_srcrs2.⊥
      | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
        νtmpr in
        let f : rtl_argument → rtl_argument → list (rtl_step globals) → list (rtl_step globals) ≝
          λs1,s2,acc.
          tmpr  ← s1 .Xor. s2 ::
          destr ← destr .Or. tmpr ::
          acc in
        let epilogue : list (rtl_step globals) ≝
          [ CLEAR_CARRY … ;
            tmpr ← 0 .Sub. destr ;
            (* now carry bit is 1 iff destrs != 0 *)
            destr ← 0 .Addc. 0 ] in
         translate_cast_unsigned … destrs' @
         destr ← srcr1 .Xor. srcr2 ::
         foldr2 ??? f epilogue srcrs1' srcrs2' ?
       ] (refl …)
     ] (refl …)
   ] (refl …).
   destruct normalize in srcrs1_prf; normalize in srcrs2_prf; destruct // qed.

(* if destrs is 0 or 1, it inverses it. To be used after operations that
   ensure this. *)
definition translate_toggle_bool : ∀globals.?→list (rtl_step globals) ≝
  λglobals: list ident.
  λdestrs: list register.
  match destrs with
  [ nil ⇒ [ ]
  | cons destr _ ⇒ [destr ← .Cmpl. destr]
  ].
  
definition translate_lt_unsigned :
  ∀globals.
  ∀destrs: list register.
  ∀srcrs1: list rtl_argument.
  ∀srcrs2: list rtl_argument.
  |destrs| = |srcrs1| →
  |srcrs1| = |srcrs2| →
  list (rtl_step globals) ≝
  λglobals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
  match destrs with
  [ nil ⇒ [ ]
  | cons destr destrs' ⇒
    translate_cast_unsigned … destrs' @
    (* I perform a subtraction, but the only interest is in the carry bit *)
    translate_op ? Sub (make … destr (|destrs|)) srcrs1 srcrs2 ?? @
    [ destr ← 0 .Addc. 0 ]
  ].
[ <make_length ] assumption qed.

(* shifts signed integers by adding 128 to the most significant byte
   it replaces it with a fresh register which must be provided *)
let rec shift_signed globals
  (tmp : register)
  (srcrs : list rtl_argument) on srcrs :
  (list rtl_argument) × (list (rtl_step globals)) ≝
  match srcrs with
  [ nil ⇒ 〈[ ],[ ]〉
  | cons srcr srcrs' ⇒
    match srcrs' with
    [ nil ⇒ 〈[ Reg tmp ], [ tmp ← srcr .Add. 128 ]〉
    | _ ⇒
      let 〈new_srcrs', op〉 ≝ shift_signed globals tmp srcrs' in
      〈srcr :: new_srcrs', op〉
    ]
  ].

lemma shift_signed_length : ∀globals,tmp,srcrs.
  |\fst (shift_signed globals tmp srcrs)| = |srcrs|.
#globals #tmp #srcrs elim srcrs [//]
#srcr * [//]
#srcr' #srcrs'' #Hi
whd in ⊢ (??(??(???%))?);
@pair_elim #new_srcrs' #op #EQ >EQ in Hi;
normalize #Hi >Hi //
qed.

definition translate_lt_signed :
  ∀globals.
  ∀destrs: list register.
  ∀srcrs1: list rtl_argument.
  ∀srcrs2: list rtl_argument.
  |destrs| = |srcrs1| →
  |srcrs1| = |srcrs2| →
  bind_list register unit (rtl_step globals) ≝
  λglobals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
  νtmp_last_s1 in
  νtmp_last_s2 in
  let p1 ≝ shift_signed globals tmp_last_s1 srcrs1 in
  let new_srcrs1 ≝ \fst p1 in
  let shift_srcrs1 ≝ \snd p1 in
  let p2 ≝ shift_signed globals tmp_last_s2 srcrs2 in
  let new_srcrs2 ≝ \fst p2 in
  let shift_srcrs2 ≝ \snd p2 in
  shift_srcrs1 @ shift_srcrs2 @
  translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2 ??.
>shift_signed_length [2: >shift_signed_length] assumption qed.

definition translate_lt : bool→∀globals.?→?→?→?→?→bind_list register unit (rtl_step globals) ≝
  λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
  if is_unsigned then
    translate_lt_unsigned globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  else
    translate_lt_signed globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf.

definition translate_cmp ≝
  λis_unsigned,globals,cmp,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
  match cmp with
  [ Ceq ⇒
    translate_ne globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf @
    translate_toggle_bool globals destrs
  | Cne ⇒
    translate_ne globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  | Clt ⇒
    translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  | Cgt ⇒
    translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? ?
  | Cle ⇒
    translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? ? @
    translate_toggle_bool globals destrs
  | Cge ⇒
    translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf @
    translate_toggle_bool globals destrs
  ].
// qed.
  
definition translate_op2 :
  ∀globals.?→?→?→?→?→?→bind_list register unit (rtl_step globals) ≝
  λglobals: list ident.
  λop2.
  λdestrs: list register.
  λsrcrs1: list rtl_argument.
  λsrcrs2: list rtl_argument.
  λsrcrs1_prf: |destrs| = |srcrs1|.
  λsrcrs2_prf: |srcrs1| = |srcrs2|.
  match op2 with
  [ Oadd ⇒
    translate_op globals Add destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  | Oaddp ⇒
    translate_op globals Add destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  | Osub ⇒
    translate_op globals Sub destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  | Osubpi ⇒
    translate_op globals Sub destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  | Osubpp _ ⇒
    translate_op globals Sub destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  | Omul ⇒
    translate_mul globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  | Odivu ⇒
    translate_divumodu8 globals true destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  | Omodu ⇒
    translate_divumodu8 globals false destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  | Oand ⇒
    translate_op globals And destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  | Oor ⇒
    translate_op globals Or destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  | Oxor ⇒
    translate_op globals Xor destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  | Ocmp c ⇒
    translate_cmp false globals c destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  | Ocmpu c ⇒
    translate_cmp true globals c destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  | Ocmpp c ⇒
    translate_cmp true globals c destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
  | _ ⇒ ? (* assert false, implemented in run time or float op *)
  ].
  cases not_implemented (* XXX: yes, really *) qed.

definition translate_cond: ∀globals: list ident. list register → label → bind_list register unit (rtl_step globals) ≝
  λglobals: list ident.
  λsrcrs: list register.
  λlbl_true: label.
  match srcrs with
  [ nil ⇒ [ ]
  | cons srcr srcrs' ⇒
    ν tmpr in
    let f : register → rtl_step globals ≝
      λr. tmpr ← tmpr .Or. r in 
    MOVE rtl_params globals 〈tmpr,srcr〉 ::
    map … f srcrs' @
    [ COND ?? tmpr lbl_true ]
  ].

(* Paolo: to be controlled (original seemed overly complex) *)
definition translate_load ≝
  λglobals: list ident.
  λaddr : list rtl_argument.
  λaddr_prf: 2 = |addr|.
  λdestrs: list register.
  ν tmp_addr_l in
  ν tmp_addr_h in
  let f ≝ λdestr : register.λacc : list (rtl_step globals).
    LOAD rtl_params globals destr (Reg tmp_addr_l) (Reg tmp_addr_h) ::
    translate_op … Add
      [tmp_addr_l ; tmp_addr_h]
      [Reg tmp_addr_l ; Reg tmp_addr_h]
      [imm_nat 0 ; Imm int_size] ? ? @ acc in
  translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @
  foldr … f [ ] destrs.
[1: <addr_prf] // qed.
  
definition translate_store ≝
  λglobals: list ident.
  λaddr : list rtl_argument.
  λaddr_prf: 2 = |addr|.
  λsrcrs: list rtl_argument.
  ν tmp_addr_l in
  ν tmp_addr_h in
  let f ≝ λsrcr : rtl_argument.λacc : list (rtl_step globals).
    STORE rtl_params globals (Reg tmp_addr_l) (Reg tmp_addr_h) srcr ::
    translate_op … Add
      [tmp_addr_l ; tmp_addr_h]
      [Reg tmp_addr_l ; Reg tmp_addr_h]
      [imm_nat 0 ; Imm int_size] ? ? @ acc in
  translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @
  foldr … f [ ] srcrs.
[1: <addr_prf] // qed.

(* alias for b_adds_graph *)
definition rtl_adds_graph ≝
  λglobals.b_adds_graph rtl_params globals register unit
    (rtl_ertl_fresh_reg rtl_params rtl_params globals).

axiom fake_label: label.

definition stmt_not_final ≝ λstmt.match stmt with
  [ St_return ⇒ False
  | St_tailcall_id _ _ ⇒ False
  | St_tailcall_ptr _ _ ⇒ False
  | _ ⇒ True ].

definition translate_inst : ∀globals.?→?→?→
  (bind_list register unit (rtl_step globals)) × label ≝
  λglobals: list ident.
  λlenv: local_env.
  λstmt.
  λstmt_typed : 
  λstmt_prf : stmt_not_final stmt.
  match stmt return λx.stmt = x →
    (bind_list register unit (rtl_step globals)) × label with
  [ St_skip lbl' ⇒ λ_.
    〈[ ], lbl'〉
  | St_cost cost_lbl lbl' ⇒ λ_.
    〈[COST_LABEL … cost_lbl], lbl'〉
  | St_const destr cst lbl' ⇒ λ_.
    〈translate_cst globals cst (find_local_env destr lenv) ?, lbl'〉
  | St_op1 ty ty' op1 destr srcr lbl' ⇒ λ_.
    〈translate_op1 globals ty' ty op1
      (find_local_env destr lenv)
      (find_local_env srcr lenv) ??, lbl'〉
  | St_op2 op2 destr srcr1 srcr2 lbl' ⇒ λ_.
    〈translate_op2 globals op2
      (find_local_env destr lenv)
      (find_local_env_arg srcr1 lenv)
      (find_local_env_arg srcr2 lenv) ??, lbl'〉
    (* XXX: should we be ignoring this? *)
  | St_load ignore addr destr lbl' ⇒ λ_.
    〈translate_load globals
      (find_local_env_arg addr lenv) ? (find_local_env destr lenv), lbl'〉
    (* XXX: should we be ignoring this? *)
  | St_store ignore addr srcr lbl' ⇒ λ_.
    〈translate_store globals (find_local_env_arg addr lenv) ?
      (find_local_env_arg srcr lenv), lbl'〉
  | St_call_id f args retr lbl' ⇒ λ_.
    (* Paolo: no notation to avoid ambiguity *)
    〈bcons … (
      match retr with
      [ Some retr ⇒
        CALL_ID rtl_params globals f (rtl_args args lenv) (find_local_env retr lenv)
      | None ⇒
        CALL_ID … f (rtl_args args lenv) [ ]
      ]) [ ], lbl'〉
  | St_call_ptr f args retr lbl' ⇒ λ_.
    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    (* Paolo: no notation to avoid ambiguity *)
    〈bcons … (
      match retr return λ_.rtl_step globals with
      [ Some retr ⇒
        rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv)
      | None ⇒
        rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ]
      ]) [ ], lbl'〉
  | St_cond r lbl_true lbl_false ⇒ λ_.
    〈translate_cond globals (find_local_env r lenv) lbl_true, lbl_false〉
  | St_jumptable r l ⇒  λ_.? (* assert false: not implemented yet *)
  | _ ⇒ λeq_stmt.⊥
  ] (refl …).
  [12: cases not_implemented (* jtable case *)
  |10,11,13: >eq_stmt in stmt_prf; normalize //
  |*: cases daemon
  (* TODO: proofs regarding lengths of lists, examine! *)
  (* Paolo: probably hypotheses need to be added *)
  ]
qed.

definition translate_stmt ≝
  λglobals,lenv,lbl,stmt,def.
  match stmt return λx.stmt = x → rtl_internal_function globals with
  [ St_return ⇒ λ_.add_graph rtl_params globals lbl (RETURN …) def
  | St_tailcall_id f args ⇒ λ_.
    add_graph rtl_params globals lbl
      (extension_fin … (rtl_st_ext_tailcall_id f (rtl_args args lenv))) def
  | St_tailcall_ptr f args ⇒ λ_.
    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    add_graph rtl_params globals lbl
      (extension_fin … (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) def
  | _ ⇒ λstmt_eq.
    let 〈translation, lbl'〉 ≝ translate_inst globals lenv stmt ? in
    rtl_adds_graph globals translation lbl lbl' def
  ] (refl …).
[10: cases daemon (* length of address lookup *)
|*: >stmt_eq normalize %] qed.
  
  
(* XXX: we use a "hack" here to circumvent the proof obligations required to
   create res, an empty internal_function record.  we insert into our graph
   the start and end nodes to ensure that they are in, and place dummy
   skip instructions at these nodes. *)
definition translate_internal ≝
  λglobals: list ident.
  λdef.
  let runiverse ≝ f_reggen def in
  let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
    (f_params def @ f_locals def) (f_result def) in
  let parameters ≝ map_list_local_env lenv (map … \fst (f_params def)) in
  let locals ≝ map_list_local_env lenv (map … \fst (f_locals def)) in
  let result ≝
    match (f_result def) with
    [ None ⇒ [ ]
    | Some r_typ ⇒
      let 〈r, typ〉 ≝ r_typ in
        find_local_env r lenv
    ]
  in
  let luniverse' ≝ f_labgen def in
  let runiverse' ≝ runiverse in
  let result' ≝ result in
  let params' ≝ parameters in
  let locals' ≝ locals in
  let stack_size' ≝ f_stacksize def in
  let entry' ≝ f_entry def in
  let exit' ≝ f_exit def in
  let graph' ≝ empty_map LabelTag ? in
  let graph' ≝ add LabelTag ? graph' entry'
    (GOTO … exit') in 
  let graph' ≝ add LabelTag ? graph' exit'
    (RETURN …) in
  let res ≝
    mk_joint_internal_function globals rtl_params luniverse' runiverse' result' params'
     locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in
    foldi … (translate_stmt globals … lenv) (f_graph def) res.
[ @graph_add_lookup ] @graph_add
qed.

(*CSC: here we are not doing any alignment on variables, like it is done in OCaml
  because of CompCert heritage *)
definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
 λp. transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).