include "utilities/RegisterSet.ma".
include "common/Identifiers.ma".
include "RTL/RTL.ma".
include "ERTL/ERTL.ma".
include "joint/TranslateUtils.ma".
include "joint/joint_stacksizes.ma".

include alias "basics/lists/list.ma".

definition save_hdws :
  ∀globals.list (register×(Σr.ertl_hdw_readable r∧ertl_hdw_writable r)) → list (joint_seq ERTL globals) ≝
 λglobals.
  let save_hdws_internal : (register×(Σr.?)) → ? ≝
     λdestr_srcr.PSD (\fst destr_srcr) ← HDW (\snd destr_srcr) in
  map ?? save_hdws_internal.
[ @(π1 (pi2 ?? (\snd destr_srcr))) | @I ] qed.

definition restore_hdws :
  ∀globals.list (psd_argument×(Σr.ertl_hdw_readable r∧ertl_hdw_writable r)) → list (joint_seq ERTL globals) ≝
  λglobals.
   let restore_hdws_internal ≝
    λdestr_srcr:psd_argument×(Σr.?).HDW (\snd destr_srcr) ← \fst destr_srcr in
    map ? ? restore_hdws_internal.
  @(π2 (pi2 ?? (\snd destr_srcr))) qed.
  
definition RegisterParamsSig : list (Σr.ertl_hdw_readable r∧ertl_hdw_writable r) ≝
[Register30; Register31; Register32; Register33; Register34; Register35;
   Register36; Register37]. %% qed.

(*definition RegisterCalleeSavedSig : list (Σr.ertl_hdw_readable r∧ertl_hdw_writable r) ≝
[Register20; Register21; Register22; Register23; Register24; Register25;
   Register26; Register27]. %% qed.*)

definition RegisterRetsSig : list (Σr.ertl_hdw_readable r∧ertl_hdw_writable r) ≝
 [Register00; Register01; Register02; Register03]. %% qed.

definition get_params_hdw :
  ∀globals.list register → list (joint_seq ERTL globals) ≝
  λglobals,params.
  save_hdws … (zip_pottier … params RegisterParamsSig).

definition get_param_stack :
  ∀globals.register → register → register →
  list (joint_seq ERTL globals) ≝
  λglobals,addr1,addr2,destr.
  (* liveness analysis will erase the last useless ops *)
  [ LOAD ?? destr addr1 addr2 ;
    addr1 ← addr1 .Add. (int_size : Byte) ;
    addr2 ← addr2 .Addc. zero_byte
  ].

definition get_params_stack :
  ∀globals.register → register → register → list register →
  list (joint_seq ERTL globals) ≝
  λglobals.
  λtmpr,addr1,addr2,params.
  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
  [ (ertl_frame_size tmpr : joint_seq ??) ;
    CLEAR_CARRY ?? ;
    tmpr ← tmpr .Sub. params_length_byte ; (* will be constant later *)
    PSD addr1 ← HDW RegisterSPL ;
    PSD addr2 ← HDW RegisterSPH ;
    addr1 ← addr1 .Add. tmpr ;
    addr2 ← addr2 .Addc. zero_byte ] @    
  flatten … (map ?? (get_param_stack globals addr1 addr2) params). % qed.

definition get_params ≝
  λglobals,tmpr,addr1,addr2,params.
  let n ≝ min (length … params) (length … RegisterParams) in
  let 〈hdw_params, stack_params〉 ≝ list_split … n params in
  get_params_hdw globals hdw_params @ get_params_stack … tmpr addr1 addr2 stack_params.

(*
definition save_return :
  ∀globals.list register → list (joint_seq ERTL globals) ≝
  λglobals,ret_regs.
  match reduce_strong ? ? RegisterSTS ret_regs with
  [ mk_Sig crl crl_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 *)
    map2 … (λst : Σr.?.λr : register.HDW st ← r) commonl commonr crl_proof @
    map … (λst : Σr.?.HDW st ← zero_byte) restl
  ]. @(pi2 ?? st) qed.
*)


definition assign_result : ∀globals.
  list register → list (joint_seq ERTL globals) ≝
  λglobals,ret_regs.
  match reduce_strong ?? RegisterRetsSig ret_regs with
  [ mk_Sig crl crl_proof ⇒
    let commonl ≝ \fst (\fst crl) in
    let commonr ≝ \fst (\snd crl) in
    let restl ≝ \snd (\fst crl) in
    map2 … (λR : Σr.?.λr : register.HDW R ← PSD r) commonl commonr crl_proof @
    map … (λR : Σr.?.HDW R ← zero_byte) restl
  ]. [ @I |*: @(π2 (pi2 ?? R)) ] qed.

lemma All_map2 : ∀A,B,C,P,R,f,l1,l2,prf.
 All2 A B P l1 l2 →
 (∀x,y.P x y → R (f x y)) →
 All C R (map2 A B C f l1 l2 prf).
#A #B #C #P #R #f #l1 elim l1 -l1
[ * [ #prf * #H % ] #hd' #tl'
| #hd #tl #IH * [2: #hd' #tl' ]
] #prf normalize in prf; destruct
* #H1 #H2 #H % [ @H @H1 | @IH assumption ] qed.

lemma All2_True : ∀A,B,l1,l2.|l1| = |l2| → All2 A B (λ_.λ_.True) l1 l2.
#A #B #l1 elim l1 -l1
[ * [ #prf % ] #hd' #tl'
| #hd #tl #IH * [2: #hd' #tl' ]
] #prf normalize in prf; destruct %{I} @IH assumption
qed.

lemma All_True : ∀A,l.All A (λ_.True) l.
#A #l elim l -l [ % | #hd #tl #IH %{I IH} ] qed.

definition epilogue :
  ∀globals.list register → register → register →
  Σl : list (joint_seq ERTL globals).
  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
  λglobals,ret_regs,sral,srah.
  assign_result globals ret_regs @
  [ PUSH ERTL ? sral ;
    PUSH … srah ].
@hide_prf
@All_append
[ whd in match assign_result;
  generalize in match reduce_strong; #f normalize nodelta
  cases (f ????) #l #prf normalize nodelta
  @All_append
  [ @(All_map2 … (All2_True … prf)) #x #y #_ %
  | @(All_map … (All_True …)) #x #_ %
  ]
| %%%
]
qed.

definition prologue :
  ∀globals.list register → register → register → register → register → register →
  bind_new register (list (joint_seq ERTL globals)) ≝
  λglobals,params,sral,srah,tmpr,addr1,addr2.
  [ POP ERTL … srah ;
    POP … sral
  ] @ get_params … tmpr addr1 addr2 params.

definition set_params_hdw :
  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
  λglobals,params.
  restore_hdws globals (zip_pottier ? ? params RegisterParamsSig).

definition set_param_stack :
  ∀globals.register → register → psd_argument →
  list (joint_seq ERTL globals) ≝
  λglobals,addr1,addr2,arg.
  [ STORE … addr1 addr2 arg ;
    addr1 ← addr1 .Add. (int_size : Byte) ;
    addr2 ← addr2 .Addc. zero_byte
  ].

definition set_params_stack :
  ∀globals.list psd_argument → bind_new register ? ≝
  λglobals,params.
  νaddr1,addr2 in
  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
  [ PSD addr1 ← HDW RegisterSPL ;
    PSD addr2 ← HDW RegisterSPH ;
    CLEAR_CARRY ?? ;
    addr1 ← addr1 .Sub. params_length_byte ;
    addr2 ← addr2 .Sub. zero_byte
  ] @
  flatten … (map … (set_param_stack globals addr1 addr2) params). % qed.

definition set_params :
  ∀globals.list psd_argument →
  Σb : bind_new register (list (joint_seq ERTL globals)).
  BindNewP … (All (joint_seq ??) (λs.step_labels … s = [ ])) b ≝
  λglobals,params.
  let n ≝ min (|params|) (|RegisterParamsSig|) in
  let hdw_stack_params ≝ split ? params n in
  let hdw_params ≝ \fst hdw_stack_params in
  let stack_params ≝ \snd hdw_stack_params in
  set_params_hdw globals hdw_params @@ set_params_stack globals stack_params.
@hide_prf
  @mp_bind [3: #l1 #H1 @mp_bind [3: #l2 #H2 @(All_append … H1 H2) ] |*:]
  [ #r1 #r2
    %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)}
    @All_append [ % ]
    elim stack_params [ % ] #hd #tl #IH whd in match flatten; normalize nodelta
    whd in match (foldr ?????); %{(refl …)} %{(refl …)} %{(refl …)} @IH
  | whd whd in match set_params_hdw; normalize nodelta
    whd in match restore_hdws; normalize nodelta @(All_map … (All_True …))
    #a #_ %
  ]
qed.

definition fetch_result :
  ∀globals.list register →
  Σl : list (joint_seq ERTL globals).
  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
  λglobals,ret_regs.
  match reduce_strong ?? ret_regs RegisterRetsSig with
  [ mk_Sig crl crl_proof ⇒
    let commonl ≝ \fst (\fst crl) in
    let commonr ≝ \fst (\snd crl) in
    map2 … (λr.λR : Σr.?.PSD r ← HDW R) commonl commonr crl_proof
  ].
@hide_prf [2: % |3: @(π1 (pi2 … R)) ]
@(All_map2 … (All2_True … crl_proof)) #x #y #_ %
qed.

definition translate_step :
  ∀globals.label → joint_step RTL globals →
    bind_step_block ERTL globals ≝
  λglobals.λ_.λs.
  match s return λ_.bind_step_block ?? with
  [ step_seq s ⇒
    bret … match s return λ_.step_block ?? with
    [ PUSH _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *)
    | POP _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *)
    | MOVE rs ⇒ [PSD (\fst rs) ← \snd rs]
    | ADDRESS x prf off r1 r2 ⇒
      [ADDRESS ERTL ? x prf off r1 r2]
    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
      [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2]
    | OP1 op1 destr srcr ⇒
      [OP1 ERTL ? op1 destr srcr]
    | OP2 op2 destr srcr1 srcr2 ⇒
      [OP2 ERTL ? op2 destr srcr1 srcr2]
    | CLEAR_CARRY ⇒
      [CLEAR_CARRY ??]
    | SET_CARRY ⇒
      [SET_CARRY ??]
    | LOAD destr addr1 addr2 ⇒
      [LOAD ERTL ? destr addr1 addr2]
    | STORE addr1 addr2 srcr ⇒
      [STORE ERTL ? addr1 addr2 srcr]
    | COMMENT msg ⇒
      [COMMENT … msg]
    | extension_seq ext ⇒
      match ext return λ_.step_block ?? with
      [ rtl_stack_address addr1 addr2 ⇒
        [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
      ]
    ]
  | COST_LABEL lbl ⇒
    bret … 〈[ ], λ_.COST_LABEL ERTL ? lbl, [ ]〉
  | CALL f args ret_regs ⇒
    ! pref ← pi1 … (set_params ? args) ;
    bret ? (step_block ??) 〈add_dummy_variance … pref,
             λ_.CALL ERTL ? f (|args|) it,
             fetch_result ? ret_regs〉
  | COND r ltrue ⇒
    bret … 〈[ ], λ_.COND ERTL ? r ltrue, [ ]〉
  ]. % qed.

definition translate_fin_step :
  ∀globals.list register → register → register →
    label → joint_fin_step RTL →
    bind_fin_block ERTL globals ≝
  λglobals.λral,rah,to_restore.λ_.λs.
  match s return λ_.bind_fin_block ERTL ? with
  [ GOTO lbl' ⇒ bret … 〈[ ], GOTO … lbl'〉
  | RETURN ⇒ bret … 〈epilogue … ral rah to_restore, RETURN ?〉
  | TAILCALL b _ _ ⇒ match b in False with [ ]
  ].

definition translate_data :
 ∀globals.joint_closed_internal_function RTL globals →
 bound_b_graph_translate_data RTL ERTL globals ≝
λglobals,def.
let params ≝ joint_if_params … def in
    νral,rah,tmpr,addr1,addr2 in
    ! prologue ← prologue globals params ral rah tmpr addr1 addr2 ;
    return mk_b_graph_translate_data RTL ERTL globals
    (* init_ret ≝ *) it
    (* init_params ≝ *) it
    (* init_local_stacksize ≝ *) (joint_if_local_stacksize … def)
    (* init_params_stacksize ≝ *) (joint_if_params_stacksize … def + (* is 0, but needed for monotonicity *)
                                   (|params| - |RegisterParams|))
    (* init_spilled_stacksize ≝ *) (joint_if_spilled_stacksize … def(* is 0, but needed for monotonicity *)) 
    (* added_prologue ≝ *) prologue
    (* new_regs ≝ *) ([ral ; rah ; tmpr ; addr1 ; addr2 ])
    (* f_step ≝ *) (translate_step globals)
    (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah)
    ????.
@hide_prf
[2: #l #c %
|1: #l * [ #c' | #f #args #dest | #a #ltrue | #s ] #c whd
  [2: #r1 #r2 ] whd #l' #EQ destruct try %
  cases s in EQ; whd in match ensure_step_block; normalize nodelta
  try #a try #b try #c try #d try #e try #f destruct
  cases a in b; #a1 #a2 normalize nodelta #EQ destruct
|5: #ral #rah #tmpr #addr1 #addr2 %
|*:  cases daemon (* TODO *)
]
(* #l *
[ #l whd %{I} %{I} %1 %
| whd %{I} cases (epilogue ?????) @All_mp #s #EQ whd >EQ %
| *
| #c %{I} %{I} #l %
| #called #args #dest @(mp_bind … (BindNewP …))
  [2: @(pi2 ? (λ_.?)) |*:] #l1 #H1 whd % [%]
    [ @(All_map … H1) #a #EQ #l whd >EQ %
    | #l %
    | cases (fetch_result ??) @All_mp #s #EQ whd >EQ %
    ]
| #a #l_true whd %{I} %{I} #l %{I} %2 %1 %
| * try #a try #b try #c try #d try #e whd
  try (%{I} %{I} #l %)
  cases a -a #a #b whd %{I} % [ %{I} ] #l %
]*)
qed.

(* removing this because of how insert_prologue is now defined
definition generate ≝
  λglobals.
  λstmt.
  λdef: joint_internal_function globals ERTL.
  let 〈entry, def〉 ≝ fresh_label … def in
  let graph ≝ add … (joint_if_code … def) entry stmt in
   set_joint_if_graph … (ERTL globals) graph def ??.
  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
    *) cases daemon (*CSC: XXX *)
  ]
qed.

let rec find_and_remove_first_cost_label_internal (globals: list ident)
  (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat)
    on num_nodes ≝
  match num_nodes with
  [ O ⇒ 〈None ?, def〉
  | S num_nodes' ⇒
    match lookup … (joint_if_code … def) lbl with
    [ None ⇒ 〈None ?, def〉
    | Some stmt ⇒ 
      match stmt with
      [ sequential inst lbl ⇒
         match inst with
          [ COST_LABEL cost_lbl ⇒
             〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉
          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
      | RETURN ⇒ 〈None …, def〉
      | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
      ]]].
    
definition find_and_remove_first_cost_label ≝
  λglobals,def.  
    find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)).

definition move_first_cost_label_up_internal ≝
  λglobals,def.
  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in
  match cost_label with
  [ None ⇒ def
  | Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
  ].

definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
*)

definition rtl_to_ertl : rtl_program → ertl_program ≝
  b_graph_transform_program … translate_data.

lemma RTLToERTL_monotone_stacksizes :
∀p_in.let p_out ≝ rtl_to_ertl p_in in
stack_cost_model_le (stack_cost ? p_in) (stack_cost ? p_out) ≝
joint_transform_monotone_stacksizes ….