Changeset 3372


Ignore:
Timestamp:
Jul 1, 2013, 4:34:13 PM (4 years ago)
Author:
piccolo
Message:

Added new implementation of labelling approach based on LTS and emmission of costlabels during transitions

Files:
2 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTLProof.ma

    r3371 r3372  
    6666     (beloadv m2) (beloadv m3).
    6767
     68(*
    6869definition callee_saved_remap :
    6970(Σb:block.block_region b=Code) → (block → list register) →
     
    8788  ]
    8889].
     90*)
     91
    8992(*
    9093definition mem_relation : fixpoint_computer → coloured_graph_computer →
     
    97100     (λptr1,ptr2.ERTL_validate_pointer … ge f st ptr1 = return it ∧ ptr1 = ptr2) R
    98101     (beloadv m2) (beloadv m3).
     102*)
    99103
    100104definition callee_saved_remap : fixpoint_computer → coloured_graph_computer →
     
    123127  | None ⇒ d
    124128  ]
    125 ]. *)
    126 
     129].
     130
     131xxxxxxxxxxxxx
    127132
    128133let rec frames_relation_aux (prog : ertl_program) (stacksize : ident → option ℕ)
     
    520525qed.*)
    521526
    522 
    523527lemma ps_reg_retrieve_hw_reg_retrieve_commute :
    524528∀prog,stacksize,init,color_f,live_f,color_fun,live_fun.
     
    10231027cases daemon qed.
    10241028
     1029axiom BadVertexValue : ErrorMessage.
     1030
    10251031definition ertl_vertex_retrieve :  ertl_reg_env → vertex → res beval ≝
    1026 λregs,v.match v with [inl r ⇒ ps_reg_retrieve regs r | inr r ⇒ hw_reg_retrieve regs r ].
    1027 
     1032λregs,v.match v with
     1033[inl r ⇒ ps_reg_retrieve regs r
     1034| inr r ⇒ match hwreg_retrieve (\snd regs) r with
     1035   [ BVundef ⇒ Error ? [MSG BadVertexValue]
     1036   | _ ⇒ OK ? (hwreg_retrieve (\snd regs) r)
     1037   ]
     1038].
     1039 
    10281040definition eq_decision : decision → decision → bool ≝
    10291041λd1,d2.match d1 with
     
    10421054qed.
    10431055
     1056lemma ertl_vertex_retrieve_ok_on_hw_regs :
     1057∀regs,r,bv.ertl_vertex_retrieve regs (inr ?? r) = return bv →
     1058hwreg_retrieve (\snd regs) r = bv.
     1059#regs #r #bv whd in match ertl_vertex_retrieve; normalize nodelta
     1060cases(hwreg_retrieve ??) normalize nodelta
     1061[|| #x #y #p | #b | #p | #ptr #p | #pc #p ]
     1062#EQ whd in EQ : (???%); destruct %
     1063qed.
    10441064
    10451065lemma vertex_retrieve_read_arg_decision_commute :
     
    10541074     (λv,d.
    10551075      bool_to_Prop
    1056         (live_fun fn (point_of_pc ERTL_semantics pc) v) ∧
     1076        (live_fun fn (point_of_pc ERTL_semantics pc) v) ∧ 
    10571077      d =
    10581078      (color_fun fn v))
    1059      (λbv,bv'.bv = sigma_beval prog stacksize init init_regs f_lbls f_regs bv') …
    1060      (λst1.ertl_vertex_retrieve (regs … st1))
    1061      (λst,d.m_map Res ?? (\fst …)
    1062       (read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
     1079     (λx,y.\fst x = sigma_beval prog stacksize init init_regs f_lbls f_regs (\fst y) ∧
     1080            gen_state_rel prog stacksize init color_f live_f color_fun
     1081            live_fun init_regs f_lbls f_regs pc (\snd x) (\snd y)) …
     1082     (λst1,v.! bv ← ertl_vertex_retrieve (regs … st1) v;
     1083              return〈bv,st1〉)
     1084     (λst,d.(read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
    10631085#prog #stacksize #init #color_f #live_f #color_fun #live_fun #init_regs #f_lbls #f_regs
    10641086#f #fn #pc #EQfn #st1 #st2 *
     
    10661088** >EQfn whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1) #_ cases(st_frms ??) [*] #frames
    10671089normalize nodelta ***** #_ #H1 #_ #_ #_ #_ * #live_R #EQ destruct(EQ) #bv #EQbv
    1068 lapply((proj2 ?? H1 …) R live_R) cases(color_fun ??) normalize nodelta [#n1 | #R1 ]
    1069 whd in EQbv : (??%%); destruct(EQbv)
     1090lapply((proj2 ?? H1 …) R live_R ?)
     1091[ % #ABS whd in match ertl_vertex_retrieve in EQbv; normalize nodelta in EQbv;
     1092  >ABS in EQbv; normalize nodelta whd in ⊢ (???% → ?); #EQ destruct(EQ) ]
     1093 cases(color_fun ??) normalize nodelta [#n1 | #R1 ] lapply(ertl_vertex_retrieve_ok_on_hw_regs … EQbv)
     1094 #EQ destruct(EQ)
    10701095[ inversion (hwreg_retrieve_sp ?) normalize nodelta [2: #e #_ *] #sp #EQsp
    10711096  inversion(beloadv ??) normalize nodelta [ #_ *] #bv1 #EQbv1 #Hbv1 %{bv1}
     
    11121137qed.
    11131138
     1139(*
    11141140lemma update_color_lemma :
    11151141∀fix_comp,colour,prog,init.
     
    11781204     (update_fun ?? eq_vertex (live_fun fn (point_of_pc ERTL_semantics pc)) v new_live))
    11791205 init_regs f_lbls f_regs pc st1 st2.
    1180 cases daemon qed. 
     1206cases daemon qed.  *)
    11811207
    11821208lemma move_preserve :
Note: See TracChangeset for help on using the changeset viewer.