Changeset 3449 for LTS/Vm.ma


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

clean up

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.