Changeset 3535 for LTS/Final.ma


Ignore:
Timestamp:
Mar 16, 2015, 4:30:28 PM (5 years ago)
Author:
piccolo
Message:

final statement of cerco with the first pass integrated in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Final.ma

    r3531 r3535  
    1414
    1515include "Simulation.ma".
    16 include "Vm.ma".   
     16include "Vm.ma".
     17include "Lang_meas.ma".
    1718
    1819theorem cerco:
     
    7677#S1 #p #p' #prog letin S2 ≝ (asm_operational_semantics ???) #rel #sim_conds
    7778#R #mT #map #EQmap #si #s1 #s2 #sn #t #Hmeas #si' #Hclass #Rsisi'
    78 cases (simulates_measurable … sim_conds … Hmeas … Hclass Rsisi')
     79cases (simulates_measurable S1 S2 rel sim_conds … Hmeas … Rsisi')
     80[2: #H cases Hclass >H #ABS cases(ABS (refl …)) ]
    7981#sn' * #t' ** #Rsnsn' #EQcostlabs * #s1' * #s2' #Hmeas'
    8082%{sn'} %{t'} %{Rsnsn'} %{EQcostlabs} %{s1'} %{s2'} %{Hmeas'} #acts #EQacts
     
    8385qed. 
    8486
     87lemma is_permutation_mem : ∀A :DeqSet.
     88∀l1,l2 : list A.∀x : A.mem … x l1 →
     89is_permutation A l1 l2 → mem … x l2.
     90cases daemon
     91qed.
     92
     93definition is_abelian ≝ λM : monoid.
     94∀x,y : M.op … M x y = op … M y x.
     95
     96lemma action_on_permutation : ∀M : abstract_transition_sys.is_abelian (abs_instr M) →
     97∀l1,l2 : list (abs_instr M).∀a.is_permutation … l1 l2 →
     98(〚l1〛 a) = (〚l2〛 a).
     99cases daemon
     100qed.
     101
     102lemma is_permutation_dependent_map : ∀A,B : DeqSet.∀l1,l2 : list A.
     103∀f : (∀a : A.mem … a l1 → B).∀g : (∀a : A.mem … a l2 → B).
     104∀perm : is_permutation A l1 l2.
     105(∀a : A.
     106 ∀prf : mem … a l1.f a prf = g a ?) →
     107is_permutation B (dependent_map … l1 f) (dependent_map … l2 g).
     108[2: @(is_permutation_mem … perm) //]
     109cases daemon
     110qed.
     111
     112theorem final_cerco :
     113(* for all programs in the imperative language (possibly with call non post labelled) *)
     114∀p,p',prog.
     115no_duplicates_labels … prog →
     116
     117(* let t_prog be the same program in which all calls are post-labelled *)
     118let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
     119
     120(* Let S1 be the operational semantics of the source code  *)
     121let S1 ≝ operational_semantics p p' prog in
     122
     123(* Let S2 be the operational semantics of the soource code with call post labelled  *)
     124let S2 ≝ operational_semantics p p' t_prog in
     125
     126(* for all assmbler programs *)
     127∀p_asm,p_asm',prog_asm.
     128(* Let S3 be the operational semantics of the compiled code  *)
     129let S3 ≝ asm_operational_semantics p_asm p_asm' prog_asm in
     130
     131(* If the simulation conditions between the source with call post-labelled and compiled
     132    code holds (i.e. if the compiler is correct after the first pass) *)
     133∀rel: relations S2 S3. simulation_conditions … rel →
     134
     135(* let REL be semantical relation between the states of the source program and
     136   the states of compiled code *)
     137let REL ≝ λsi : S1.λsi' : S3.∃si'' : S2.∃abs_top,abs_tail.state_rel … m keep abs_top abs_tail si si'' ∧
     138Srel … rel si'' si' in
     139
     140 (* Given an abstract interpretation framework for the compiled code *)
     141∀R: asm_abstract_interpretation p_asm p_asm' prog_asm.
     142
     143(* If the abstract instructions monoid is abelian *)
     144is_abelian (abs_instr … (aabs_d … (asm_galois_conn … R))) → 
     145 
     146 (* If the static analysis does not fail *)
     147∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog_asm = return map1.
     148
     149 (* For every source trace whose measurable fragment starts in s1 and ends in s2 or,
     150   equivalently, whose state after the initial labelled transition is s1
     151   and whose state after the final labelled transition is s2  *)
     152 ∀si,s1,s2,sn. ∀t: raw_trace S1 … si sn.
     153 measurable … s1 s2 … t →
     154
     155 (* For each target non I/O state si' in relation with the source state si *)
     156 ∀si': S3. as_classify … si' ≠ cl_io → REL si si' →
     157
     158 (* There exists a corresponding target trace starting from si' *)
     159 ∃sn'. ∃t': raw_trace … si' sn'.
     160  REL sn sn' ∧
     161 
     162   (* Let labels be the costlabels observed in the trace of the source with all call post-labelled
     163     (last one excluded), that can be computed from the costlabels observed in the trace of
     164     the source language *)
     165 let labels ≝ map_labels_on_trace … m … (chop … (get_costlabels_of_trace …  t)) in
     166 
     167  (*The labels emitted by the trace of the source with all call post-labelled
     168    is a permutation of the labels emitted by the target trace (excluded the last one) *)
     169  ∃perm:is_permutation … labels (chop … (get_costlabels_of_trace … t')).
     170 
     171 (* that has a measurable fragment starting in s1' and ending in s2' *)
     172 ∃s1',s2'. measurable … s1' s2' … t' ∧
     173
     174(* Let abs_actions be the list of statically computed abstract actions
     175   associated to each label in labels. *)
     176 ∀abs_actions.
     177  abs_actions =
     178   dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →
     179
     180 (* Given an abstract state in relation with the first state of the measurable
     181    fragment *)
     182 ∀a1.R s1' a1 →
     183
     184 (* The final state of the measurable fragment is in relation with the one
     185   obtained by applying every semantics in abs_trace. *)
     186 R s2' (〚abs_actions〛 a1).
     187[2: @hide_prf normalize nodelta in prf; change with labels in prf : (???%);
     188    lapply(is_permutation_mem … prf … perm) -prf #prf
     189    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
     190    #lbl' #pc * #Hmem #EQ destruct
     191    >(proj1 … (static_analisys_ok … EQmap … Hmem))
     192    @(proj2 … (static_analisys_ok … EQmap … Hmem))
     193]
     194#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
     195#p_asm #p_asm' #prog_asm #rel #sim_cond #R #abelian #mT #map #EQmap #si #s1 #s2 #sn
     196#t #meas_t #si' #Hclass * #si'' * #abs_top * #abs_tail * #Rsi_si'' #Rsi_si'
     197lapply(correctness_theorem … p' prog no_dup) >EQt_prog normalize nodelta
     198#H cases(H … meas_t … Rsi_si'') -H #abs_top' * #abs_tail' * #sn'' * #t'' ** #Rsn_sn''
     199#Hperm * #s1'' * #s2'' #meas_t''
     200cases(cerco … sim_cond … EQmap … meas_t'' … Rsi_si') //
     201#sn' * #t' * #Rsn_sn' * #EQcost * #s1' * #s2' * #meas_t' normalize nodelta #Hcerco
     202%{sn'} %{t'} %
     203[ %{sn''} %{abs_top'} %{abs_tail'} /2 by conj/ ] %
     204 [ @(is_permutation_transitive … Hperm) >EQcost // ]
     205 %{s1'} %{s2'} %{meas_t'} #abs_actions #EQactions #a1 #Rs1_a1
     206 >(action_on_permutation … abelian)
     207 [@Hcerco [% | assumption]
     208 | >EQactions -EQactions @is_permutation_dependent_map //
     209 |
     210 ]
     211qed.
     212
    85213(* TODO:
    86 1. Monoide di costo: eliminare.
    87 2. Discorso I/O, fallimento della block-cost, ipotesi di premisurabilita'
    88    sull'assembler
     2141. Spostare chop e eliminare suffix.
     2152. La block cost non fallisce in caso di I/O.
    892163. Integrare la prima passata di Language nel risultato finale
    902175. Cambi al control flow: Paolo's trick (label = coppia label-pezzo di stato)
Note: See TracChangeset for help on using the changeset viewer.