Legend:
- Unmodified
- Added
- Removed
-
LTS/Vm.ma
r3457 r3463 29 29 | Iret: AssemblerInstr p. 30 30 31 definition AssemblerProgram ≝λp.list (AssemblerInstr p) × ℕ. 31 record AssemblerProgram (p : assembler_params) : Type[0] ≝ 32 { instructions : list (AssemblerInstr p) 33 ; endmain : ℕ 34 ; endmain_ok : endmain ≤ |instructions| 35 }. 32 36 33 37 definition fetch: ∀p.AssemblerProgram p → ℕ → option (AssemblerInstr p) ≝ 34 λp,l,n. nth_opt ? n ( \fstl).38 λp,l,n. nth_opt ? n (instructions … l). 35 39 36 40 definition stackT: Type[0] ≝ list (nat). … … 43 47 ; eval_asm_io : io_instr p → asm_store_type → option asm_store_type 44 48 ; cost_of_io : io_instr p → asm_store_type → m 45 ; cost_of : AssemblerInstr p → m49 ; cost_of : AssemblerInstr p → asm_store_type → m 46 50 }. 47 51 … … 73 77 asm_is_io … st1 = asm_is_io … st2 → 74 78 S (pc … st1) = pc … st2 → 75 op … (cost … st1) (cost_of p p' (Seq p i l) ) = cost … st2 →79 op … (cost … st1) (cost_of p p' (Seq p i l) (asm_store … st1)) = cost … st2 → 76 80 vmstep … (cost_act l) st1 st2 77 81 | vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ. … … 82 86 asm_is_io … st1 = asm_is_io … st2 → 83 87 new_pc = pc … st2 → 84 op … (cost … st1) (cost_of p p' (Ijmp … new_pc) ) = cost … st2 →88 op … (cost … st1) (cost_of p p' (Ijmp … new_pc) (asm_store … st1)) = cost … st2 → 85 89 vmstep … (cost_act (None ?)) st1 st2 86 90 | vm_cjump_true : … … 93 97 asm_is_io … st1 = asm_is_io … st2 → 94 98 pc … st2 = new_pc → 95 op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse) ) = cost … st2 →99 op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 → 96 100 vmstep … (cost_act (Some ? ltrue)) st1 st2 97 101 | vm_cjump_false : … … 104 108 asm_is_io … st1 = asm_is_io … st2 → 105 109 S (pc … st1) = pc … st2 → 106 op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse) ) = cost … st2 →110 op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 → 107 111 vmstep … (cost_act (Some ? lfalse)) st1 st2 108 112 | vm_io_in : … … 134 138 asm_is_io … st1 = asm_is_io … st2 → 135 139 entry_of_function p f = pc … st2 → 136 op … (cost … st1) (cost_of p p' (Icall p f) ) = cost … st2 →140 op … (cost … st1) (cost_of p p' (Icall p f) (asm_store … st1)) = cost … st2 → 137 141 label_of_pc ? (call_label_fun p) (entry_of_function p f) = return lbl → 138 142 vmstep … (call_act f lbl) st1 st2 … … 146 150 newpc = pc … st2 → 147 151 label_of_pc ? (return_label_fun p) newpc = return lbl → 148 op … (cost … st1) (cost_of p p' (Iret p) ) = cost … st2 →152 op … (cost … st1) (cost_of p p' (Iret p) (asm_store … st1)) = cost … st2 → 149 153 vmstep … (ret_act (Some ? lbl)) st1 st2. 150 154 … … 161 165 return 〈cost_act opt_l, 162 166 mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false 163 (op … (cost … st) (cost_of p p' (Seq p x opt_l) ))〉167 (op … (cost … st) (cost_of p p' (Seq p x opt_l) (asm_store … st)))〉 164 168 | Ijmp newpc ⇒ 165 169 if asm_is_io … st then … … 168 172 return 〈cost_act (None ?), 169 173 mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false 170 (op … (cost … st) (cost_of p p' (Ijmp … newpc) ))〉174 (op … (cost … st) (cost_of p p' (Ijmp … newpc) (asm_store … st)))〉 171 175 | CJump cond newpc ltrue lfalse ⇒ 172 176 if asm_is_io … st then … … 177 181 return 〈cost_act (Some ? ltrue), 178 182 mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false 179 (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) ))〉183 (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉 180 184 else 181 185 return 〈cost_act (Some ? lfalse), 182 186 mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false 183 (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) ))〉187 (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉 184 188 | Iio lin io lout ⇒ 185 189 if asm_is_io … st then … … 203 207 ((S (pc … st)) :: (asm_stack … st)) 204 208 (asm_store … st) false 205 (op … (cost … st) (cost_of p p' (Icall p f) ))〉209 (op … (cost … st) (cost_of p p' (Icall p f) (asm_store … st)))〉 206 210 | Iret ⇒ if asm_is_io … st then 207 211 None ? … … 211 215 return 〈ret_act (Some ? lbl), 212 216 mk_vm_state ?? newpc tl (asm_store … st) false 213 (op … (cost … st) (cost_of p p' (Iret p) ))〉217 (op … (cost … st) (cost_of p p' (Iret p) (asm_store … st)))〉 214 218 ]. 215 219 … … 245 249 qed. 246 250 251 252 lemma vm_step_to_eval : ∀p,p',prog,st1,st2,l.vmstep … prog l st1 st2 → 253 eval_vmstate p p' prog st1 = return 〈l,st2〉. 254 #p #p' #prog * #pc1 #stack1 #store1 #io1 #cost1 255 * #pc2 #stack2 #store2 #io2 #cost2 #l #H inversion H 256 [ #s1 #s2 #i #opt_l #EQfetch #EQio #EQstore #EQstack #EQio1 #EQpc #EQcost 257 #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta 258 >EQfetch >m_return_bind normalize nodelta >EQio normalize nodelta >EQstore 259 >m_return_bind <EQio1 >EQio <EQpc >EQstack >EQcost % 260 | #s1 #s2 #newpc #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc #EQcost 261 #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta 262 >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta <EQio2 >EQio1 263 >EQstore >EQstack <EQcost >EQstore % 264 |3,4: #s1 #s2 #cond #newoc #ltrue #lfalse #EQev_cond #EQfetch #EQio1 #EQstore 265 #EQstack #EQio2 #EQnewoc #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct 266 whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind 267 normalize nodelta >EQio1 normalize nodelta >EQev_cond >m_return_bind 268 normalize nodelta <EQio1 >EQio2 >EQstore >EQstack <EQcost >EQstore [%] >EQnewoc % 269 |5,6: #s1 #s2 #lin #io #lout #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQpc 270 #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; 271 normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 272 normalize nodelta >EQstack <EQpc >EQcost [ >EQstore <EQio2 %] 273 >EQstore >m_return_bind <EQpc <EQio2 % 274 | #s1 #s2 #f #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQentry 275 #EQcost #EQlab_pc #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; 276 normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 277 normalize nodelta >EQlab_pc >m_return_bind >EQentry >EQcost <EQio2 >EQio1 278 <EQstack >EQstore % 279 | #s1 #s2 #newpc #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc 280 #EQlab_pc #EQcosts #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; 281 normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta 282 >EQstack whd in match option_pop; normalize nodelta >m_return_bind 283 >EQlab_pc >m_return_bind >EQcosts >EQstore <EQio2 >EQio1 % 284 ] 285 qed. 286 287 coercion vm_step_to_eval. 288 247 289 include "../src/utilities/hide.ma". 248 290 … … 252 294 λp,p',prog.mk_abstract_status 253 295 (vm_state p p') 254 (λl.λst1,st2 : vm_state p p'.(eqb (pc ?? st1) ( \sndprog)) = false ∧296 (λl.λst1,st2 : vm_state p p'.(eqb (pc ?? st1) (endmain … prog)) = false ∧ 255 297 vmstep p p' prog l st1 st2) 256 298 (λ_.λ_.True) … … 269 311 (λ_.true) 270 312 (λs.eqb (pc ?? s) O) 271 (λs.eqb (pc … s) ( \sndprog))313 (λs.eqb (pc … s) (endmain … prog)) 272 314 ???. 273 @hide_prf cases daemon (*315 @hide_prf 274 316 [ #s1 #s2 #l inversion(fetch ???) normalize nodelta 275 317 [ #_ #EQ destruct] * normalize nodelta … … 281 323 | #_ 282 324 ] 283 #EQ destruct * #_ #H inversion H in ⊢ ?; 284 [ #st1 #st2 #i #lbl #EQ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 285 | #st1 #st2 #new_pc #EQ #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 286 | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 287 | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 288 | #st1 #st2 #lin #io #lout #EQ #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 289 | #st1 #st2 #lin #io #lout #EQ #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 290 | #st1 #st2 #f #EQ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 291 | #st1 #st2 #new_pc #EQ #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 292 ] 293 destruct >EQfetch in EQ; whd in ⊢ (??%% → ?); #EQ 294 lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct % // 325 #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate; 326 normalize nodelta >EQfetch >m_return_bind normalize nodelta cases(asm_is_io ??) 327 normalize nodelta [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H 328 * * #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct % // 295 329 | #s1 #s2 #l inversion(fetch ???) normalize nodelta 296 330 [ #_ #EQ destruct] * normalize nodelta … … 302 336 | #_ 303 337 ] 304 #EQ destruct * #_ #H inversion H in ⊢ ?; 305 [ #st1 #st2 #i #lbl #EQf #EQio1 #H2 #H3 #H4 #EQio2 #H6 #H7 #H8 #H9 #H10 #H11 306 | #st1 #st2 #new_pc #EQf #EQio1 #H13 #H14 #H15 #EQio2 #H17 #H18 #H19 #H20 #H21 #H22 307 | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQf #EQio1 #H26 #H27 #H28 #EQio2 #H30 #H31 #H32 #H33 #H34 #H35 308 | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQf #EQio1 #H38 #H39 #H40 #EQio2 #H42 #H43 #H44 #H45 #H46 #H47 309 | #st1 #st2 #lin #io #lout #EQf #EQio1 #H50 #H51 #H52 #EQio2 #H54 #H55 #H56 #H57 #H58 #H59 310 | #st1 #st2 #lin #io #lout #EQf #EQio1 #H61 #H62 #H63 #EQio2 #H65 #H66 #H67 #H68 #H69 #H70 311 | #st1 #st2 #f #EQf #EQio1 #H74 #H75 #H76 #EQio2 #H78 #H79 #H80 #H81 #H82 #H83 312 | #st1 #st2 #new_pc #EQf #EQio1 #H86 #H87 #H88 #EQio2 #H90 #H91 #H92 #H93 #H94 #H95 313 ] 314 destruct >EQio in EQio2; >EQio1 #EQ destruct %{lin} // 338 #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate; 339 normalize nodelta #H cases(bind_inversion ????? H) -H * 340 [ #seq1 #lbl1 341 | #n1 342 | #cond1 #newpc1 #ltrue1 #lfalse1 343 | #lin1 #io1 #lout1 344 | #f 345 | 346 ] 347 normalize nodelta * #_ cases(asm_is_io ??) normalize nodelta 348 [1,3,5,9,11: whd in ⊢ (??%% → ?); #EQ destruct 349 |2,6,7,10,12: #H cases(bind_inversion ????? H) -H #x * #_ 350 [2: cases x normalize nodelta 351 |5: #H cases(bind_inversion ????? H) -H #y * #_ 352 ] 353 ] 354 whd in ⊢ (??%% → ?); #EQ destruct destruct % // 315 355 | #s1 #s2 #l inversion(fetch ???) normalize nodelta 316 356 [ #_ #EQ destruct] * normalize nodelta 317 357 [ #seq #lbl #_ 318 358 | #n #_ 319 | #cond #newpc #ltrue #lfalse # EQfetch320 | #lin #io #lout #EQfetch cases (asm_is_io ??) normalize nodelta359 | #cond #newpc #ltrue #lfalse #_ 360 | #lin #io #lout #EQfetch inversion(asm_is_io ??) normalize nodelta #EQio 321 361 | #f #_ 322 362 | #_ 323 363 ] 324 #EQ destruct * #_ #H inversion H in ⊢ ?; 325 [ #st1 #st2 #i #lbl #EQ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 326 | #st1 #st2 #new_pc #EQ #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 327 | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 328 | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 329 | #st1 #st2 #lin1 #io1 #lout1 #EQ #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 330 | #st1 #st2 #lin1 #io1 #lout1 #EQ #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 331 | #st1 #st2 #f #EQ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 332 | #st1 #st2 #new_pc #EQ #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 333 ] 334 destruct >EQfetch in EQ; whd in ⊢ (??%% → ?); #EQ 335 lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct % // 336 ]*) 364 #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate; 365 normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio 366 normalize nodelta #H cases(bind_inversion ????? H) -H #x * #_ 367 whd in ⊢ (??%% → ?); #EQ destruct % // 337 368 qed. 338 369 … … 358 389 … (fetch_state p p' prog) instr_m. 359 390 391 definition non_empty_list : ∀A.list A → bool ≝ 392 λA,l.match l with [ nil ⇒ false | _ ⇒ true ]. 360 393 361 394 let rec block_cost (p : assembler_params) … … 368 401 [ O ⇒ None ? 369 402 | S program_size' ⇒ 370 if eqb program_counter ( \sndprog) then403 if eqb program_counter (endmain … prog) then 371 404 return e … abs_t 372 405 else … … 379 412 ]. 380 413 381 axiom initial_act : CostLabel. 414 inductive InitCostLabel : Type[0] ≝ 415 costlab : CostLabel → InitCostLabel 416 | initial_act : InitCostLabel. 417 418 definition eq_init_costlabel ≝ (λi1,i2.match i1 with 419 [ initial_act ⇒ match i2 with [initial_act ⇒ true | _ ⇒ false ] 420 | costlab c ⇒ match i2 with [costlab c1 ⇒ c == c1 | _ ⇒ false ] 421 ]). 422 423 definition DEQInitCostLabel ≝ mk_DeqSet InitCostLabel eq_init_costlabel ?. 424 * [#c] * [1,3: #c1] whd in match eq_init_costlabel; normalize nodelta 425 [4: /2/ | 2,3: % #EQ destruct] % [ #H >(\P H) % | #EQ destruct >(\b (refl …)) %] 426 qed. 427 428 coercion costlab. 429 430 definition list_cost_to_list_initcost : list CostLabel → list InitCostLabel ≝ 431 map … costlab. 432 433 coercion list_cost_to_list_initcost. 382 434 383 435 record cost_map_T (dom : DeqSet) (codom : Type[0]) : Type[1] ≝ … … 390 442 }. 391 443 392 let rec labels_pc (p : assembler_params) 393 (prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝ 394 match prog with 395 [ nil ⇒ [〈initial_act,O〉] @ 396 map … (λx.let〈y,z〉 ≝ x in 〈a_call z,y〉) (call_label_fun … p) @ 397 map … (λx.let〈y,z〉 ≝ x in 〈a_return_post z,y〉) (return_label_fun … p) 398 | cons i is ⇒ 399 match i with 444 definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (InitCostLabel × ℕ) ≝ 445 λp,i,program_counter. 446 match i with 400 447 [ Seq _ opt_l ⇒ match opt_l with 401 [ Some lbl ⇒ [〈 a_non_functional_label lbl,S program_counter〉]448 [ Some lbl ⇒ [〈costlab (a_non_functional_label lbl),S program_counter〉] 402 449 | None ⇒ [ ] 403 450 ] 404 451 | Ijmp _ ⇒ [ ] 405 | CJump _ newpc ltrue lfalse ⇒ [〈a_non_functional_label ltrue,newpc〉;〈a_non_functional_label lfalse,S program_counter〉] 406 | Iio lin _ lout ⇒ [〈a_non_functional_label lout,S program_counter〉] 452 | CJump _ newpc ltrue lfalse ⇒ [〈costlab (a_non_functional_label ltrue),newpc〉; 453 〈costlab (a_non_functional_label lfalse),S program_counter〉] 454 | Iio lin _ lout ⇒ [〈costlab (a_non_functional_label lin),program_counter〉; 455 〈costlab (a_non_functional_label lout),S program_counter〉] 407 456 | Icall f ⇒ [ ] 408 457 | Iret ⇒ [ ] 409 ] @ labels_pc p is (S program_counter) 458 ]. 459 460 let rec labels_pc (p : assembler_params) 461 (prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (InitCostLabel × ℕ) ≝ 462 match prog with 463 [ nil ⇒ [〈initial_act,O〉] @ 464 map … (λx.let〈y,z〉 ≝ x in 〈costlab (a_call z),y〉) (call_label_fun … p) @ 465 map … (λx.let〈y,z〉 ≝ x in 〈costlab (a_return_post z),y〉) (return_label_fun … p) 466 | cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p is (S program_counter) 410 467 ]. 411 468 469 lemma labels_pc_ok : ∀p,prog,i,lbl,pc,m. 470 fetch p prog pc = return i → 471 mem ? lbl (labels_pc_of_instr … i (m+pc)) → 472 mem ? lbl (labels_pc p (instructions … prog) m). 473 #p * #instrs #end_main #Hend_main #i #lbl #pc 474 whd in match fetch; normalize nodelta lapply pc -pc 475 -end_main elim instrs 476 [ #pc #m whd in ⊢ (??%% → ?); #EQ destruct] 477 #x #xs #IH * [|#pc'] #m whd in ⊢ (??%% → ?); 478 [ #EQ destruct #lbl_addr whd in match (labels_pc ???); 479 /2 by mem_append_l1/ 480 | #EQ #H2 whd in match (labels_pc ???); @mem_append_l2 @(IH … EQ) // 481 ] 482 qed. 483 484 lemma labels_pc_return: ∀p,prog,x1,x2. 485 label_of_pc ReturnPostCostLabel (return_label_fun p) x1=return x2 → 486 ∀m. 487 mem … 〈costlab (a_return_post x2),x1〉 (labels_pc p (instructions p prog) m). 488 #p * #l #endmain #_ whd in match (labels_pc ???); #x1 #x2 #H elim l 489 [ #m @mem_append_l2 @mem_append_l2 whd in H:(??%?); 490 elim (return_label_fun ?) in H; [ whd in ⊢ (??%% → ?); #EQ destruct] 491 * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim 492 normalize nodelta 493 [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/ 494 | #NEQ #H2 %2 @IH // ] 495 | #hd #tl #IH #m @mem_append_l2 @IH ] 496 qed. 497 498 lemma labels_pc_call: ∀p,prog,x1,x2. 499 label_of_pc CallCostLabel (call_label_fun p) x1=return x2 → 500 ∀m. 501 mem … 〈costlab (a_call x2),x1〉 (labels_pc p (instructions p prog) m). 502 #p * #l #endmain #_ whd in match (labels_pc ???); #x1 #x2 #H elim l 503 [ #m @mem_append_l2 @mem_append_l1 whd in H:(??%?); 504 elim (call_label_fun ?) in H; [ whd in ⊢ (??%% → ?); #EQ destruct] 505 * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim 506 normalize nodelta 507 [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/ 508 | #NEQ #H2 %2 @IH // ] 509 | #hd #tl #IH #m @mem_append_l2 @IH ] 510 qed. 511 512 unification hint 0 ≔ ; 513 X ≟ DEQInitCostLabel 514 (* ---------------------------------------- *) ⊢ 515 InitCostLabel ≡ carr X. 516 517 518 unification hint 0 ≔ p1,p2; 519 X ≟ DEQInitCostLabel 520 (* ---------------------------------------- *) ⊢ 521 eq_init_costlabel p1 p2 ≡ eqb X p1 p2. 522 523 524 let rec m_foldr (M : Monad) (X,Y : Type[0]) (f : X→Y→M Y) (l : list X) (y : Y) on l : M Y ≝ 525 match l with 526 [ nil ⇒ return y 527 | cons x xs ⇒ ! z ← m_foldr M X Y f xs y; f x z 528 ]. 529 412 530 definition static_analisys : ∀p : assembler_params.∀abs_t : monoid.(AssemblerInstr p → abs_t) → 413 ∀mT : cost_map_T DEQ CostLabel abs_t.AssemblerProgram p → option mT ≝531 ∀mT : cost_map_T DEQInitCostLabel abs_t.AssemblerProgram p → option mT ≝ 414 532 λp,abs_t,instr_m,mT,prog. 415 let 〈instrs,final〉 ≝ prog in 416 let prog_size ≝ S (|instrs|) in 417 m_fold Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m w prog_size; 418 return set_map … m z k) (labels_pc … instrs O) 419 (empty_map ?? mT). 533 let prog_size ≝ S (|instructions … prog|) in 534 m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m w prog_size; 535 return set_map … m z k) (labels_pc … (instructions … prog) O) 536 (empty_map ?? mT). 537 538 539 include "basics/lists/listb.ma". 540 541 (*doppione da mettere a posto*) 542 let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝ 543 match l with 544 [ nil ⇒ True 545 | cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs 546 ]. 547 548 definition asm_no_duplicates ≝ 549 λp,prog.no_duplicates … (map ?? \fst … (labels_pc … (instructions p prog) O)). 420 550 421 551 (*falso: necessita di no_duplicates*) 422 axiom static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map. 552 553 definition eq_deq_prod : ∀D1,D2 : DeqSet.D1 × D2 → D1 × D2 → bool ≝ 554 λD1,D2,x,y.\fst x == \fst y ∧ \snd x == \snd y. 555 556 definition DeqProd ≝ λD1 : DeqSet.λD2 : DeqSet. 557 mk_DeqSet (D1 × D2) (eq_deq_prod D1 D2) ?. 558 @hide_prf 559 * #x1 #x2 * #y1 #y2 whd in match eq_deq_prod; normalize nodelta 560 % [2: #EQ destruct @andb_Prop >(\b (refl …)) %] 561 inversion (? ==?) #EQ1 whd in match (andb ??); #EQ2 destruct 562 >(\P EQ1) >(\P EQ2) % 563 qed. 564 (* 565 unification hint 0 ≔ D1,D2 ; 566 X ≟ DeqProd D1 D2 567 (* ---------------------------------------- *) ⊢ 568 D1 × D2 ≡ carr X. 569 570 571 unification hint 0 ≔ D1,D2,p1,p2; 572 X ≟ DeqProd D1 D2 573 (* ---------------------------------------- *) ⊢ 574 eq_deq_prod D1 D2 p1 p2 ≡ eqb X p1 p2. 575 576 definition deq_prod_to_prod : ∀D1,D2 : DeqSet.DeqProd D1 D2 → D1 × D2 ≝ 577 λD1,D2,x.x. 578 579 coercion deq_prod_to_prod. 580 *) 581 582 lemma map_mem : ∀A,B,f,l,a.mem A a l → ∃b : B.mem B b (map A B f l) 583 ∧ b = f a. 584 #A #B #f #l elim l [ #a *] #x #xs #IH #a * 585 [ #EQ destruct %{(f x)} % // % // | #H cases(IH … H) 586 #b * #H1 #EQ destruct %{(f a)} % // %2 // 587 ] 588 qed. 589 590 lemma static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map. 591 asm_no_duplicates p prog → 423 592 static_analisys p abs_t instr_m mT prog = return map → 424 mem … 〈lbl,pc〉 (labels_pc … (\fst prog) O) → 425 get_map … map lbl = block_cost … prog abs_t instr_m pc (S (|(\fst prog)|)). 593 mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) O) → 594 get_map … map lbl = block_cost … prog abs_t instr_m pc (S (|(instructions … prog)|)). 595 #p #abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta 596 whd in match asm_no_duplicates; normalize nodelta lapply (labels_pc ???) 597 #l #endmain #Hendmain elim l [ #x #y #z #w #h * ] 598 * #hd1 #hd2 #tl #IH #lbl #pc #map * #H1 #H2 #H 599 cases(bind_inversion ????? H) -H #map1 * #EQmap1 normalize nodelta #H 600 cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); #EQ 601 destruct * 602 [ #EQ destruct >get_set_hit >EQelem % 603 | #H >get_set_miss [ @IH //] inversion (? == ?) [2: #_ %] 604 #ABS cases H1 -H1 #H1 @⊥ @H1 >(\P ABS) >mem_to_memb // 605 cases(map_mem … \fst … H) #z1 * #Hz1 #EQ destruct @Hz1 606 ] 607 qed. 426 608 427 609 include "Simulation.ma". … … 437 619 ] 438 620 }. 439 440 axiom vm_step_to_eval : ∀p,p',prog,st1,st2,l.vmstep … prog l st1 st2 →441 eval_vmstate p p' prog st1 = return 〈l,st2〉.442 443 coercion vm_step_to_eval.444 621 445 622 definition big_op: ∀M: monoid. list M → M ≝ … … 472 649 qed. 473 650 474 lemma static_dynamic : ∀p,p',prog. 651 lemma monotonicity_of_block_cost : ∀p,prog,abs_t,instr_m,pc,size,k. 652 block_cost p prog abs_t instr_m pc size = return k → 653 ∀size'.size ≤ size' → 654 block_cost p prog abs_t instr_m pc size' = return k. 655 #p #prog #abs_t #instr_m #pc #size lapply pc elim size 656 [ #pc #k whd in ⊢ (??%% → ?); #EQ destruct] 657 #n #IH #pc #k whd in ⊢ (??%% → ?); @eqb_elim 658 [ #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct 659 #size' * [2: #m #_] whd in ⊢ (??%%); @eqb_elim try( #_ %) * #H @⊥ @H % 660 | #Hpc normalize nodelta #H cases(bind_inversion ????? H) -H #i 661 * #EQi #H cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); 662 #EQ destruct #size' * 663 [ whd in ⊢ (??%?); @eqb_elim 664 [ #EQ @⊥ @(absurd ?? Hpc) assumption ] 665 #_ normalize nodelta >EQi >m_return_bind >EQelem % 666 | #m #Hm whd in ⊢ (??%?); @eqb_elim 667 [ #EQ @⊥ @(absurd ?? Hpc) assumption ] 668 #_ normalize nodelta >EQi >m_return_bind 669 cases (emits_labels ??) in EQelem; normalize nodelta 670 [ whd in ⊢ (??%%→ ??%%); #EQ destruct %] 671 #f #EQelem >(IH … EQelem) [2: /2/ ] % 672 ] 673 ] 674 qed. 675 676 lemma step_emit : ∀p,p',prog,st1,st2,l,i. 677 fetch p prog (pc … st1) = return i → 678 eval_vmstate p p' … prog st1 = return 〈l,st2〉 → 679 emits_labels … i = None ? → ∃x. 680 match l in ActionLabel return λ_:ActionLabel.(list CostLabel) with 681 [call_act f c ⇒ [a_call c] 682 |ret_act x ⇒ 683 match x with [None⇒[]|Some c⇒[a_return_post c]] 684 |cost_act x ⇒ 685 match x with [None⇒[]|Some c⇒[a_non_functional_label c]] 686 |init_act⇒[ ] 687 ] = [x] ∧ 688 (mem … 〈costlab x,pc … st2〉 (labels_pc p (instructions … prog) O)). 689 #p #p' #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta 690 >EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta 691 [ #seq * [|#lab] 692 | #newpc 693 | #cond #newpc #ltrue #lfalse 694 | #lin #io #lout 695 | #f 696 | 697 ] 698 #EQi cases(asm_is_io ???) normalize nodelta 699 [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct 700 |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1 701 [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta 702 |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2 703 ] 704 ] 705 whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels; 706 normalize nodelta #EQ destruct % [2,4,6,8,10,12,14: % try % |*:] 707 [1,2,4,5,7: @(labels_pc_ok … EQi) normalize /3 by or_introl,or_intror/ ] 708 /2 by labels_pc_return, labels_pc_call/ 709 qed. 710 711 lemma step_non_emit : ∀p,p',prog,st1,st2,l,i,f. 712 fetch p prog (pc … st1) = return i → 713 eval_vmstate p p' … prog st1 = return 〈l,st2〉 → 714 emits_labels … i = Some ? f → 715 match l in ActionLabel return λ_:ActionLabel.(list CostLabel) with 716 [call_act f c ⇒ [a_call c] 717 |ret_act x ⇒ 718 match x with [None⇒[]|Some c⇒[a_return_post c]] 719 |cost_act x ⇒ 720 match x with [None⇒[]|Some c⇒[a_non_functional_label c]] 721 |init_act⇒[ ] 722 ] = [ ] ∧ pc … st2 = f (pc … st1). 723 #p #p' #prog #st1 #st2 #l #i #f #EQi whd in match eval_vmstate; normalize nodelta 724 >EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta 725 [ #seq * [|#lab] 726 | #newpc 727 | #cond #newpc #ltrue #lfalse 728 | #lin #io #lout 729 | #f 730 | 731 ] 732 #EQi cases(asm_is_io ???) normalize nodelta 733 [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct 734 |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1 735 [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta 736 |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2 737 ] 738 ] 739 whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels; 740 normalize nodelta #EQ destruct /2 by refl, conj/ 741 qed. 742 743 744 lemma static_dynamic : ∀p,p',prog.asm_no_duplicates p prog → 475 745 ∀abs_t : abstract_transition_sys (m … p').∀instr_m. 476 746 ∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1. … … 481 751 ∀k. 482 752 pre_measurable_trace … t → 483 block_cost p prog … instr_m (pc … st1) (S (|( \fstprog)|)) = return k →753 block_cost p prog … instr_m (pc … st1) (S (|(instructions … prog)|)) = return k → 484 754 ∀a1.rel_galois … good st1 a1 → 485 755 let stop_state ≝ match R_post_step … ter with [None ⇒ st2 | Some x ⇒ \snd x ] in … … 488 758 rel_galois … good stop_state (act_abs … abs_t (big_op … costs) (act_abs … abs_t k a1)). 489 759 [2: @hide_prf cases daemon] 490 #p #p' #prog # abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #ter #t760 #p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #ter #t 491 761 lapply ter -ter elim t 492 762 [ #st #ter inversion(R_post_step … ter) normalize nodelta [| * #lbl #st3 ] … … 522 792 | -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H 523 793 #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????); 524 whd #costs <map_append #EQ destruct >big_op_associative >act_op @IH 525 [ 526 inversion H in ⊢ ?; 527 [ #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct 528 | #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_ 529 #EQ1 #EQ2 #EQ3 #EQ4 destruct 530 | #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_ 531 #EQ1 #EQ2 #EQ3 #EQ4 destruct 532 | #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct 533 * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 534 | #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H * 535 ] // 536 | whd in H2 : (??%?); >H3 in H2; normalize nodelta #H 537 cases(bind_inversion ????? H) #i * #EQi whd in match (emits_labels ??); 538 539 inversion l [#fn #lbl | * [|#lbl] | * [|#lbl] ] #EQlbl normalize nodelta 540 inversion (R_post_step ???) [|2,4,6,8,10,12,14,16: * #post_lbl #post_state] 541 #EQR_post_step normalize nodelta lapply (IH ter) -IH 542 >EQR_post_step normalize nodelta #IH 543 whd in match (foldl ?????); 544 [ >act_op @IH 545 try (> act_op) 546 547 548 549 550 551 552 whd in ⊢ (??%% → ?); [ >H1 in ⊢ (% → ?); | >H1 in ⊢ (% → ?); | >H1 in ⊢ (% → ?);] 553 normalize nodelta lapply(vm_step_to_eval … H2) whd in match eval_vmstate; 554 normalize nodelta #H cases(bind_inversion ????? H) -H * normalize nodelta 555 [1,7,13: #seq * [2,4,6: #lbl1] 556 |2,8,14: #newpc 557 |3,9,15: #cond #newpc #ltrue #lfalse 558 |4,10,16: #lin #io #lout 559 |5,11,17: #f 560 |*: 561 ] * normalize nodelta #EQfetch 562 [13,14,15: whd in s1_noio : (?(??%?)); >EQfetch in s1_noio; 563 normalize nodelta cases(asm_is_io ???) normalize nodelta 564 [1,3,5: * #H @⊥ @H % ] #_ 565 |*: cases(asm_is_io ???) normalize nodelta 566 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: 567 whd in ⊢ (??%% → ?); #EQ destruct] 568 [13 569 570 #i * #EQi #H cases(bind_inversion ????? H) -H #el 571 inversion H4 572 [ #s1 #s2 #i1 * [| #lbl] #EQfetch #no_io #EQstore #EQstack #EQio #EQpc 573 #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct >EQi in EQfetch; whd in ⊢ (??%% → ?); 574 #EQ destruct whd in match emits_labels; normalize nodelta 575 [ cases H1 whd in ⊢ (% → ?); [ * | #EQ destruct]] 576 * whd in ⊢ (??%% → ?); #EQ destruct >neutral whd in ⊢ (??%% → ?); 577 #EQ destruct whd in match (foldr ?????); 578 579 580 581 794 whd #costs whd in match list_cost_to_list_initcost; normalize nodelta 795 <map_append <map_append 796 change with (list_cost_to_list_initcost ?) in match (list_cost_to_list_initcost ?); 797 #EQ destruct whd in H2 : (??%?); >H3 in H2; normalize nodelta #H 798 cases(bind_inversion ????? H) -H #i * #EQi 799 inversion(emits_labels ??) 800 [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct >big_op_associative >act_op @IH 801 | #f #EQemits normalize nodelta #H 802 cases(bind_inversion ????? H) -H #k' * #EQk' whd in ⊢ (??%% → ?); 803 #EQ destruct(EQ) >act_op whd in match (append ???); @IH 804 ] 805 [1,5: inversion H in ⊢ ?; 806 [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct 807 |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_ 808 #EQ1 #EQ2 #EQ3 #EQ4 destruct 809 |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_ 810 #EQ1 #EQ2 #EQ3 #EQ4 destruct 811 |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct 812 * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 813 |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H * 814 ] // 815 | cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx >EQx 816 whd in match (map ????); whd in match (map ????); whd in match (big_op ??); 817 >neutral_l @opt_safe_elim #elem #EQget <(static_analisys_ok … x … (pc … st2) … EQmap) 818 assumption 819 | >neutral_r @(instr_map_ok … good … EQi … good_a1) /2/ 820 | % 821 | >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) 822 >(monotonicity_of_block_cost … EQk') // 823 | @(instr_map_ok … good … EQi … good_a1) /2/ 824 | >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) % 825 ] 826 ] 827 qed. 828 829 830 831
Note: See TracChangeset
for help on using the changeset viewer.