Changeset 3489 for LTS


Ignore:
Timestamp:
Sep 24, 2014, 4:32:23 PM (5 years ago)
Author:
sacerdot
Message:

Second daemon closed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3488 r3489  
    516516qed.
    517517
     518lemma labels_pf_in_act: ∀p,prog,pc.
     519  mem CostLabel (in_act p prog)
     520  (map (CostLabel×ℕ) CostLabel \fst
     521   (labels_pc p (instructions p prog) (call_label_fun p prog)
     522    (return_label_fun p prog) (in_act p prog) pc)).
     523 #p #prog elim (instructions p prog) normalize /2/
     524qed.
     525
    518526lemma labels_pc_return: ∀p,prog,l1,l2,iact,x1,x2.
    519527 label_of_pc ReturnPostCostLabel l2 x1=return x2 →
     
    772780
    773781lemma labels_of_trace_are_in_code :
    774 ∀p,p',prog.∀st1,st2 :  vm_ass_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
     782∀p,p',prog.∀st1,st2 : vm_ass_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
    775783∀lbl.
    776784mem … lbl (get_costlabels_of_trace … t) →
    777 mem … (lbl) (map ?? \fst … (labels_pc … (instructions p prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)).
    778 cases daemon (*
     785mem … lbl (map … \fst … (labels_pc … (instructions p prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)).
    779786#p #p' #prog #st1 #st2 #t elim t
    780787[ #st #lbl *
    781 | #st1 #st2 #st3 #l * #H1 #H2 #tl #IH #lbl whd in match (get_costlabels_of_trace ????);
    782   #H cases(mem_append ???? H) -H [2: #H @IH //]
    783   lapply(vm_step_to_eval … H2) whd in match eval_vmstate;
    784   normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi #_
    785   inversion(emits_labels … i)
    786   [ #EQemit cases(step_emit … (vm_step_to_eval … H2)) // #x * #EQ1 #EQ2 >EQ1 *
    787     [2: *] #EQ destruct cases(map_mem … \fst … EQ2) #y * #H3 #EQ destruct //
    788   | #f #EQemit >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H2) … EQemit))
    789     *
    790   ]
    791 ]  *)
     788| #st1 #st2 #st3 #l whd in ⊢ (% → ?);
     789  cases st1 -st1 normalize nodelta [2: * |3: #st1]
     790  cases st2 -st2 normalize nodelta [1,4,5: * |2: * #HN1 #HN2 >HN2 -HN2 |6: #st2 * #HN1 #HN2 >HN2 -HN2 |3: #st2 ]
     791  [3: * #H1 #H2 #tl #IH #lbl whd in match (get_costlabels_of_trace ????);
     792      #H cases(mem_append ???? H) -H [2: #H @IH //]
     793      lapply(vm_step_to_eval … H2) whd in match eval_vmstate;
     794      normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi #_
     795      inversion(emits_labels … i)
     796      [ #EQemit cases(step_emit … (vm_step_to_eval … H2)) // #x * #EQ1 #EQ2 >EQ1 *
     797        [2: *] #EQ destruct cases(map_mem … \fst … EQ2) #y * #H3 #EQ destruct //
     798      | #f #EQemit >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H2) … EQemit))
     799        *
     800      ]
     801  |*: #tl #IH #lbl whd in match (get_costlabels_of_trace ????); * // @IH
     802]
    792803qed.
    793804
Note: See TracChangeset for help on using the changeset viewer.