Changeset 3449


Ignore:
Timestamp:
Feb 20, 2014, 10:59:25 AM (5 years ago)
Author:
piccolo
Message:

clean up

Location:
LTS
Files:
3 deleted
3 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3448 r3449  
    8585].
    8686
     87
    8788(*
    8889lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) →
     
    9596  [|*: #x #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
    9697  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
    99107*)
    100108
     
    150158].
    151159
    152 definition is_ret_act : ActionLabel → Prop ≝
    153 λa.match a with [ret_act _ ⇒ True | _ ⇒ False ].
     160definition is_ret_call_act : ActionLabel → Prop ≝
     161λa.match a with [ret_act _ ⇒ True | call_act _ _ ⇒ True | _ ⇒ False ].
    154162
    155163inductive execute_l (p : state_params) (p' : sem_state_params p) (env : list (env_item p p)) :
     
    157165| empty : ∀st,st',hd,tl.(code ? st) = (EMPTY p)→ (cont ? st) = hd :: tl →
    158166           (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'
    160168| seq_sil : ∀st,st',i,cd,s,opt_l.(code ? st) = SEQ … i opt_l cd →
    161169             eval_seq … p' i (store … st) = return s → (code ? st') = cd →
     
    24282436  ]
    24292437| #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  ]
    24312450  #st11 #st12 #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
    24322451  #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3
    24332452  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  ]
    24352466   #st41 #st42 #r_t #mem1 #new_cont #opt_l1 #cd #EQcode41 #EQcont41 #EQ destruct(EQ)
    24362467   #EQio41 #EQio42 #EQmem1 #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct #st11_noio
     
    24432474    #abs_top_cont #abs_tail_cont #EQcheck
    24442475    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' #_
    24462500    #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ)
    24472501    lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H
     
    24882542     normalize nodelta inversion(call_post_clean ?????) normalize nodelta
    24892543     [ #_ 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     ]
    24912552     cut(act_lbl = ret_act (Some ? lbl') ∧ cont_st42' = cont … st1' ∧ i'' = i')
    24922553     [ cases(stack_safety1 [ ] …)
     
    24992560     whd in ⊢ (??%% → ?); #EQ destruct ****** #_ #HH3 #EQ destruct(EQ)
    25002561     >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 ⊢ (??%% → ?);
    25022591     #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore_st41' #EQinfo_st41'
    25032592     #EQ destruct(EQ) >EQcont11_42 in EQcheck; >EQ_contst42 in ⊢ (% → ?);
  • LTS/Simulation.ma

    r3396 r3449  
    1 include "Common.ma".
    21include "Traces.ma".
    32
  • LTS/Vm.ma

    r3448 r3449  
    33include "../src/utilities/option.ma".
    44include "basics/jmeq.ma".
     5
     6lemma 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 …)} //
     12qed.
    513
    614record monoid: Type[1] ≝
     
    5664definition label_of_pc ≝ λL.λl.λpc.find …
    5765   (λp.let 〈x,y〉 ≝ p in if eqb x pc then Some L y else None ? ) l.
     66   
     67definition option_pop ≝
     68  λA.λl:list A. match l with
     69  [ nil ⇒ None ?
     70  | cons a tl ⇒ Some ? (〈a,tl〉) ].
    5871
    5972
     
    143156           op … (cost … st1) (cost_of p p' (Iret p)) = cost … st2 →
    144157           vmstep … (ret_act (Some ? lbl)) st1 st2.
    145            
     158
     159definition eval_vmstate : ∀p : assembler_params.∀p' : sem_params p.
     160AssemblerProgram p → vm_state p p' → option (ActionLabel × (vm_state p p')) ≝
     161λp,p',prog,st.
     162! i ← fetch … prog (pc … st);
     163match 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
     224lemma eval_vmstate_to_Prop : ∀p,p',prog,st1,st2,l.
     225eval_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]
     253qed.
     254
    146255include "../src/utilities/hide.ma".
    147256
     
    325434 }.
    326435 
    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 
    335436lemma static_dynamic : ∀p,p',prog,k,mT,map.
    336437static_analisys p p' mT prog = return map →
Note: See TracChangeset for help on using the changeset viewer.