- Timestamp:
- Feb 20, 2014, 10:59:25 AM (7 years ago)
- Location:
- LTS
- Files:
-
- 3 deleted
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Language.ma
r3448 r3449 85 85 ]. 86 86 87 87 88 (* 88 89 lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) → … … 95 96 [|*: #x #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ 96 97 lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ') 97 | cases daemon (*TODO*) 98 qed. 98 | #seq * [| #lbl] #i #IH * normalize 99 [1,8: |2,9: #t_t |3,10: #seq1 #opt_l #i2 |4,11: #cond #ltrue #i_t #lfalse #i_f #i_c 100 |5,12: #cond #ltrue #i_t #lfalse #i_f |6,13: #f #act_p #ret #i3 |*: #lin #io #lout #i3] 101 #H1 #H2 try(@H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct) 102 inversion(?==?) normalize nodelta 103 [2,4: #ABS @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 104 >(\b (refl …)) in ABS; #EQ destruct] 105 #EQseq inversion(eq_instructions ???) normalize nodelta #Heq_i2 106 [2,4: @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 99 107 *) 100 108 … … 150 158 ]. 151 159 152 definition is_ret_ act : ActionLabel → Prop ≝153 λa.match a with [ret_act _ ⇒ True | _ ⇒ False ].160 definition is_ret_call_act : ActionLabel → Prop ≝ 161 λa.match a with [ret_act _ ⇒ True | call_act _ _ ⇒ True | _ ⇒ False ]. 154 162 155 163 inductive execute_l (p : state_params) (p' : sem_state_params p) (env : list (env_item p p)) : … … 157 165 | empty : ∀st,st',hd,tl.(code ? st) = (EMPTY p)→ (cont ? st) = hd :: tl → 158 166 (code ? st') = \snd hd → (cont … st') = tl → (store … st) = (store … st') → 159 (io_info … st = true → is_non_silent_cost_act (\fst hd)) → (io_info … st') = false → ¬ is_ret_ act (\fst hd) → execute_l … (\fst hd) st st'167 (io_info … st = true → is_non_silent_cost_act (\fst hd)) → (io_info … st') = false → ¬ is_ret_call_act (\fst hd) → execute_l … (\fst hd) st st' 160 168 | seq_sil : ∀st,st',i,cd,s,opt_l.(code ? st) = SEQ … i opt_l cd → 161 169 eval_seq … p' i (store … st) = return s → (code ? st') = cd → … … 2428 2436 ] 2429 2437 | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #H inversion H in ⊢ ?; 2430 [1,2,3,4,5,6,7,9: cases daemon (*assurdi*) ] 2438 [1,2,3,4,5,6,7,9: 2439 [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 2440 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 2441 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 2442 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 2443 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 2444 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 2445 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 2446 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 2447 ] 2448 destruct #t1 #t2 #prf #_ #_ * #y1 * #y2 #EQ destruct(EQ) @⊥ >EQ in x12; * #H @H % 2449 ] 2431 2450 #st11 #st12 #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem 2432 2451 #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 2433 2452 destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #t1 #t2 #H inversion H in ⊢ ?; 2434 [1,2,3,4,5,6,7,8: cases daemon (*assurdi*) ] 2453 [1,2,3,4,5,6,7,8: 2454 [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 2455 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 2456 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 2457 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 2458 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 2459 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 2460 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 2461 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 #x21 2462 ] 2463 destruct #_ #_ #_ #_ #_ #_ #_ whd in ⊢ (% → ?); #EQ destruct(EQ) 2464 @⊥ >EQ in x12; * #H @H % 2465 ] 2435 2466 #st41 #st42 #r_t #mem1 #new_cont #opt_l1 #cd #EQcode41 #EQcont41 #EQ destruct(EQ) 2436 2467 #EQio41 #EQio42 #EQmem1 #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct #st11_noio … … 2443 2474 #abs_top_cont #abs_tail_cont #EQcheck 2444 2475 normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1') 2445 [1,2,3,4,5,7: (*assurdi da fare*) cases daemon] #f' #act_p' #opt_l' #i' #_ 2476 [1,2,3,4,5,7: 2477 [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 2478 | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 2479 | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) 2480 normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta 2481 [2: #l1 cases(?==?) normalize nodelta]] 2482 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 2483 | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ 2484 whd in ⊢ (??%% → ?); cases(call_post_clean ?????) 2485 [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) 2486 [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) 2487 [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] 2488 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 2489 | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ 2490 whd in ⊢ (??%% → ?); cases(call_post_clean ?????) 2491 [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) 2492 [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] 2493 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 2494 | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) 2495 normalize nodelta 2496 [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] 2497 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 2498 ] 2499 ] #f' #act_p' #opt_l' #i' #_ 2446 2500 #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ) 2447 2501 lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H … … 2488 2542 normalize nodelta inversion(call_post_clean ?????) normalize nodelta 2489 2543 [ #_ whd in ⊢ (??%% → ?); #EQ destruct ***** ] * #abs_top'''' #i''' 2490 #EQ_clean_i'' inversion(act_lbl) normalize nodelta [1,3,4: cases daemon (*assurdi*)] 2544 #EQ_clean_i'' inversion(act_lbl) normalize nodelta 2545 [1,3,4: 2546 [ #x1 #x2 #EQ whd in ⊢ (??%% → ?); #EQ1 destruct ***** 2547 | * [|#x1] #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); 2548 #EQ destruct ****** [2: *] #EQ destruct 2549 | #EQ whd in ⊢ (??%% → ?); #EQ1 destruct ***** 2550 ] 2551 ] 2491 2552 cut(act_lbl = ret_act (Some ? lbl') ∧ cont_st42' = cont … st1' ∧ i'' = i') 2492 2553 [ cases(stack_safety1 [ ] …) … … 2499 2560 whd in ⊢ (??%% → ?); #EQ destruct ****** #_ #HH3 #EQ destruct(EQ) 2500 2561 >EQcode41 in ⊢ (% → ?); inversion(code … st41') 2501 [1,3,4,5,6,7: cases daemon (*ASSURDI*) ] #r_t' #EQcode_st41' whd in ⊢ (??%% → ?); 2562 [1,3,4,5,6,7: 2563 [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 2564 | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) 2565 normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta 2566 [2: #l1 cases(?==?) normalize nodelta]] 2567 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 2568 | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ 2569 whd in ⊢ (??%% → ?); cases(call_post_clean ?????) 2570 [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) 2571 [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) 2572 [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] 2573 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 2574 | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ 2575 whd in ⊢ (??%% → ?); cases(call_post_clean ?????) 2576 [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) 2577 [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] 2578 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 2579 | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) 2580 normalize nodelta 2581 [2,4: * #z1 #z2 cases lbl normalize nodelta 2582 [2,4: #l1 cases(memb ???) normalize nodelta 2583 [1,3: cases(?==?) normalize nodelta ]]] 2584 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 2585 | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) 2586 normalize nodelta 2587 [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] 2588 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 2589 ] 2590 ] #r_t' #EQcode_st41' whd in ⊢ (??%% → ?); 2502 2591 #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore_st41' #EQinfo_st41' 2503 2592 #EQ destruct(EQ) >EQcont11_42 in EQcheck; >EQ_contst42 in ⊢ (% → ?); -
LTS/Simulation.ma
r3396 r3449 1 include "Common.ma".2 1 include "Traces.ma". 3 2 -
LTS/Vm.ma
r3448 r3449 3 3 include "../src/utilities/option.ma". 4 4 include "basics/jmeq.ma". 5 6 lemma bind_inversion : ∀A,B : Type[0].∀m : option A. 7 ∀f : A → option B.∀y : B. 8 ! x ← m; f x = return y → 9 ∃ x.(m = return x) ∧ (f x = return y). 10 #A #B * [| #a] #f #y normalize #EQ [destruct] 11 %{a} %{(refl …)} // 12 qed. 5 13 6 14 record monoid: Type[1] ≝ … … 56 64 definition label_of_pc ≝ λL.λl.λpc.find … 57 65 (λp.let 〈x,y〉 ≝ p in if eqb x pc then Some L y else None ? ) l. 66 67 definition option_pop ≝ 68 λA.λl:list A. match l with 69 [ nil ⇒ None ? 70 | cons a tl ⇒ Some ? (〈a,tl〉) ]. 58 71 59 72 … … 143 156 op … (cost … st1) (cost_of p p' (Iret p)) = cost … st2 → 144 157 vmstep … (ret_act (Some ? lbl)) st1 st2. 145 158 159 definition eval_vmstate : ∀p : assembler_params.∀p' : sem_params p. 160 AssemblerProgram p → vm_state p p' → option (ActionLabel × (vm_state p p')) ≝ 161 λp,p',prog,st. 162 ! i ← fetch … prog (pc … st); 163 match i with 164 [ Seq x opt_l ⇒ 165 if asm_is_io … st then 166 None ? 167 else 168 ! new_store ← eval_asm_seq p p' x (asm_store … st); 169 return 〈cost_act opt_l, 170 mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false 171 (op … (cost … st) (cost_of p p' (Seq p x opt_l)))〉 172 | Ijmp newpc ⇒ 173 if asm_is_io … st then 174 None ? 175 else 176 return 〈cost_act (None ?), 177 mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false 178 (op … (cost … st) (cost_of p p' (Ijmp … newpc)))〉 179 | CJump cond newpc ltrue lfalse ⇒ 180 if asm_is_io … st then 181 None ? 182 else 183 ! b ← eval_asm_cond p p' cond (asm_store … st); 184 if b then 185 return 〈cost_act (Some ? ltrue), 186 mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false 187 (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse)))〉 188 else 189 return 〈cost_act (Some ? lfalse), 190 mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false 191 (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse)))〉 192 | Iio lin io lout ⇒ 193 if asm_is_io … st then 194 ! new_store ← eval_asm_io … io (asm_store … st); 195 return 〈cost_act (Some ? lout), 196 mk_vm_state ?? (S (pc … st)) (asm_stack … st) 197 new_store false 198 (op … (cost … st) 199 (cost_of_io p p' io (asm_store … st)))〉 200 else 201 return 〈cost_act (Some ? lin), 202 mk_vm_state ?? (pc … st) (asm_stack … st) (asm_store … st) 203 true (cost … st)〉 204 | Icall f ⇒ 205 if asm_is_io … st then 206 None ? 207 else 208 ! lbl ← label_of_pc ? (call_label_fun p) (entry_of_function p f); 209 return 〈call_act f lbl, 210 mk_vm_state ?? (entry_of_function p f) 211 ((S (pc … st)) :: (asm_stack … st)) 212 (asm_store … st) false 213 (op … (cost … st) (cost_of p p' (Icall p f)))〉 214 | Iret ⇒ if asm_is_io … st then 215 None ? 216 else 217 ! 〈newpc,tl〉 ← option_pop … (asm_stack … st); 218 ! lbl ← label_of_pc ? (return_label_fun p) newpc; 219 return 〈ret_act (Some ? lbl), 220 mk_vm_state ?? newpc tl (asm_store … st) false 221 (op … (cost … st) (cost_of p p' (Iret p)))〉 222 ]. 223 224 lemma eval_vmstate_to_Prop : ∀p,p',prog,st1,st2,l. 225 eval_vmstate p p' prog st1 = return 〈l,st2〉 → vmstep … prog l st1 st2. 226 #p #p' #prog #st1 #st2 #l whd in match eval_vmstate; normalize nodelta 227 #H cases(bind_inversion ????? H) -H * normalize nodelta 228 [ #seq #opt_l * #EQfetch inversion(asm_is_io ???) normalize nodelta 229 [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H) 230 #newstore * #EQnewstore whd in ⊢ (??%% → ?); #EQ destruct 231 @vm_seq // 232 | #newpc * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio 233 [ whd in ⊢ (??%% → ?); #EQ destruct] whd in ⊢ (??%% → ?); #EQ destruct 234 @vm_ijump // 235 | #cond #new_pc #ltrue #lfase * #EQfetch inversion(asm_is_io ???) normalize nodelta 236 [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H) -H 237 * normalize nodelta * #EQcond whd in ⊢ (??%% → ?); #EQ destruct 238 [ @(vm_cjump_true … EQfetch) // | @(vm_cjump_false … EQfetch) //] 239 | #lin #io #lout * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio 240 [ #H cases(bind_inversion ????? H) -H #newstore * #EQnewstore ] 241 whd in ⊢ (??%% → ?); #EQ destruct 242 [ @(vm_io_out … EQfetch) // | @(vm_io_in … EQfetch) // ] 243 | #f * #EQfetch inversion(asm_is_io ???) #EQio normalize nodelta 244 [ whd in ⊢ (??%% → ?); #EQ destruct ] #H cases (bind_inversion ????? H) -H 245 #lbl * #EQlb whd in ⊢ (??%% → ?); #EQ destruct @(vm_call … EQfetch) // 246 | * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio 247 [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H 248 * #newpc #tl * whd in match option_pop; normalize nodelta inversion(asm_stack ???) 249 normalize nodelta [#_ whd in ⊢ (??%% → ?); #EQ destruct] #newpc1 #tl1 #_ 250 #EQstack whd in ⊢ (??%% → ?); #EQ destruct #H cases(bind_inversion ????? H) #lbl 251 * #EQlbl whd in ⊢ (??%% → ?); #EQ destruct @vm_ret // 252 ] 253 qed. 254 146 255 include "../src/utilities/hide.ma". 147 256 … … 325 434 }. 326 435 327 lemma bind_inversion : ∀A,B : Type[0].∀m : option A.328 ∀f : A → option B.∀y : B.329 ! x ← m; f x = return y →330 ∃ x.(m = return x) ∧ (f x = return y).331 #A #B * [| #a] #f #y normalize #EQ [destruct]332 %{a} %{(refl …)} //333 qed.334 335 436 lemma static_dynamic : ∀p,p',prog,k,mT,map. 336 437 static_analisys p p' mT prog = return map →
Note: See TracChangeset
for help on using the changeset viewer.