source: LTS/monostack_to_asm_pass.ma @ 3673

(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "asm.ma".

let rec post_labelled_return_instr (p : instr_params) (l_p : label_params) (i : Instructions p l_p) on i : Prop ≝
match i with
[ EMPTY ⇒ True
| RETURN _ ⇒ True
| SEQ _ _ instr ⇒ post_labelled_return_instr … instr
| COND _ _ i_true _ i_false instr ⇒ post_labelled_return_instr … i_true ∧ post_labelled_return_instr … i_false ∧ 
       post_labelled_return_instr … instr
| LOOP _ _ i_true _ instr ⇒ post_labelled_return_instr … i_true ∧ post_labelled_return_instr … instr
| CALL _ _ opt_l instr ⇒ opt_l ≠ None ? ∧ post_labelled_return_instr … instr 
| IO _ _ _ instr ⇒ post_labelled_return_instr … instr 
].

definition post_labelled_return_program : ∀p,p',l_p.Program p p' l_p → Prop ≝ 
λp,p',l_p,prog.post_labelled_return_instr … (main … prog) ∧ All … (λx.post_labelled_return_instr … (f_body … x)) (env … prog).

let rec trans_mono_stack_instr (i : mono_stack_Instructions)
(pc : ℕ) : post_labelled_return_instr … i → (list asm_instructions) × (list (ℕ × (ReturnPostCostLabel flat_labels))) ≝
match i return λx.(post_labelled_return_instr ?? x) → ? with 
[ EMPTY ⇒ λ_.〈nil ?,nil ?〉
| RETURN _ ⇒ λ_.〈[(Seq asm_assembler_params ? asm_pop_frame (None ?)) ; (Iret …)],nil ?〉 
| SEQ i opt_l instr ⇒ λprf.
     let 〈t_instr,ret_list〉 ≝ (trans_mono_stack_instr instr (S pc) prf) in
     〈(Seq asm_assembler_params ? (asm_seq i) opt_l) :: t_instr , ret_list 〉
| CALL f act_p opt_l instr ⇒ λprf.
    let 〈t_instr,ret_list〉 ≝ (trans_mono_stack_instr instr (S (S pc)) (proj2 … prf)) in
    〈(Seq asm_assembler_params ? (asm_push_frame) (None ?)):: (Icall … f) :: t_instr,
     (〈(S (S pc)),opt_safe … (proj1 … prf)〉) :: ret_list 〉 
| COND cond ltrue i_true lfalse i_false instr ⇒ λprf.
  let 〈t_i_false,ret_ifalse〉 ≝ (trans_mono_stack_instr i_false (S pc) (proj2 ?? (proj1 … prf))) in
  let 〈t_i_true,ret_itrue〉 ≝ (trans_mono_stack_instr i_true ((S pc) + ((|t_i_false|) + 1)) (proj1 … (proj1 … prf))) in
  let 〈t_instr,ret_list〉 ≝ (trans_mono_stack_instr instr ((S pc) + ((|t_i_false|) + 1) + (|t_i_true|)) (proj2 … prf)) in
  〈CJump asm_assembler_params ? it ((S pc) + ((|t_i_false|) + 1)) ltrue lfalse ::
    (t_i_false @ [Ijmp asm_assembler_params ?  ((S pc) + ((|t_i_false|) + 1) + (|t_i_true|))] @ t_i_true @ t_instr),
  ret_ifalse @ ret_itrue @ ret_list
  〉
| LOOP cond ltrue i_true lfalse instr ⇒ λprf.
   let trans_cond ≝ foldr … (λc,tail.(Seq asm_assembler_params ? (asm_seq (push c)) (None ?)) :: tail) (nil ?) cond in
   let 〈t_i_true,ret_itrue〉 ≝ (trans_mono_stack_instr i_true (pc + (|trans_cond|) + 3) (proj1 … prf)) in
   let 〈t_instr,ret_list〉 ≝ (trans_mono_stack_instr instr (pc + (|trans_cond|) + 3 + (|t_i_true|) + 1) (proj2 … prf)) in
   〈trans_cond @ 
    [Seq asm_assembler_params ? (asm_seq (push push_not)) (None ?) ; 
     Seq asm_assembler_params ? (pop_cond) (None ?); 
     CJump asm_assembler_params ? it (pc + (|trans_cond|) + 3 + (|t_i_true|) + 1) ltrue lfalse] @ t_i_true @
    [Ijmp asm_assembler_params ? pc] @ t_instr,
   ret_itrue @ ret_list 〉
| IO _ io _ _ ⇒ ?
].
cases io qed.

record asm_env_trans_info : Type[0] ≝ 
{ asm_instr : list asm_instructions
; asm_entry_fun : FunctionName → ℕ
; asm_call_label_fun : list (ℕ × (CallCostLabel flat_labels))
; asm_ret_label_fun :list (ℕ × (ReturnPostCostLabel flat_labels))
}.

let rec trans_mono_stack_env_prog (env : list mono_stack_envitem) (pc : ℕ) 
(entry_f : FunctionName → ℕ) on env : All … (λx.post_labelled_return_instr … (f_body … x)) env → asm_env_trans_info ≝ 
match env return λx.All ?? x → ? with
[ nil ⇒ λ_.mk_asm_env_trans_info (nil ?) entry_f (nil ?) (nil ?)
| cons hd tl ⇒ λprf.let 〈t_body,list_ret〉 ≝ trans_mono_stack_instr (f_body … hd) (S pc) (proj1 … prf) in
                    let ih_info ≝ trans_mono_stack_env_prog tl (pc + 1 + |t_body|) entry_f (proj2 … prf) in
                    mk_asm_env_trans_info
                     ((Seq asm_assembler_params ? (asm_alloc_frame (f_pars … (f_sig … hd))) (None ?))::(t_body @ (asm_instr … ih_info)))
                     (update_fun … (asm_entry_fun … ih_info) (f_name … (f_sig … hd)) pc)
                     (〈pc,f_lab … hd〉::asm_call_label_fun … ih_info)
                     (list_ret @ asm_ret_label_fun … ih_info)
].

definition trans_mono_stack_prog : ∀prog : Program stack_env_params stack_instr_params flat_labels.
no_duplicates_labels … prog → post_labelled_return_program … prog → asm_program ≝ 
λprog,no_dup,post_lab.
let 〈t_main,main_ret_lab〉 ≝ trans_mono_stack_instr (main … prog) O (proj1 … post_lab) in 
let trans_env_info ≝ trans_mono_stack_env_prog (env … prog) (|t_main|) (λ_.O) (proj2 … post_lab) in 
mk_AssemblerProgram ?? (t_main @ (asm_instr … trans_env_info)) (pred (|t_main|)) ? (asm_entry_fun … trans_env_info) 
 (asm_call_label_fun … trans_env_info) (main_ret_lab @ (asm_ret_label_fun … trans_env_info)) ??.
try @hide_prf cases daemon (*init_act to fix on language*)
qed.

let rec mono_asm_state_rel_aux (s_stack : list ((ActionLabel flat_labels) × mono_stack_Instructions)) (stack_t : stackT)
(post_t : list asm_instructions) (t_code : list asm_instructions) (post_t_pc : ℕ) on s_stack : 
All … (λx.post_labelled_return_instr … (\snd x)) s_stack → Prop ≝ 
match s_stack return λx.All ?? x → ? with
[ nil ⇒ λ_.stack_t = nil ? (*stati finali to be fixed*)
| cons hd tl ⇒ λprf.
  (match hd return λx.hd = x → ? with
  [ mk_Prod act code ⇒ λEQ.
    match act with
    [ call_act f lab ⇒ False
    | ret_act opt_l ⇒ ∃pc :ℕ.∃stl : list ℕ.stack_t = pc :: stl ∧
                    let 〈ts_code,ret_label〉 ≝ trans_mono_stack_instr code pc ? in 
                    ∃pre_pc,post_pc.t_code = pre_pc @ ts_code @post_pc ∧ (|pre_pc|) = pc ∧
                    mono_asm_state_rel_aux tl stl post_pc t_code (pc + |ts_code|) (proj2 … prf)
    | cost_act opt_l ⇒ let 〈ts_code,ret_label〉 ≝ trans_mono_stack_instr code post_t_pc ? in 
                     (∃post_pc.post_t = ts_code @ post_pc ∧
                         mono_asm_state_rel_aux tl stack_t post_pc t_code (post_t_pc + |ts_code|) (proj2 … prf)) 
                     ∨
                     (∃new_pc.nth_opt … O post_t = return (Ijmp … new_pc) ∧
                      ∃pre_pc,post_pc.t_code = pre_pc @ ts_code @post_pc ∧ (|pre_pc|) = new_pc ∧
                      mono_asm_state_rel_aux tl stack_t post_pc t_code (new_pc + |ts_code|) (proj2 … prf))
    ]
  ])(refl …)
].
@hide_prf >EQ in prf; * // qed.

definition mono_asm_state_rel : ∀s_code : mono_stack_Instructions.
∀s_stack : list ((ActionLabel flat_labels) × mono_stack_Instructions). 
ℕ → stackT → list asm_instructions → ? → post_labelled_return_instr … s_code → 
All … (λx.post_labelled_return_instr … (\snd x)) s_stack → Prop ≝  
λs_code,s_stack,pc,t_stack,t_code,init_act,prf1,prf2.
let 〈ts_code,ret_label〉 ≝ trans_mono_stack_instr s_code pc prf1 in
∃pre_pc,post_t.t_code = pre_pc @ ts_code @ post_t ∧ (|pre_pc|) = pc ∧ 
∃chop_stack.s_stack = chop_stack @ [〈init_act,EMPTY …〉] ∧
 (All … (λx.let 〈act,code〉 ≝ x in is_cost_label … act → (bool_to_Prop (is_silent_cost_act_b … act))) chop_stack) ∧
 mono_asm_state_rel_aux s_stack t_stack post_t t_code (pc + |ts_code|) prf2.

definition monostack_asm_pass_rel : 
∀prog : Program stack_env_params stack_instr_params flat_labels.
∀no_dup : no_duplicates_labels … prog.∀prf : post_labelled_return_program … prog.
let t_prog ≝ trans_mono_stack_prog prog no_dup prf in
∀bound.
relations flat_labels 
(operational_semantics mono_stack_state_params (mono_stack_sem_state_params bound) prog)
(asm_operational_semantics … (asm_sem_params) t_prog) ≝ 
λprog,no_dup,prf,bound.
let t_prog ≝ trans_mono_stack_prog prog no_dup prf in
(mk_relations flat_labels (operational_semantics mono_stack_state_params (mono_stack_sem_state_params bound) prog)
 (asm_operational_semantics … (asm_sem_params) t_prog)
 (λs1,s2.
   match s2 with
   [ INITIAL ⇒ bool_to_Prop (lang_initial … (mono_stack_sem_state_params bound) prog s1)
   | FINAL ⇒ bool_to_Prop (lang_final … s1)
   | STATE s2' ⇒ store … s1 = (\fst (asm_store … s2')) ∧ ∃prf1 : post_labelled_return_instr … (code … s1).
                 ∃prf2 : All … (λx.post_labelled_return_instr … (\snd x)) (cont … s1).
                 mono_asm_state_rel (code … s1) (cont … s1) (pc … s2') (asm_stack … s2') (instructions … t_prog) 
                   (cost_act … (Some ? (initial_act … prog))) prf1 prf2
   ]
  )
 (λ_.λ_.True)).


definition mono_stack_asm_pass : ∀prog : Program stack_env_params stack_instr_params flat_labels.
∀no_dup : no_duplicates_labels … prog.∀prf : post_labelled_return_program … prog.
let t_prog ≝ trans_mono_stack_prog prog no_dup prf in
∀bound.simulation_conditions … (monostack_asm_pass_rel prog no_dup prf bound) ≝ 
λprog,no_dup,prf,bound.mk_simulation_conditions ….
[4: #s1 #s1' #s2 #H inversion H
  [ #st1 #st2 * #act #instr #tl #EQcode_st1 #EQcont_st1 #EQ1 #EQ2 destruct #EQstore #Hio1 #Hio2
    #no_ret #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in ⊢ (% → ?); cases s1' -s1' normalize nodelta
    [ whd in match lang_initial; normalize nodelta #H cases(andb_Prop_true … H) -H 
      #H cases(andb_Prop_true … H) -H #H cases(andb_Prop_true … H) -H #_ inversion(eqb_list ???) [2: #_ *]
      #ABS @⊥ >EQcont_st1 in ABS; normalize #EQ destruct
    | whd in match lang_final; normalize nodelta #H cases(andb_Prop_true … H) -H #_ >EQcont_st1 *
    ]
    #st2' * #EQstore1 * #post_label1 * #post_label2 whd in match mono_asm_state_rel; normalize nodelta lapply post_label1 
    >EQcode_st1 * whd in match (trans_mono_stack_instr ???); normalize nodelta
    * #pre_pc * #post_t ** #EQinstructions #EQpc ** [|#chop_hd #chop_tail] ** 
    [ >EQcont_st1 in ⊢ (% → ?); | >EQcont_st1 in ⊢ (% → ?); ] whd in ⊢ (??%% → ?); #EQ destruct -EQ
    * #_ #Hchop_tail >EQcont_st1 in post_label2; * #post_code_st2 #post_tail 
    whd in match (mono_asm_state_rel_aux ??????); @pair_elim #t_code_st2 #t_ret_st2 
    whd in match (length ??); <plus_n_O #EQt_code_st2
    * 
    [ * #post_pc1 * #EQ destruct #Haux #class1 #class2 %{(STATE … st2')} %{(t_base …)} % [2: %2 normalize % *]
      whd  % [ <EQstore1 //] %{post_code_st2} %{post_tail} whd >EQt_code_st2
      normalize nodelta %{pre_pc} %{post_pc1} % [ % // >EQinstructions %] %{chop_tail} % 
      [ % //] assumption
    | * #new_pc * #EQnew_pc * #pre_pc * #post_pc ** #EQinstructions1 #EQ destruct #Hcont #class1 #class2
      %{(STATE … (mk_vm_state … (|pre_pc|) (asm_stack … st2') (asm_store … st2') (asm_is_io … st2')))}
      %{(t_ind … (cost_act … (None ?)) … (t_base …))}
      [ whd <EQpc % [ cases daemon (* BOH!!! *) ] @(vm_ijump … (|pre_pc|)) // [2: cases daemon (* TODO ???*) ]
      whd in match fetch; normalize nodelta >EQinstructions >nth_second <EQpc [2: //] <minus_n_n assumption ]      
      % [2: %1 %2 cases daemon ] whd % [ <EQstore //] %{post_code_st2} %{post_tail} whd @pair_elim #p1 #p2 
      <EQpc in EQt_code_st2; #EQt_code_st2
      cut (∀a,b,c,c'. trans_mono_stack_instr a b c = trans_mono_stack_instr a b c')
      [ #a #b #c #d % ] #KK >KK [ <EQt_code_st2
      
       #K lapply (trans_eq ???? (sym_eq … EQt_code_st2) K)
      
       >EQt_code_st2 in ⊢ (% → ?);
      normalize nodelta
  |*: cases daemon
  ]
]
cases daemon
qed.