Changeset 3578
- Timestamp:
- Jul 1, 2015, 11:45:08 PM (6 years ago)
- Location:
- LTS
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/imp.ma
r3575 r3578 60 60 expr ≡ carr X. 61 61 62 (* ambigous input? why?62 (* 63 63 unification hint 0 ≔ p1,p2; 64 64 X ≟ DeqExpr -
LTS/monostack_to_asm_pass.ma
r3574 r3578 94 94 qed. 95 95 96 97 98 96 let rec mono_asm_state_rel_aux (s_stack : list ((ActionLabel flat_labels) × mono_stack_Instructions)) (stack_t : stackT) 99 97 (post_t : list asm_instructions) (t_code : list asm_instructions) (post_t_pc : ℕ) on s_stack : … … 114 112 mono_asm_state_rel_aux tl stack_t post_pc t_code (post_t_pc + |ts_code|) (proj2 … prf)) 115 113 ∨ 116 (∃new_pc. option_hd …post_t = return (Ijmp … new_pc) ∧114 (∃new_pc.nth_opt … O post_t = return (Ijmp … new_pc) ∧ 117 115 ∃pre_pc,post_pc.t_code = pre_pc @ ts_code @post_pc ∧ (|pre_pc|) = new_pc ∧ 118 116 mono_asm_state_rel_aux tl stack_t post_pc t_code (new_pc + |ts_code|) (proj2 … prf)) … … 124 122 definition mono_asm_state_rel : ∀s_code : mono_stack_Instructions. 125 123 ∀s_stack : list ((ActionLabel flat_labels) × mono_stack_Instructions). 126 ℕ → stackT → list asm_instructions → post_labelled_return_instr … s_code →124 ℕ → stackT → list asm_instructions → ? → post_labelled_return_instr … s_code → 127 125 All … (λx.post_labelled_return_instr … (\snd x)) s_stack → Prop ≝ 128 λs_code,s_stack,pc,t_stack,t_code, prf1,prf2.126 λs_code,s_stack,pc,t_stack,t_code,init_act,prf1,prf2. 129 127 let 〈ts_code,ret_label〉 ≝ trans_mono_stack_instr s_code pc prf1 in 130 128 ∃pre_pc,post_t.t_code = pre_pc @ ts_code @ post_t ∧ (|pre_pc|) = pc ∧ 131 (All … (λx.let 〈act,code〉 ≝ x in is_cost_label … act → (bool_to_Prop (is_silent_cost_act_b … act))) s_stack) ∧ 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) ∧ 132 131 mono_asm_state_rel_aux s_stack t_stack post_t t_code (pc + |ts_code|) prf2. 133 132 134 133 definition monostack_asm_pass_rel : 135 134 ∀prog : Program stack_env_params stack_instr_params flat_labels. … … 144 143 (mk_relations flat_labels (operational_semantics mono_stack_state_params (mono_stack_sem_state_params bound) prog) 145 144 (asm_operational_semantics … (asm_sem_params) t_prog) 146 (λs1,s2.∃s2'.s2 = STATE … s2' ∧ store … s1 = (\fst (asm_store … s2')) ∧ ∃prf1 : post_labelled_return_instr … (code … s1). 147 ∃prf2 : All … (λx.post_labelled_return_instr … (\snd x)) (cont … s1). 148 mono_asm_state_rel (code … s1) (cont … s1) (pc … s2') (asm_stack … s2') (instructions … t_prog) prf1 prf2 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 ] 149 154 ) 150 155 (λ_.λ_.True)). … … 158 163 [4: #s1 #s1' #s2 #H inversion H 159 164 [ #st1 #st2 * #act #instr #tl #EQcode_st1 #EQcont_st1 #EQ1 #EQ2 destruct #EQstore #Hio1 #Hio2 160 #no_ret #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in ⊢ (% → ?); * #st2' ** #EQ destruct #EQstore1 161 * #post_label1 * #post_label2 whd in match mono_asm_state_rel; normalize nodelta lapply post_label1 >EQcode_st1 162 * whd in match (trans_mono_stack_instr ???); normalize nodelta 163 * #pre_pc * #post_t *** #EQinstructions #EQpc lapply post_label2 164 -post_label2 >EQcont_st1 * #post_code_st2 #post_tail * #_ #Hcont_cost 165 whd in match (mono_asm_state_rel_aux ??????); @pair_elim #t_code_st2 #t_ret_st2 whd in match (length ??); 166 <plus_n_O #EQt_code_st2 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 167 178 * 168 179 [ * #post_pc1 * #EQ destruct #Haux #class1 #class2 %{(STATE … st2')} %{(t_base …)} % [2: %2 normalize % *] 169 whd %{st2'} % [ %{(refl …)} <EQstore1 //] %{post_code_st2} %{post_tail} whd >EQt_code_st2 170 normalize nodelta %{pre_pc} %{post_pc1} % [ % // % // >EQinstructions %] assumption 171 | cases daemon 172 ] 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 173 197 |*: cases daemon 174 198 ] -
LTS/variable_stack_pass.ma
r3577 r3578 203 203 qed. 204 204 205 (* 206 let rec create_silent_trace_from_eval_combinators (st : (l : list guard_combinators) 207 (prf: m_fold Option … eval_combinators l st = return st') 208 *) 205 definition safe_cast : ∀A,B : Type[0].A = B → A → B ≝ 206 λA,B,prf.match prf with [refl ⇒ λx : A.x]. 207 208 let rec create_silent_trace_from_eval_combinators (prog : Program stack_env_params stack_instr_params flat_labels) 209 (bound : ℕ) (st,st' : state stack_state_params) (l : list guard_combinators) 210 on l : 211 m_fold Option … eval_combinators l (store … st) = return (store … st') → 212 code … st = list_combinators_to_instructions l (code … st') → 213 cont … st = cont … st' → io_info … st = io_info … st' → 214 raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st' ≝ 215 match l return λx.(m_fold Option … eval_combinators x ? = ? → ? = list_combinators_to_instructions x ? → ?) with 216 [ nil ⇒ λprf1,prf2,prf3,prf4.safe_cast (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st) 217 (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st') ? (t_base ?? st) 218 | cons x xs ⇒ λprf1,prf2,prf3,prf4. 219 let next_store ≝ (opt_safe … (eval_combinators x (store … st)) ?) in 220 let next_st ≝ mk_state stack_state_params (list_combinators_to_instructions xs (code … st')) (cont … st') 221 next_store (io_info … st') in 222 let tail ≝ create_silent_trace_from_eval_combinators prog bound next_st st' xs ? (refl …) (refl …) (refl …) in 223 t_ind … (cost_act … (None ?)) … tail 224 ]. 225 @hide_prf 226 [ cases st in prf1 prf2 prf3 prf4; cases st' #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 whd in H9 : (??%%); 227 whd in H10 : (??%%); destruct % 228 |4: change with (m_bind ?????) in prf1 :(??%?); cases(bind_inversion ????? prf1) -prf1 #w * #EQw #_ >EQw % 229 whd in ⊢ (??%% → ?); #EQ destruct 230 | whd @seq_sil 231 [4: >prf2 in ⊢ (??%?); % 232 |8: % 233 |5: change with (eval_combinators ??) in ⊢ (??%?); normalize nodelta @opt_safe_elim #w #H assumption 234 |6: % 235 |7: assumption 236 |9,10: cases daemon (*io*) 237 |*: 238 ] 239 | normalize nodelta @opt_safe_elim #w #EQw change with (m_bind ?????) in prf1 :(??%?); >EQw in prf1; 240 >m_return_bind // 241 ] 242 qed. 243 244 lemma create_silent_trace_from_eval_combinators_ok : ∀prog,bound,st,st',l,prf1,prf2,prf3,prf4,t. 245 create_silent_trace_from_eval_combinators prog bound st st' l prf1 prf2 prf3 prf4 = t → 246 pre_silent_trace … t. 247 #prog #bound #st #st' #l lapply st -st lapply st' -st' elim l 248 [ * #code' #cont' #store' #io' * #code #cont #store #io whd in ⊢ (??%% → ??%% → ?); #EQ destruct #EQ1 #EQ2 #EQ3 destruct 249 #t whd in ⊢ (??%% → ?); #EQ destruct % cases daemon (*io*) 250 | #x #xs #IH #st' #st #H cases(bind_inversion ????? H) #w * #EQw #EQstore_st' 251 whd in ⊢ (???% → ?); change with (list_combinators_to_instructions ??) in match (foldr ?????); 252 #prf2 #EQcont #EQio #t whd in ⊢ (??%? → ?); #EQ destruct %2 [cases daemon (* io *)] @IH [|*: %] 253 ] 254 qed. 255 256 (* [ @opt_safe_elim #w' >EQw whd in ⊢ (??%% → ?); #EQ destruct assumption 257 | % 258 | % c'e' un baco????*) 209 259 210 260 definition simulation_imp_frame :
Note: See TracChangeset
for help on using the changeset viewer.