source: LTS/monostack_to_asm_pass.ma @ 3582

Last change on this file since 3582 was 3578, checked in by piccolo, 4 years ago

baco

File size: 12.4 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "asm.ma".
16
17let rec post_labelled_return_instr (p : instr_params) (l_p : label_params) (i : Instructions p l_p) on i : Prop ≝
18match i with
19[ EMPTY ⇒ True
20| RETURN _ ⇒ True
21| SEQ _ _ instr ⇒ post_labelled_return_instr … instr
22| COND _ _ i_true _ i_false instr ⇒ post_labelled_return_instr … i_true ∧ post_labelled_return_instr … i_false ∧
23       post_labelled_return_instr … instr
24| LOOP _ _ i_true _ instr ⇒ post_labelled_return_instr … i_true ∧ post_labelled_return_instr … instr
25| CALL _ _ opt_l instr ⇒ opt_l ≠ None ? ∧ post_labelled_return_instr … instr
26| IO _ _ _ instr ⇒ post_labelled_return_instr … instr
27].
28
29definition post_labelled_return_program : ∀p,p',l_p.Program p p' l_p → Prop ≝
30λp,p',l_p,prog.post_labelled_return_instr … (main … prog) ∧ All … (λx.post_labelled_return_instr … (f_body … x)) (env … prog).
31
32let rec trans_mono_stack_instr (i : mono_stack_Instructions)
33(pc : ℕ) : post_labelled_return_instr … i → (list asm_instructions) × (list (ℕ × (ReturnPostCostLabel flat_labels))) ≝
34match i return λx.(post_labelled_return_instr ?? x) → ? with
35[ EMPTY ⇒ λ_.〈nil ?,nil ?〉
36| RETURN _ ⇒ λ_.〈[(Seq asm_assembler_params ? asm_pop_frame (None ?)) ; (Iret …)],nil ?〉
37| SEQ i opt_l instr ⇒ λprf.
38     let 〈t_instr,ret_list〉 ≝ (trans_mono_stack_instr instr (S pc) prf) in
39     〈(Seq asm_assembler_params ? (asm_seq i) opt_l) :: t_instr , ret_list 〉
40| CALL f act_p opt_l instr ⇒ λprf.
41    let 〈t_instr,ret_list〉 ≝ (trans_mono_stack_instr instr (S (S pc)) (proj2 … prf)) in
42    〈(Seq asm_assembler_params ? (asm_push_frame) (None ?)):: (Icall … f) :: t_instr,
43     (〈(S (S pc)),opt_safe … (proj1 … prf)〉) :: ret_list 〉
44| COND cond ltrue i_true lfalse i_false instr ⇒ λprf.
45  let 〈t_i_false,ret_ifalse〉 ≝ (trans_mono_stack_instr i_false (S pc) (proj2 ?? (proj1 … prf))) in
46  let 〈t_i_true,ret_itrue〉 ≝ (trans_mono_stack_instr i_true ((S pc) + ((|t_i_false|) + 1)) (proj1 … (proj1 … prf))) in
47  let 〈t_instr,ret_list〉 ≝ (trans_mono_stack_instr instr ((S pc) + ((|t_i_false|) + 1) + (|t_i_true|)) (proj2 … prf)) in
48  〈CJump asm_assembler_params ? it ((S pc) + ((|t_i_false|) + 1)) ltrue lfalse ::
49    (t_i_false @ [Ijmp asm_assembler_params ?  ((S pc) + ((|t_i_false|) + 1) + (|t_i_true|))] @ t_i_true @ t_instr),
50  ret_ifalse @ ret_itrue @ ret_list
51  〉
52| LOOP cond ltrue i_true lfalse instr ⇒ λprf.
53   let trans_cond ≝ foldr … (λc,tail.(Seq asm_assembler_params ? (asm_seq (push c)) (None ?)) :: tail) (nil ?) cond in
54   let 〈t_i_true,ret_itrue〉 ≝ (trans_mono_stack_instr i_true (pc + (|trans_cond|) + 3) (proj1 … prf)) in
55   let 〈t_instr,ret_list〉 ≝ (trans_mono_stack_instr instr (pc + (|trans_cond|) + 3 + (|t_i_true|) + 1) (proj2 … prf)) in
56   〈trans_cond @
57    [Seq asm_assembler_params ? (asm_seq (push push_not)) (None ?) ;
58     Seq asm_assembler_params ? (pop_cond) (None ?);
59     CJump asm_assembler_params ? it (pc + (|trans_cond|) + 3 + (|t_i_true|) + 1) ltrue lfalse] @ t_i_true @
60    [Ijmp asm_assembler_params ? pc] @ t_instr,
61   ret_itrue @ ret_list 〉
62| IO _ io _ _ ⇒ ?
63].
64cases io qed.
65
66record asm_env_trans_info : Type[0] ≝
67{ asm_instr : list asm_instructions
68; asm_entry_fun : FunctionName → ℕ
69; asm_call_label_fun : list (ℕ × (CallCostLabel flat_labels))
70; asm_ret_label_fun :list (ℕ × (ReturnPostCostLabel flat_labels))
71}.
72
73let rec trans_mono_stack_env_prog (env : list mono_stack_envitem) (pc : ℕ)
74(entry_f : FunctionName → ℕ) on env : All … (λx.post_labelled_return_instr … (f_body … x)) env → asm_env_trans_info ≝
75match env return λx.All ?? x → ? with
76[ nil ⇒ λ_.mk_asm_env_trans_info (nil ?) entry_f (nil ?) (nil ?)
77| cons hd tl ⇒ λprf.let 〈t_body,list_ret〉 ≝ trans_mono_stack_instr (f_body … hd) (S pc) (proj1 … prf) in
78                    let ih_info ≝ trans_mono_stack_env_prog tl (pc + 1 + |t_body|) entry_f (proj2 … prf) in
79                    mk_asm_env_trans_info
80                     ((Seq asm_assembler_params ? (asm_alloc_frame (f_pars … (f_sig … hd))) (None ?))::(t_body @ (asm_instr … ih_info)))
81                     (update_fun … (asm_entry_fun … ih_info) (f_name … (f_sig … hd)) pc)
82                     (〈pc,f_lab … hd〉::asm_call_label_fun … ih_info)
83                     (list_ret @ asm_ret_label_fun … ih_info)
84].
85
86definition trans_mono_stack_prog : ∀prog : Program stack_env_params stack_instr_params flat_labels.
87no_duplicates_labels … prog → post_labelled_return_program … prog → asm_program ≝
88λprog,no_dup,post_lab.
89let 〈t_main,main_ret_lab〉 ≝ trans_mono_stack_instr (main … prog) O (proj1 … post_lab) in
90let trans_env_info ≝ trans_mono_stack_env_prog (env … prog) (|t_main|) (λ_.O) (proj2 … post_lab) in
91mk_AssemblerProgram ?? (t_main @ (asm_instr … trans_env_info)) (pred (|t_main|)) ? (asm_entry_fun … trans_env_info)
92 (asm_call_label_fun … trans_env_info) (main_ret_lab @ (asm_ret_label_fun … trans_env_info)) ??.
93try @hide_prf cases daemon (*init_act to fix on language*)
94qed.
95
96let rec mono_asm_state_rel_aux (s_stack : list ((ActionLabel flat_labels) × mono_stack_Instructions)) (stack_t : stackT)
97(post_t : list asm_instructions) (t_code : list asm_instructions) (post_t_pc : ℕ) on s_stack :
98All … (λx.post_labelled_return_instr … (\snd x)) s_stack → Prop ≝
99match s_stack return λx.All ?? x → ? with
100[ nil ⇒ λ_.stack_t = nil ? (*stati finali to be fixed*)
101| cons hd tl ⇒ λprf.
102  (match hd return λx.hd = x → ? with
103  [ mk_Prod act code ⇒ λEQ.
104    match act with
105    [ call_act f lab ⇒ False
106    | ret_act opt_l ⇒ ∃pc :ℕ.∃stl : list ℕ.stack_t = pc :: stl ∧
107                    let 〈ts_code,ret_label〉 ≝ trans_mono_stack_instr code pc ? in
108                    ∃pre_pc,post_pc.t_code = pre_pc @ ts_code @post_pc ∧ (|pre_pc|) = pc ∧
109                    mono_asm_state_rel_aux tl stl post_pc t_code (pc + |ts_code|) (proj2 … prf)
110    | cost_act opt_l ⇒ let 〈ts_code,ret_label〉 ≝ trans_mono_stack_instr code post_t_pc ? in
111                     (∃post_pc.post_t = ts_code @ post_pc ∧
112                         mono_asm_state_rel_aux tl stack_t post_pc t_code (post_t_pc + |ts_code|) (proj2 … prf))
113                     ∨
114                     (∃new_pc.nth_opt … O post_t = return (Ijmp … new_pc) ∧
115                      ∃pre_pc,post_pc.t_code = pre_pc @ ts_code @post_pc ∧ (|pre_pc|) = new_pc ∧
116                      mono_asm_state_rel_aux tl stack_t post_pc t_code (new_pc + |ts_code|) (proj2 … prf))
117    ]
118  ])(refl …)
119].
120@hide_prf >EQ in prf; * // qed.
121
122definition mono_asm_state_rel : ∀s_code : mono_stack_Instructions.
123∀s_stack : list ((ActionLabel flat_labels) × mono_stack_Instructions).
124ℕ → stackT → list asm_instructions → ? → post_labelled_return_instr … s_code →
125All … (λx.post_labelled_return_instr … (\snd x)) s_stack → Prop ≝ 
126λs_code,s_stack,pc,t_stack,t_code,init_act,prf1,prf2.
127let 〈ts_code,ret_label〉 ≝ trans_mono_stack_instr s_code pc prf1 in
128∃pre_pc,post_t.t_code = pre_pc @ ts_code @ post_t ∧ (|pre_pc|) = pc ∧
129∃chop_stack.s_stack = chop_stack @ [〈init_act,EMPTY …〉] ∧
130 (All … (λx.let 〈act,code〉 ≝ x in is_cost_label … act → (bool_to_Prop (is_silent_cost_act_b … act))) chop_stack) ∧
131 mono_asm_state_rel_aux s_stack t_stack post_t t_code (pc + |ts_code|) prf2.
132
133definition monostack_asm_pass_rel :
134∀prog : Program stack_env_params stack_instr_params flat_labels.
135∀no_dup : no_duplicates_labels … prog.∀prf : post_labelled_return_program … prog.
136let t_prog ≝ trans_mono_stack_prog prog no_dup prf in
137∀bound.
138relations flat_labels
139(operational_semantics mono_stack_state_params (mono_stack_sem_state_params bound) prog)
140(asm_operational_semantics … (asm_sem_params) t_prog) ≝
141λprog,no_dup,prf,bound.
142let t_prog ≝ trans_mono_stack_prog prog no_dup prf in
143(mk_relations flat_labels (operational_semantics mono_stack_state_params (mono_stack_sem_state_params bound) prog)
144 (asm_operational_semantics … (asm_sem_params) t_prog)
145 (λs1,s2.
146   match s2 with
147   [ INITIAL ⇒ bool_to_Prop (lang_initial … (mono_stack_sem_state_params bound) prog s1)
148   | FINAL ⇒ bool_to_Prop (lang_final … s1)
149   | STATE s2' ⇒ store … s1 = (\fst (asm_store … s2')) ∧ ∃prf1 : post_labelled_return_instr … (code … s1).
150                 ∃prf2 : All … (λx.post_labelled_return_instr … (\snd x)) (cont … s1).
151                 mono_asm_state_rel (code … s1) (cont … s1) (pc … s2') (asm_stack … s2') (instructions … t_prog)
152                   (cost_act … (Some ? (initial_act … prog))) prf1 prf2
153   ]
154  )
155 (λ_.λ_.True)).
156
157
158definition mono_stack_asm_pass : ∀prog : Program stack_env_params stack_instr_params flat_labels.
159∀no_dup : no_duplicates_labels … prog.∀prf : post_labelled_return_program … prog.
160let t_prog ≝ trans_mono_stack_prog prog no_dup prf in
161∀bound.simulation_conditions … (monostack_asm_pass_rel prog no_dup prf bound) ≝
162λprog,no_dup,prf,bound.mk_simulation_conditions ….
163[4: #s1 #s1' #s2 #H inversion H
164  [ #st1 #st2 * #act #instr #tl #EQcode_st1 #EQcont_st1 #EQ1 #EQ2 destruct #EQstore #Hio1 #Hio2
165    #no_ret #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in ⊢ (% → ?); cases s1' -s1' normalize nodelta
166    [ whd in match lang_initial; normalize nodelta #H cases(andb_Prop_true … H) -H
167      #H cases(andb_Prop_true … H) -H #H cases(andb_Prop_true … H) -H #_ inversion(eqb_list ???) [2: #_ *]
168      #ABS @⊥ >EQcont_st1 in ABS; normalize #EQ destruct
169    | whd in match lang_final; normalize nodelta #H cases(andb_Prop_true … H) -H #_ >EQcont_st1 *
170    ]
171    #st2' * #EQstore1 * #post_label1 * #post_label2 whd in match mono_asm_state_rel; normalize nodelta lapply post_label1
172    >EQcode_st1 * whd in match (trans_mono_stack_instr ???); normalize nodelta
173    * #pre_pc * #post_t ** #EQinstructions #EQpc ** [|#chop_hd #chop_tail] **
174    [ >EQcont_st1 in ⊢ (% → ?); | >EQcont_st1 in ⊢ (% → ?); ] whd in ⊢ (??%% → ?); #EQ destruct -EQ
175    * #_ #Hchop_tail >EQcont_st1 in post_label2; * #post_code_st2 #post_tail
176    whd in match (mono_asm_state_rel_aux ??????); @pair_elim #t_code_st2 #t_ret_st2
177    whd in match (length ??); <plus_n_O #EQt_code_st2
178    *
179    [ * #post_pc1 * #EQ destruct #Haux #class1 #class2 %{(STATE … st2')} %{(t_base …)} % [2: %2 normalize % *]
180      whd  % [ <EQstore1 //] %{post_code_st2} %{post_tail} whd >EQt_code_st2
181      normalize nodelta %{pre_pc} %{post_pc1} % [ % // >EQinstructions %] %{chop_tail} %
182      [ % //] assumption
183    | * #new_pc * #EQnew_pc * #pre_pc * #post_pc ** #EQinstructions1 #EQ destruct #Hcont #class1 #class2
184      %{(STATE … (mk_vm_state … (|pre_pc|) (asm_stack … st2') (asm_store … st2') (asm_is_io … st2')))}
185      %{(t_ind … (cost_act … (None ?)) … (t_base …))}
186      [ whd <EQpc % [ cases daemon (* BOH!!! *) ] @(vm_ijump … (|pre_pc|)) // [2: cases daemon (* TODO ???*) ]
187      whd in match fetch; normalize nodelta >EQinstructions >nth_second <EQpc [2: //] <minus_n_n assumption ]     
188      % [2: %1 %2 cases daemon ] whd % [ <EQstore //] %{post_code_st2} %{post_tail} whd @pair_elim #p1 #p2
189      <EQpc in EQt_code_st2; #EQt_code_st2
190      cut (∀a,b,c,c'. trans_mono_stack_instr a b c = trans_mono_stack_instr a b c')
191      [ #a #b #c #d % ] #KK >KK [ <EQt_code_st2
192     
193       #K lapply (trans_eq ???? (sym_eq … EQt_code_st2) K)
194     
195       >EQt_code_st2 in ⊢ (% → ?);
196      normalize nodelta
197  |*: cases daemon
198  ]
199]
200cases daemon
201qed.
Note: See TracBrowser for help on using the repository browser.