source: src/RTLabs/RTLabsToRTL.ma @ 1354

include "RTLabs/syntax.ma".
include "RTL/RTL.ma".
include "common/AssocList.ma".
include "common/FrontEndOps.ma".
include "common/Graphs.ma".
include "joint/TranslateUtils.ma".
include alias "ASM/BitVector.ma".
include alias "arithmetics/nat.ma".

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 complete_regs ≝
  λglobals.
  λdef.
  λsrcrs1.
  λsrcrs2.
  if leb (length … srcrs2) (length … srcrs1) then
   let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs1) (length ? srcrs2)) in
    〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉
  else
   let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs2) (length ? srcrs1)) in
    〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.

lemma complete_regs_length:
  ∀globals,def,left,right.
   |\fst (\fst (complete_regs globals def left right))| = |\snd (\fst (complete_regs globals def left right))|.
 #globals #def #left #right
 whd in match complete_regs normalize nodelta
 @leb_elim normalize nodelta #H
 [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right)))
 | generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)))]
 cases (fresh_regs ????) #def' #fresh normalize >append_length
 generalize in match H -H;
 generalize in match (length … left) generalize in match (length … right) generalize in match (length … fresh)
 [ /2/ | #x #y #z #H generalize in match (not_le_to_lt … H) -H #H #E >E >commutative_plus
         <plus_minus_m_m /2/ ]
qed.

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 ≝ BitVectorTrie (list register) 16.

definition mem_local_env : register → local_env → bool ≝
  λr. member … (word_of_identifier … r).

definition add_local_env : register → list register → local_env → local_env ≝
  λr. insert … (word_of_identifier … r).

definition find_local_env : register → local_env → list register ≝
  λr: register.λbvt. lookup … (word_of_identifier … r) bvt [].

definition initialize_local_env_internal ≝
  λlenv_runiverse.
  λ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_local_env r rs lenv,runiverse〉.

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

definition map_list_local_env_internal ≝
  λlenv,res,r. res @ (find_local_env r lenv).
    
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. make_addr ? (find_local_env r lenv).

definition rtl_args ≝
  λregs_list,lenv. flatten … (map … (λr. find_local_env r lenv) regs_list).

definition translate_cst_int_internal ≝
  λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl.

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〉 ≝ split ? 8 … int in [l;h])] cases (split ????) //
| %[@(let 〈h1,l〉 ≝ split ? 8 … int in
      let 〈h2,l〉 ≝ split ? 8 … l in
      let 〈h3,l〉 ≝ split ? 8 … l in
       [l;h3;h2;h1])]
  cases (split ????) #h1 #l normalize
  cases (split ????) #h2 #l normalize
  cases (split ????) // ]
qed.

lemma eqb_implies_eq:
  ∀m, n: nat.
    eqb m n = true → m = n.
  #M
  elim M
  [1: #N normalize
      cases N
      [1: normalize //
      |2: #M' normalize #HYP destruct(HYP)
      ]
  |2: #M' #IND_HYP #N
      normalize
      cases N
      [1: normalize #HYP destruct(HYP)
      |2: #M'' normalize #HYP
          @eq_f @(IND_HYP M'')
          assumption
      ]
   ]
qed.

definition translate_op: ∀globals. ? → list register → list register → list register →
  label → label → rtl_internal_function globals → rtl_internal_function globals ≝
  λglobals: list ident.
  λop.
  λdestrs: list register.
  λsrcrs1: list register.
  λsrcrs2: list register.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef: rtl_internal_function globals.
  match reduce_strong register register srcrs1 srcrs2 with
  [ dp reduced first_reduced_proof ⇒
    let srcrsl_common ≝ \fst (\fst reduced) in
    let srcrsr_common ≝ \fst (\snd reduced) in
    let srcrsl_rest ≝ \snd (\fst reduced) in
    let srcrsr_rest ≝ \snd (\snd reduced) in
    let srcrs_rest ≝ srcrsl_rest @ srcrsr_rest in
    match reduce_strong register register destrs srcrsl_common with
    [ dp reduced second_reduced_proof ⇒
      let destrs_common ≝ \fst (\fst reduced) in
      let destrs_rest ≝ \snd (\fst reduced) in
      match reduce_strong register register destrs_rest srcrs_rest with
      [ dp reduced third_reduced_proof ⇒
        let destrs_cted ≝ \fst (\fst reduced) in
        let destrs_rest ≝ \snd (\fst reduced) in
        let srcrs_cted ≝ \fst (\snd reduced) in
        let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
        let insts_init ≝ [
          sequential … (CLEAR_CARRY …);
          sequential … (INT rtl_params_ globals tmpr (zero …))
        ] in
        let f_add ≝ λdestr. λsrcr1. λsrcr2. sequential … (OP2 rtl_params_ globals op destr srcr1 srcr2) in
        let insts_add ≝ map3 ? ? ? ? f_add destrs_common srcrsl_common srcrsr_common ? ? in
        let f_add_cted ≝ λdestr. λsrcr. sequential … (OP2 rtl_params_ globals op destr srcr tmpr) in
        let insts_add_cted ≝ map2 … f_add_cted destrs_cted srcrs_cted ? in
        let f_rest ≝ λdestr. sequential … (OP2 rtl_params_ globals op destr tmpr tmpr) in
        let insts_rest ≝ map … f_rest destrs_rest in
          adds_graph rtl_params1 globals (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def
      ]
    ]
  ].
  [1: @third_reduced_proof
  |3: @first_reduced_proof
  |*: cases daemon (* XXX: some of these look like they may be false *)
  ]
qed.

let rec translate_cst
  (globals: list ident) (cst: constant) (destrs: list register)
    (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function globals)
      on cst: rtl_internal_function globals ≝
  match cst with
  [ Ointconst size const ⇒
    match destrs with
    [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
    | _   ⇒
      let size' ≝ size_intsize size in
        match eqb size' (|destrs|) return λx. (eqb size' (|destrs|)) = x → rtl_internal_function globals with
        [ true  ⇒ λgood_case.
          match split_into_bytes size const with
          [ dp bytes bytes_length_proof ⇒
            let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in
              adds_graph rtl_params1 globals mapped start_lbl dest_lbl def
          ]
        | false ⇒ λbad_case. ?
        ] (refl … (eqb size' (|destrs|)))
    ]
  | Ofloatconst float ⇒ ⊥
  | Oaddrsymbol id offset ⇒
    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (ADDRESS rtl_params_ globals id ? r1 r2) dest_lbl) def in
    let def ≝ translate_op globals Addc [r1] [r1] [r2] start_lbl dest_lbl def in
      def
  | Oaddrstack offset ⇒
    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (extension rtl_params_ globals (rtl_st_ext_stack_address r1 r2)) dest_lbl) def in
    let def ≝ translate_op globals Addc [r1] [r1] [r2] start_lbl dest_lbl def in
      def
  ].
  [1: >bytes_length_proof
      cut(size' = |destrs|)
      [1: @eqb_implies_eq
          assumption
      |2: #EQ_HYP
          <EQ_HYP %
      ]
  |2: cases daemon (* XXX: bad case where destrs is of the wrong length *)
  |3: cases not_implemented (* XXX: float, error_float in o'caml *)
  |*: cases daemon (* XXX: various proofs to be filled in *)
  ].
qed.
  
definition translate_move_internal ≝
  λglobals.
  λdestr: register.
  λsrcr: register.
    sequential rtl_params_ globals (MOVE … 〈destr,srcr〉).

definition translate_move ≝
  λglobals.
  λdestrs: list register.
  λsrcrs: list register.
  λstart_lbl: label.
    match reduce_strong register register destrs srcrs with
    [ dp crl_crr len_proof ⇒
      let commonl ≝ \fst (\fst crl_crr) in
      let commonr ≝ \fst (\snd crl_crr) in
      let restl ≝ \snd (\fst crl_crr) in
      let restr ≝ \snd (\snd crl_crr) in
      let f_common ≝ translate_move_internal globals in
      let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in
      let translate2 ≝ translate_cst … (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
        add_translates … [ translate1 ; translate2 ] start_lbl
    ].
    @len_proof
qed.

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 translate_cast_unsigned ≝
  λglobals.
  λdestrs.
  λstart_lbl.
  λdest_lbl.
  λdef: joint_internal_function … (rtl_params globals).
  let 〈def, tmp_zero〉 ≝ fresh_reg … def in
  let zeros ≝ make … tmp_zero (length … destrs) in
    add_translates … [
      adds_graph rtl_params1 … [
        sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0))
        ];
      translate_move globals destrs zeros
    ] start_lbl dest_lbl def.

definition translate_cast_signed:
    ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
  λglobals: list ident.
  λdestrs.
  λsrcr.
  λstart_lbl.
  λdest_lbl.
  λdef.
  let 〈def, tmp_128〉 ≝ fresh_reg … def in
  let 〈def, tmp_255〉 ≝ fresh_reg … def in
  let 〈def, tmpr〉 ≝ fresh_reg … def in
  let 〈def, dummy〉 ≝ fresh_reg … def in
  let insts ≝ [
    sequential  … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128));
    sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr);
    sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128);
    sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255));
    sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255)
  ]
  in
  let srcrs ≝ make … tmpr (length … destrs) in
    add_translates rtl_params1 globals [
      adds_graph rtl_params1 globals insts;
      translate_move globals destrs srcrs
    ] start_lbl dest_lbl def.

definition translate_cast ≝
  λglobals: list ident.
  λsrc_size: nat.
  λsrc_sign: signedness.
  λdest_size: nat.
  λdestrs: list register.
  λsrcrs: list register.
  match |srcrs| return λx. |srcrs| = x → ? with
  [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ]
  | S n' ⇒ λsucc_prf.
    if ltb dest_size src_size then
      translate_move globals destrs srcrs
    else
      match reduce_strong register register destrs srcrs with
      [ dp crl len_proof ⇒
        let commonl ≝ \fst (\fst crl) in
        let commonr ≝ \fst (\snd crl) in
        let restl ≝ \snd (\fst crl) in
        let restr ≝ \snd (\snd crl) in
        let insts_common ≝ translate_move globals commonl commonr in
        let sign_reg ≝ last_safe ? srcrs ? in
        let insts_sign ≝
          match src_sign with
          [ Unsigned ⇒ translate_cast_unsigned globals restl
          | Signed ⇒ translate_cast_signed globals restl sign_reg
          ]
        in
          add_translates rtl_params1 globals [ insts_common; insts_sign ]
      ]
  ] (refl ? (|srcrs|)).
  >succ_prf //
qed.

definition translate_negint ≝
  λglobals: list ident.
  λdestrs: list register.
  λsrcrs: list register.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef: rtl_internal_function globals.
  λprf: |destrs| = |srcrs|. (* assert in caml code *)
  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
  let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in
  let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in
  let insts_init ≝ [
    sequential … (SET_CARRY …);
    sequential … (INT rtl_params_ globals tmpr (zero ?))
  ] in
  let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in
  let insts_add ≝ map … f_add destrs in
    adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.

definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
  λglobals: list ident.
  λdestrs: list register.
  λsrcrs: list register.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef: rtl_internal_function globals.
  match destrs with
  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def
  | cons destr destrs ⇒
    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in
    let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in
    let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in
    let f ≝ λtmp_srcr. [
      sequential … (CLEAR_CARRY rtl_params_ globals);
      sequential … (INT rtl_params_ globals tmpr (zero ?));
      sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr);
      sequential … (INT rtl_params_ globals tmpr (zero ?));
      sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr);
      sequential … (OP2 rtl_params_ globals Xor destr destr tmpr)
    ] in
    let insts ≝ init_destr :: (flatten … (map … f tmp_srcrs)) in
    let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
      add_translates rtl_params1 globals [
        save_srcrs; adds_graph rtl_params1 globals insts; epilogue
      ] start_lbl dest_lbl def
  ].

(* TODO: examine this properly.  This is a change from the O'caml code due
   to us dropping the explicit use of a cast destination size field.  We
   instead infer the size of the cast's destination from the context.  Is
   this correct?
*)
definition translate_op1 ≝
  λglobals: list ident.
  λop1: unary_operation.
  λdestrs: list register.
  λsrcrs: list register.
  λprf: |destrs| = |srcrs|.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef: rtl_internal_function globals.
  match op1 with
  [ Ocastint src_sign src_size ⇒
    let dest_size ≝ |destrs| * 8 in
    let src_size ≝ bitsize_of_intsize src_size in
      translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
  | Onegint ⇒
      translate_negint globals destrs srcrs start_lbl dest_lbl def prf
  | Onotbool ⇒
      translate_notbool globals destrs srcrs start_lbl dest_lbl def
  | Onotint ⇒
    let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in
    let l ≝ map2 … f destrs srcrs prf in
      adds_graph rtl_params1 globals l start_lbl dest_lbl def
  | Optrofint r ⇒
      translate_move globals destrs srcrs start_lbl dest_lbl def
  | Ointofptr r ⇒
      translate_move globals destrs srcrs start_lbl dest_lbl def
  | Oid ⇒
      translate_move globals destrs srcrs start_lbl dest_lbl def
  | _ ⇒ ? (* float operations implemented in runtime *)
  ].
  cases not_implemented
qed.

let rec translate_mul1
  (globals: list ident) (dummy: register) (tmpr: register)
    (destrs: list register) (srcrs1: list register) (srcr2: register)
      (start_lbl: label)
        on srcrs1 ≝
  match destrs with
  [ nil ⇒ adds_graph rtl_params1 globals [ GOTO … ] start_lbl
  | cons destr tl ⇒
    match tl with
    [ nil ⇒
      match srcrs1 with
      [ nil ⇒
        adds_graph rtl_params1 globals [
          sequential … (INT rtl_params_ globals tmpr (zero …));
          sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
        ] start_lbl
      | cons srcr1 tl' ⇒
        adds_graph rtl_params1 globals [
          sequential … (OPACCS rtl_params_ globals Mul tmpr dummy srcr2 srcr1);
          sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
        ] start_lbl
      ]
    | cons destr2 destrs ⇒
      match srcrs1 with
      [ nil ⇒
        add_translates rtl_params1 globals [
          adds_graph rtl_params1 globals [
            sequential … (INT rtl_params_ globals tmpr (zero …));
            sequential … (OP2 rtl_params_ globals Addc destr destr tmpr);
            sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr)
          ];
          translate_cst globals (Ointconst I8 (zero …)) destrs
        ] start_lbl
      | cons srcr1 srcrs1 ⇒
        match destrs with
        [ nil ⇒
          add_translates rtl_params1 globals [
            adds_graph rtl_params1 globals [
              sequential … (INT rtl_params_ globals tmpr (zero …));
              sequential … (OP2 rtl_params_ globals Addc destr destr tmpr);
              sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr)
            ];
            translate_cst globals (Ointconst I8 (zero ?)) destrs
          ] start_lbl
        | cons destr2 destrs ⇒
          add_translates rtl_params1 globals [
            adds_graph rtl_params1 globals [
              sequential … (OPACCS rtl_params_ globals Mul tmpr destr2 srcr2 srcr1);
              sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
            ];
            translate_mul1 globals dummy tmpr (destr2 :: destrs) srcrs1 srcr2
          ] start_lbl
        ]
      ]
    ]
  ].

definition translate_muli ≝
  λglobals: list ident.
  λdummy: register.
  λtmpr: register.
  λdestrs: list register.
  λtmp_destrs: list register.
  λsrcrs1: list register.
  λdummy_lbl: label.
  λi: nat.
  λi_prf: i ≤ |tmp_destrs|.
  λtranslates: list ?.
  λsrcr2i: register.
  let 〈tmp_destrs1, tmp_destrs2〉 ≝ split … tmp_destrs i i_prf in
  let tmp_destrs2' ≝
    match tmp_destrs2 with
    [ nil ⇒ [ ]
    | cons tmp_destr2 tmp_destrs2 ⇒ [
        adds_graph rtl_params1 globals [
          sequential rtl_params_ globals (CLEAR_CARRY …);
          sequential … (INT rtl_params_ globals tmp_destr2 (zero …))
        ];
        translate_mul1 globals dummy tmpr tmp_destrs2 srcrs1 srcr2i;
        translate_cst globals (Ointconst I8 (zero …)) tmp_destrs1;
        adds_graph rtl_params1 globals [
          sequential rtl_params_ globals (CLEAR_CARRY …)
        ];
        translate_op globals Addc destrs destrs tmp_destrs
      ]
    ]
  in
    translates @ tmp_destrs2'.
  
axiom foldi_strong:
  ∀a: Type[0].
  ∀b: Type[0].
  ∀the_list: list b.
  ∀f: (∀i: nat. ∀proof: i ≤ |the_list|. a → b → a).
  ∀seed: a.
    a.
  
definition translate_mul ≝
  λglobals: list ident.
  λdestrs: list register.
  λsrcrs1: list register.
  λsrcrs2: list register.
  λregs_proof: |destrs| = |srcrs2|.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef: rtl_internal_function globals.
  let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    match fresh_regs_strong rtl_params0 globals def (|destrs|) with
    [ dp def_tmp_destrs tmp_destrs_prf ⇒
      let def ≝ \fst def_tmp_destrs in
      let tmp_destrs ≝ \snd def_tmp_destrs in
      let 〈def, fresh_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
      let 〈def, fresh_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
      let insts_init ≝ [
        translate_move globals fresh_srcrs1 srcrs1;
        translate_move globals fresh_srcrs2 srcrs2;
        translate_cst globals (Ointconst I8 (zero …)) destrs
      ]
      in
        let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
        let f' ≝ λi. λi_proof: i ≤ |srcrs2|. f i ? in
        let insts_mul ≝ foldi_strong … srcrs2 f' [ ] in
          add_translates rtl_params1 globals (insts_init @ insts_mul) start_lbl dest_lbl def
    ].
  >tmp_destrs_prf
  >regs_proof
  assumption
qed.

definition translate_divumodu8 ≝
  λglobals: list ident.
  λorder: bool.
  λdestrs: list register.
  λsrcr1: register.
  λsrcr2: register.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef: rtl_internal_function globals.
  match destrs with
  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
  | cons destr destrs ⇒
    let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
    let 〈destr1, destr2〉 ≝ match order with [ true ⇒ 〈destr, dummy〉 | _ ⇒ 〈dummy, destr〉 ] in
    let inst_div ≝ adds_graph rtl_params1 globals [
      sequential rtl_params_ globals (OPACCS … DivuModu destr1 destr2 srcr1 srcr2)
    ]
    in
    let insts_rest ≝ translate_cst globals (Ointconst I8 (zero ?)) destrs in
      add_translates rtl_params1 globals [ inst_div; insts_rest ] start_lbl dest_lbl def
  ].

definition translate_ne: ∀globals: list ident. ? → ? → ? → ? → ? → ? → rtl_internal_function globals ≝
  λglobals: list ident.
  λdestrs: list register.
  λsrcrs1: list register.
  λsrcrs2: list register.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef: rtl_internal_function globals.
  match destrs with
  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
  | cons destr destrs ⇒
    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params0 globals def in
    let 〈def, tmp_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
    let save_srcrs1 ≝ translate_move globals tmp_srcrs1 srcrs1 in
    let 〈def, tmp_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
    let save_srcrs2 ≝ translate_move globals tmp_srcrs2 srcrs2 in
    match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with
    [ dp crl their_proof ⇒
      let commonl ≝ \fst (\fst crl) in
      let commonr ≝ \fst (\snd crl) in
      let restl ≝ \snd (\snd crl) in
      let restr ≝ \snd (\snd crl) in
      let rest ≝ restl @ restr in
      let inits ≝ [
        sequential … (INT rtl_params_ globals destr (zero …));
        sequential … (INT rtl_params_ globals tmp_zero (zero …))
      ]
      in
      let f_common ≝ λtmp_srcr1. λtmp_srcr2. [
        sequential … (CLEAR_CARRY …);
        sequential … (OP2 rtl_params_ globals Sub tmpr tmp_srcr1 tmp_srcr2);
        sequential … (OP2 rtl_params_ globals Or destr destr tmpr)
      ]
      in
      let insts_common ≝ flatten … (map2 … f_common commonl commonr ?) in
      let f_rest ≝ λtmp_srcr. [
        sequential … (CLEAR_CARRY …);
        sequential … (OP2 rtl_params_ globals Sub tmpr tmp_zero tmp_srcr);
        sequential … (OP2 rtl_params_ globals Or destr destr tmpr)
      ]
      in
      let insts_rest ≝ flatten … (map … f_rest rest) in
      let insts ≝ inits @ insts_common @ insts_rest in
      let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
        add_translates rtl_params1 globals [
          save_srcrs1; save_srcrs2; adds_graph rtl_params1 globals insts; epilogue
        ] start_lbl dest_lbl def
    ]
  ].
  @their_proof
qed.

definition translate_eq_reg ≝
  λglobals: list ident.
  λtmp_zero: register.
  λtmp_one: register.
  λtmpr1: register.
  λtmpr2: register.
  λdestr: register.
  λdummy_lbl: label.
  λsrcr12: register × register.
  let 〈srcr1, srcr2〉 ≝ srcr12 in
  [ sequential … (CLEAR_CARRY …);
    sequential rtl_params_ globals (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2);
    sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero);
    sequential … (OP2 rtl_params_ globals Sub tmpr2 srcr2 srcr1);
    sequential … (OP2 rtl_params_ globals Addc tmpr2 tmp_zero tmp_zero);
    sequential … (OP2 rtl_params_ globals Or tmpr1 tmpr1 tmpr2);
    sequential … (OP2 rtl_params_ globals Xor tmpr1 tmpr1 tmp_one);
    sequential … (OP2 rtl_params_ globals And destr destr tmpr1) ].

definition translate_eq_list ≝
  λglobals: list ident.
  λtmp_zero: register.
  λtmp_one: register.
  λtmpr1: register.
  λtmpr2: register.
  λdestr: register.
  λleq: list (register × register).
  λdummy_lbl: label.
  let f ≝ translate_eq_reg globals tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
    (sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1))) ::
      flatten … (map … f leq).

definition translate_atom ≝
  λglobals: list ident.
  λtmp_zero: register.
  λtmp_one: register.
  λtmpr1: register.
  λtmpr2: register.
  λtmpr3: register.
  λdestr: register.
  λdummy_lbl: label.
  λleq: list (register × register).
  λsrcr1: register.
  λsrcr2: register.
    translate_eq_list globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @
    [ sequential … (CLEAR_CARRY …);
      sequential … (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2);
      sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero);
      sequential … (OP2 rtl_params_ globals And tmpr3 tmpr3 tmpr1);
      sequential … (OP2 rtl_params_ globals Or destr destr tmpr3) ].

definition translate_lt_main ≝
  λglobals: list ident.
  λtmp_zero: register.
  λtmp_one: register.
  λtmpr1: register.
  λtmpr2: register.
  λtmpr3: register.
  λdestr: register.
  λdummy_lbl: label.
  λsrcrs1: list register.
  λsrcrs2: list register.
  λproof: |srcrs1| = |srcrs2|.
  let f ≝ λinsts_leq. λsrcr1. λsrcr2.
    let 〈insts, leq〉 ≝ insts_leq in
    let added_insts ≝ translate_atom globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in
      〈insts @ added_insts, leq @ [〈srcr1, srcr2〉]〉
  in
    \fst (fold_left2 … f 〈[ ], [ ]〉 srcrs1 srcrs2 proof).

definition fresh_regs_strong:
  ∀globals. rtl_internal_function globals → ∀n: nat. Σfresh: (rtl_internal_function globals) × (list register). |\snd fresh| = n ≝
  λglobals: list ident.
  λdef.
  λn.
    fresh_regs rtl_params0 globals def n.
  @fresh_regs_length
qed.

definition complete_regs_strong:
  ∀globals: list ident. rtl_internal_function globals → list register → list register → Σcomplete: (list register) × (list register) × (list register). |\fst (\fst complete)| = |\snd (\fst complete)| ≝
  λglobals: list ident.
  λdef.
  λleft.
  λright.
    complete_regs globals def left right.
  @complete_regs_length
qed.

definition translate_lt ≝
  λglobals: list ident.
  λdestrs: list register.
  λprf_destrs: 0 < |destrs|.
  λsrcrs1: list register.
  λsrcrs2: list register.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef: rtl_internal_function globals.
  match destrs with
  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
  | _ ⇒
    match fresh_regs_strong globals def (|destrs|) with
    [ dp def_tmp_destrs tmp_destrs_proof ⇒
      let def ≝ \fst def_tmp_destrs in
      let tmp_destrs ≝ \snd def_tmp_destrs in
      let tmp_destr ≝ hd_safe ? tmp_destrs ? in
      let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params1 globals def in
      let 〈def, tmp_one〉 ≝ fresh_reg rtl_params1 globals def in
      let 〈def, tmpr1〉 ≝ fresh_reg rtl_params1 globals def in
      let 〈def, tmpr2〉 ≝ fresh_reg rtl_params1 globals def in
      let 〈def, tmpr3〉 ≝ fresh_reg rtl_params1 globals def in
      match complete_regs_strong globals def srcrs1 srcrs2 with
      [ dp srcrs12_added srcrs12_proof ⇒
        let srcrs1 ≝ \fst (\fst srcrs12_added) in
        let srcrs2 ≝ \snd (\fst srcrs12_added) in
        let added ≝ \snd srcrs12_added in
        let srcrs1' ≝ rev … srcrs1 in
        let srcrs2' ≝ rev … srcrs2 in
        let insts_init ≝ [
          translate_cst globals (Ointconst I8 (zero ?)) tmp_destrs;
          translate_cst globals (Ointconst I8 (zero ?)) added;
          adds_graph rtl_params1 globals [
            sequential rtl_params_ globals (INT rtl_params_ globals tmp_zero (zero …));
            sequential rtl_params_ globals (INT rtl_params_ globals tmp_one (bitvector_of_nat … 1))
          ]
        ]
        in
        let insts_main ≝
          translate_lt_main globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in
          let insts_main ≝ [ adds_graph rtl_params1 globals insts_main ] in
          let insts_exit ≝ [ translate_move globals destrs tmp_destrs ] in
            add_translates rtl_params1 globals (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def
      ]
    ]
  ].
  [2: >tmp_destrs_proof @prf_destrs
  |1: normalize nodelta
      generalize in match srcrs12_proof
      #HYP >rev_length >rev_length @HYP
  ]
qed.

definition add_128_to_last ≝
  λglobals: list ident.
  λtmp_128: register.
  λrs.
  λprf: 0 < |rs|.
  λstart_lbl: label.
  match rs with
  [ nil ⇒ adds_graph rtl_params1 globals [ ] start_lbl
  | _ ⇒
    let r ≝ last_safe … rs prf in
      adds_graph rtl_params1 globals [
        sequential rtl_params_ globals (OP2 rtl_params_ globals Add r r tmp_128)
      ] start_lbl
  ].

definition translate_lts ≝
  λglobals: list ident.
  λdestrs: list register.
  λdestrs_prf: 0 < |destrs|.
  λsrcrs1: list register.
  λsrcrs2: list register.
  λsrcrs1_lt_prf: 0 < |srcrs1|.
  λsrcrs2_lt_prf: 0 < |srcrs2|.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef: rtl_internal_function globals.
  match fresh_regs_strong globals def (|srcrs1|) with
  [ dp def_tmp_srcrs1 srcrs1_prf ⇒
    let def ≝ \fst def_tmp_srcrs1 in
    let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in
    match fresh_regs_strong globals def (|srcrs2|) with
    [ dp def_tmp_srcrs2 srcrs2_prf ⇒
      let def ≝ \fst def_tmp_srcrs2 in
      let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in
      let 〈def, tmp_128〉 ≝ fresh_reg rtl_params0 globals def in
        add_translates rtl_params1 globals [
          translate_move globals tmp_srcrs1 srcrs1;
          translate_move globals tmp_srcrs2 srcrs2;
          adds_graph rtl_params1 globals [
            sequential rtl_params_ globals (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128))
          ];
          add_128_to_last globals tmp_128 tmp_srcrs1 ?;
          add_128_to_last globals tmp_128 tmp_srcrs2 ?;
          translate_lt globals destrs destrs_prf tmp_srcrs1 tmp_srcrs2
        ] start_lbl dest_lbl def
    ]
  ].
  [1: >srcrs1_prf @srcrs1_lt_prf
  |2: >srcrs2_prf @srcrs2_lt_prf
  ]
qed.

definition translate_op2 ≝
  λglobals: list ident.
  λop2.
  λdestrs: list register.
  λdestrs_prf: 0 < |destrs|.
  λsrcrs1: list register.
  λsrcrs2: list register.
  λsrcrs2_destrs_prf: |srcrs2| = |destrs|.
  λsrcrs1_destrs_prf: |srcrs1| = |destrs|.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef: rtl_internal_function globals.
  match op2 with
  [ Oadd ⇒
    translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
  | Oaddp ⇒
    translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
  | Osub ⇒
    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
  | Osubpi ⇒
    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
  | Osubpp sz ⇒
    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
  | Omul ⇒
    translate_mul globals destrs srcrs1 srcrs2 ? start_lbl dest_lbl def
  | Odivu ⇒
    match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
    [ cons hd tl ⇒ λcons_prf.
      match tl with
      [ nil ⇒ translate_divumodu8 globals true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
      | _ ⇒ ? (* not implemented *)
      ] 
    | nil ⇒ λnil_absrd. ?
    ] ?
  | Omodu ⇒
    match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
    [ cons hd tl ⇒ λcons_prf.
      match tl with
      [ nil ⇒ translate_divumodu8 globals false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
      | _ ⇒ ? (* not implemented *)
      ] 
    | nil ⇒ λnil_absrd. ?
    ] ?
  | Oand ⇒
    translate_op globals And destrs srcrs1 srcrs2 start_lbl dest_lbl def
  | Oor ⇒
    translate_op globals Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
  | Oxor ⇒
    translate_op globals Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
  | Ocmp c ⇒
    match c with
    [ Ceq ⇒
      add_translates rtl_params1 globals [
        translate_ne globals destrs srcrs1 srcrs2;
        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
      ] start_lbl dest_lbl def
    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
    | Clt ⇒ translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def
    | Cgt ⇒ translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def
    | Cle ⇒
      add_translates rtl_params1 globals [
        translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ?;
        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
      ] start_lbl dest_lbl def
    | Cge ⇒
      add_translates rtl_params1 globals [
        translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ?;
        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
      ] start_lbl dest_lbl def
    ]
  | Ocmpu c ⇒
    match c with
    [ Ceq ⇒
      add_translates rtl_params1 globals [
        translate_ne globals destrs srcrs1 srcrs2;
        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
      ] start_lbl dest_lbl def
    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
    | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
    | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
    | Cle ⇒
      add_translates rtl_params1 globals [
        translate_lt globals destrs destrs_prf srcrs2 srcrs1;
        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
      ] start_lbl dest_lbl def
    | Cge ⇒
      add_translates rtl_params1 globals [
        translate_lt globals destrs destrs_prf srcrs1 srcrs2;
        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
      ] start_lbl dest_lbl def
    ]
  | Ocmpp c ⇒
    match c with
    [ Ceq ⇒
      add_translates rtl_params1 globals [
        translate_ne globals destrs srcrs1 srcrs2;
        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
      ] start_lbl dest_lbl def
    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
    | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
    | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
    | Cle ⇒
      add_translates rtl_params1 globals [
        translate_lt globals destrs destrs_prf srcrs2 srcrs1;
        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
      ] start_lbl dest_lbl def
    | Cge ⇒
      add_translates rtl_params1 globals [
        translate_lt globals destrs destrs_prf srcrs1 srcrs2;
        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
      ] start_lbl dest_lbl def
    ]
  | _ ⇒ ? (* assert false, implemented in run time or float op *)
  ].
  [1:
    @sym_eq
    assumption
  |3,8,19,22,24,25:
    >srcrs1_destrs_prf
    assumption
  |4,9:
    normalize in nil_absrd;
    cases(not_le_Sn_O 0)
    #HYP cases(HYP nil_absrd)
  |5,10,20,21,23,26:
    >srcrs2_destrs_prf
    assumption
  |*:
    cases not_implemented (* XXX: yes, really *)
  ]
qed.

definition translate_cond: ∀globals: list ident. list register → label → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
  λglobals: list ident.
  λsrcrs: list register.
  λstart_lbl: label.
  λlbl_true: label.
  λlbl_false: label.
  λdef: rtl_internal_function globals.
  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
  let 〈tmp_lbl, def〉 ≝ fresh_label rtl_params1 globals def in
  let init ≝ sequential rtl_params_ globals (INT rtl_params_ globals tmpr (zero …)) in
  let f ≝ λsrcr. sequential rtl_params_ globals (OP2 rtl_params_ globals Or tmpr tmpr srcr) in
  let def ≝ adds_graph rtl_params1 globals (init :: (map ? ? f srcrs)) start_lbl tmp_lbl def in
    add_graph rtl_params1 globals tmp_lbl (sequential rtl_params_ globals (COND rtl_params_ globals tmpr lbl_true) lbl_false) def.

definition translate_load ≝
  λglobals: list ident.
  λaddr.
  λaddr_prf: 2 = |addr|.
  λdestrs: list register.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef: rtl_internal_function globals.
  match fresh_regs_strong rtl_params0 globals def (|addr|) with
  [ dp def_save_addr save_addr_prf ⇒
    let def ≝ \fst def_save_addr in
    let save_addr ≝ \snd def_save_addr in
    match fresh_regs_strong rtl_params0 globals def (|addr|) with
    [ dp def_tmp_addr tmp_addr_prf ⇒
      let def ≝ \fst def_tmp_addr in
      let tmp_addr ≝ \snd def_tmp_addr in
      let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in
      let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
      let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
      let insts_save_addr ≝ translate_move globals save_addr addr in
      let f ≝ λtranslates_off. λr.
        let 〈translates, off〉 ≝ translates_off in
        let translates ≝ translates @ [
          adds_graph rtl_params1 globals [
            sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
          ];
          translate_op2 globals Oaddp tmp_addr ? save_addr [dummy; tmpr] ? ?;
          adds_graph rtl_params1 globals [
            sequential rtl_params_ globals (LOAD rtl_params_ globals r tmp_addr1 tmp_addr2)
          ]
        ]
        in
        let 〈carry, result〉 ≝ half_add … off int_size in
          〈translates, result〉
      in
      let 〈translates, ignore〉 ≝ foldl … f 〈[ ], (zero ?)〉 destrs in
        add_translates rtl_params1 globals (insts_save_addr :: translates) start_lbl dest_lbl def
    ]
  ].
  [1: >tmp_addr_prf >save_addr_prf %
  |2: >save_addr_prf >tmp_addr_prf
      @addr_prf
  |3: >tmp_addr_prf normalize
      <addr_prf //
  |4: >tmp_addr_prf assumption
  ]
qed.

definition translate_store ≝
  λglobals: list ident.
  λaddr.
  λaddr_prf: 2 = |addr|.
  λsrcrs: list register.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef: rtl_internal_function globals.
  match fresh_regs_strong rtl_params0 globals def (|addr|) with
  [ dp def_tmp_addr tmp_addr_prf ⇒
    let def ≝ \fst def_tmp_addr in
    let tmp_addr ≝ \snd def_tmp_addr in
    let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in
    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
    let f ≝ λtranslate_off. λsrcr.
      let 〈translates, off〉 ≝ translate_off in
      let translates ≝ translates @ [
        adds_graph rtl_params1 globals [
          sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
        ];
        translate_op2 globals Oaddp tmp_addr … addr [dummy; tmpr] ? ?;
        adds_graph rtl_params1 globals [
          sequential rtl_params_ globals (STORE rtl_params_ globals tmp_addr1 tmp_addr2 srcr)
        ]
      ]
      in
        let 〈carry, result〉 ≝ half_add … off int_size in
          〈translates, result〉
    in
    let 〈translates, ignore〉 ≝ foldl … f 〈[ ], zero …〉 srcrs in
      add_translates rtl_params1 globals translates start_lbl dest_lbl def
  ].
  [1: >tmp_addr_prf %
  |2: >tmp_addr_prf normalize
      <addr_prf //
  |3: >tmp_addr_prf <addr_prf //
  |4: >tmp_addr_prf @addr_prf
  ]
qed.

axiom fake_label: label.

(* XXX: following conversation with CSC about the mix up in extension statements
        and extension instructions in RTL, use fake_label in calls to
        tailcall_* instructions. *)
definition translate_stmt ≝
  λglobals: list ident.
  λlenv: local_env.
  λlbl: label.
  λstmt.
  λdef: rtl_internal_function globals.
  match stmt with
  [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def
  | St_cost cost_lbl lbl' ⇒ add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (COST_LABEL rtl_params_ globals cost_lbl) lbl') def
  | St_const destr cst lbl' ⇒
    translate_cst globals cst (find_local_env destr lenv) lbl lbl' def
  | St_op1 op1 destr srcr lbl' ⇒
    translate_op1 globals op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def
  | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
    translate_op2 globals op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
    (* XXX: should we be ignoring this? *)
  | St_load ignore addr destr lbl' ⇒
    translate_load globals (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
    (* XXX: should we be ignoring this? *)
  | St_store ignore addr srcr lbl' ⇒
    translate_store globals (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def
  | St_call_id f args retr lbl' ⇒
    match retr with
    [ Some retr ⇒
      add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) (find_local_env retr lenv)) lbl') def
    | None ⇒ add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) [ ]) lbl') def
    ]
  | St_call_ptr f args retr lbl' ⇒
    match retr with
    [ None ⇒
      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
        add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])) lbl') def
    | Some retr ⇒
      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
        add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv))) lbl') def
    ]
  | St_tailcall_id f args ⇒
    add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params_ globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) fake_label) def
  | St_tailcall_ptr f args ⇒
    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
      add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params1 globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) fake_label) def
  | St_cond r lbl_true lbl_false ⇒
    translate_cond globals (find_local_env r lenv) lbl lbl_true lbl_false def
  | St_jumptable r l ⇒ ? (* assert false: not implemented yet *)
  | St_return ⇒ add_graph rtl_params1 globals lbl (RETURN …) def
  ].
  [10: cases not_implemented (* jtable case *)
  |*: cases daemon (* TODO: proofs regarding lengths of lists, examine! *)
  ]
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 params ≝ 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' ≝ params 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' ≝ add LabelTag ? (empty_map LabelTag ?) entry' (GOTO rtl_params_ globals entry') in
  let graph' ≝ add LabelTag ? graph' exit' (GOTO rtl_params_ globals exit') in
  let res ≝
    mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params'
     locals' stack_size' graph' ? ? in
    foldi … (translate_stmt globals … lenv) (f_graph def) res.
[ % [@entry' | @graph_add_lookup @graph_add]
| % [@exit'  | @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 (transf_fundef … (translate_internal (prog_var_names …))).