Changeset 3524 for LTS/Vm.ma


Ignore:
Timestamp:
Mar 11, 2015, 4:26:40 PM (5 years ago)
Author:
piccolo
Message:

rearrangments of lemmas, final statement in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3523 r3524  
    8080
    8181record sem_params (p : assembler_params) : Type[1] ≝
    82 { m : monoid
    83 ; asm_store_type : Type[0]
     82{ asm_store_type : Type[0]
    8483; eval_asm_seq : seq_instr p → asm_store_type → option asm_store_type
    8584; eval_asm_cond : jump_condition p → asm_store_type → option bool
    8685; eval_asm_io : io_instr p → asm_store_type → option asm_store_type
    87 ; cost_of_io : io_instr p → asm_store_type → m
    88 ; cost_of : AssemblerInstr p → asm_store_type →  m
    8986}.
    9087
     
    9491; asm_store : asm_store_type … p'
    9592; asm_is_io : bool
    96 ; cost : m … p'
    9793}.
    9894
     
    116112           asm_is_io … st1 = asm_is_io … st2 →
    117113           S (pc … st1) = pc … st2 →
    118            op … (cost … st1) (cost_of p p' (Seq p i l) (asm_store … st1)) = cost … st2 →
    119114           vmstep … (cost_act l) st1 st2
    120115| vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ.
     
    125120           asm_is_io … st1 = asm_is_io … st2 →
    126121           new_pc = pc … st2 →
    127            op … (cost … st1) (cost_of p p' (Ijmp … new_pc) (asm_store … st1)) = cost … st2 →
    128122           vmstep … (cost_act (None ?)) st1 st2
    129123| vm_cjump_true :
     
    136130           asm_is_io … st1 = asm_is_io … st2 →
    137131           pc … st2 = new_pc →
    138            op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 →
    139132           vmstep … (cost_act (Some ? ltrue)) st1 st2
    140133| vm_cjump_false :
     
    147140           asm_is_io … st1 = asm_is_io … st2 →
    148141           S (pc … st1) = pc … st2 →
    149            op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 →
    150142           vmstep … (cost_act (Some ? lfalse)) st1 st2
    151143| vm_io_in : 
     
    157149           true = asm_is_io … st2 →
    158150           pc … st1 = pc … st2 →
    159            cost … st1 = cost … st2 →
    160151           vmstep … (cost_act (Some ? lin)) st1 st2
    161152| vm_io_out :
     
    167158           false = asm_is_io … st2 →
    168159           S (pc … st1) = pc … st2 →
    169            op … (cost … st1) (cost_of_io p p' io (asm_store … st1)) = cost … st2 →
    170160           vmstep … (cost_act (Some ? lout)) st1 st2
    171161| vm_call :
     
    177167           asm_is_io … st1 = asm_is_io … st2 →
    178168           entry_of_function … prog f = pc … st2 →
    179            op … (cost … st1) (cost_of p p' (Icall p f) (asm_store … st1)) = cost … st2 →
    180169           label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f) = return lbl →
    181170           vmstep … (call_act f lbl) st1 st2
     
    189178           newpc = pc … st2 →
    190179           label_of_pc ? (return_label_fun … prog) newpc = return lbl →
    191            op … (cost … st1) (cost_of p p' (Iret p) (asm_store … st1)) = cost … st2 →
    192180           vmstep … (ret_act (Some ? lbl)) st1 st2.
    193181
     
    203191     ! new_store ← eval_asm_seq p p' x (asm_store … st);
    204192     return 〈cost_act opt_l,
    205              mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false
    206                 (op … (cost … st) (cost_of p p' (Seq p x opt_l) (asm_store … st)))〉
     193             mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false〉
    207194| Ijmp newpc ⇒
    208195   if asm_is_io … st then
     
    210197   else
    211198     return 〈cost_act (None ?),
    212              mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
    213                 (op … (cost … st) (cost_of p p' (Ijmp … newpc) (asm_store … st)))〉
     199             mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false〉
    214200| CJump cond newpc ltrue lfalse ⇒
    215201   if asm_is_io … st then
     
    219205     if b then
    220206       return 〈cost_act (Some ? ltrue),
    221                mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
    222                 (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉
     207               mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false〉
    223208     else
    224209       return 〈cost_act (Some ? lfalse),
    225                mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false
    226                 (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉
     210               mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false〉
    227211| Iio lin io lout ⇒
    228212              if asm_is_io … st then
     
    230214                 return 〈cost_act (Some ? lout),
    231215                         mk_vm_state ?? (S (pc … st)) (asm_stack … st)
    232                          new_store false
    233                          (op … (cost … st)
    234                                (cost_of_io p p' io (asm_store … st)))〉   
     216                         new_store false〉   
    235217              else
    236218                return 〈cost_act (Some ? lin),
    237219                        mk_vm_state ?? (pc … st) (asm_stack … st) (asm_store … st)
    238                                     true (cost … st)
     220                                    true
    239221| Icall f ⇒
    240222    if asm_is_io … st then
     
    245227              mk_vm_state ?? (entry_of_function … prog f)
    246228                             ((S (pc … st)) :: (asm_stack … st))
    247                              (asm_store … st) false
    248                              (op … (cost … st) (cost_of p p' (Icall p f) (asm_store … st)))〉
     229                             (asm_store … st) false〉
    249230| Iret ⇒ if asm_is_io … st then
    250231            None ?
     
    253234            ! lbl ← label_of_pc ? (return_label_fun … prog) newpc;
    254235            return 〈ret_act (Some ? lbl),
    255                     mk_vm_state ?? newpc tl (asm_store … st) false   
    256                      (op … (cost … st) (cost_of p p' (Iret p) (asm_store … st)))〉
     236                    mk_vm_state ?? newpc tl (asm_store … st) false〉
    257237].
    258238
     
    291271lemma vm_step_to_eval : ∀p,p',prog,st1,st2,l.vmstep … prog l st1 st2 →
    292272eval_vmstate p p' prog st1 = return 〈l,st2〉.
    293 #p #p' #prog * #pc1 #stack1 #store1 #io1 #cost1
    294 * #pc2 #stack2 #store2 #io2 #cost2 #l #H inversion H
    295 [ #s1 #s2 #i #opt_l #EQfetch #EQio #EQstore #EQstack #EQio1 #EQpc #EQcost
     273#p #p' #prog * #pc1 #stack1 #store1 #io1
     274* #pc2 #stack2 #store2 #io2 #l #H inversion H
     275[ #s1 #s2 #i #opt_l #EQfetch #EQio #EQstore #EQstack #EQio1 #EQpc
    296276  #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta   
    297277  >EQfetch >m_return_bind normalize nodelta >EQio normalize nodelta >EQstore
    298   >m_return_bind <EQio1 >EQio <EQpc >EQstack >EQcost %
    299 | #s1 #s2 #newpc #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc #EQcost
     278  >m_return_bind <EQio1 >EQio <EQpc >EQstack %
     279| #s1 #s2 #newpc #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc
    300280  #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta
    301281  >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta <EQio2 >EQio1
    302   >EQstore >EQstack <EQcost >EQstore %
     282  >EQstore >EQstack >EQstore %
    303283|3,4: #s1 #s2 #cond #newoc #ltrue #lfalse #EQev_cond #EQfetch #EQio1 #EQstore
    304   #EQstack #EQio2 #EQnewoc #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct
     284  #EQstack #EQio2 #EQnewoc #EQ1 #EQ2 #EQ3 #EQ4 destruct
    305285  whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind
    306286  normalize nodelta >EQio1 normalize nodelta >EQev_cond >m_return_bind
    307   normalize nodelta <EQio1 >EQio2 >EQstore >EQstack <EQcost >EQstore [%] >EQnewoc %
     287  normalize nodelta <EQio1 >EQio2 >EQstore >EQstack >EQstore [%] >EQnewoc %
    308288|5,6: #s1 #s2 #lin #io #lout #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQpc
    309    #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
     289   #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
    310290   normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1
    311    normalize nodelta >EQstack <EQpc >EQcost [ >EQstore <EQio2 %]
     291   normalize nodelta >EQstack <EQpc [ >EQstore <EQio2 %]
    312292   >EQstore >m_return_bind <EQpc <EQio2 %
    313293| #s1 #s2 #f #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQentry
    314   #EQcost #EQlab_pc #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
     294  #EQlab_pc #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
    315295  normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1
    316   normalize nodelta >EQlab_pc >m_return_bind >EQentry >EQcost <EQio2 >EQio1
     296  normalize nodelta >EQlab_pc >m_return_bind >EQentry <EQio2 >EQio1
    317297  <EQstack >EQstore %
    318298| #s1 #s2 #newpc #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc
    319   #EQlab_pc #EQcosts #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
     299  #EQlab_pc #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
    320300  normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta
    321301  >EQstack whd in match option_pop; normalize nodelta >m_return_bind
    322   >EQlab_pc >m_return_bind >EQcosts >EQstore  <EQio2 >EQio1 %
     302  >EQlab_pc >m_return_bind >EQstore  <EQio2 >EQio1 %
    323303]
    324304qed.
     
    448428definition asm_concrete_trans_sys ≝
    449429λp,p',prog.mk_concrete_transition_sys …
    450              (asm_operational_semantics p p' prog) (m … p')
    451              (λs.match s with [STATE st ⇒ cost … st | _ ⇒ e …] ).
    452 
     430             (asm_operational_semantics p p' prog).
     431             
     432         
    453433definition emits_labels ≝
    454434λp.λinstr : AssemblerInstr p.match instr with
     
    465445
    466446record asm_galois_connection (p: assembler_params) (p': sem_params p) (prog: AssemblerProgram p) : Type[2] ≝
    467 { aabs_d : abstract_transition_sys (m … p')
     447{ aabs_d : abstract_transition_sys
    468448; agalois_rel:> galois_rel (asm_concrete_trans_sys p p' prog) aabs_d
    469449}.
Note: See TracChangeset for help on using the changeset viewer.