Changeset 2477


Ignore:
Timestamp:
Nov 20, 2012, 1:41:58 PM (7 years ago)
Author:
tranquil
Message:

status_simulation reformulated
definition of joint_classify split up in subdefinitions

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2463 r2477  
    7575  λS2 : abstract_status.
    7676  λsim_status_rel : status_rel S1 S2.
    77     ∀st1,cl,st1',st2.as_execute S1 st1 st1' →
     77    ∀st1,st1',st2.as_execute S1 st1 st1' →
    7878    sim_status_rel st1 st2 →
    79     ∀prf : as_classifier S1 st1 cl.
    80     match cl return λc.as_classifier S1 st1 c → ? with
    81     [ cl_call ⇒ λprf.
     79    match as_classify … st1 with
     80    [ cl_call ⇒ ∀prf.
    8281      (*
    8382           st1' ------------S----------\
     
    9897      sim_status_rel st1' st2' ∧
    9998      label_rel … st1' st2_after_call
    100     | cl_return ⇒ λ_.
     99    | cl_return ⇒
    101100      (*
    102101           st1
     
    121120      ret_rel … sim_status_rel st1' st2_after_ret ∧
    122121      label_rel … st1' st2'
    123     | _ ⇒ λ_.
    124       (*
    125          st1 → st1'
     122    | cl_other ⇒
     123        (*         
     124        st1 → st1'
    126125          |      \
    127126          S      S,L
     
    132131         case when both st1 and st1' are labelled (we would be able to collapse
    133132         labels otherwise)
    134          also notice that this allows to freely exchange cl_other and cl_jump,
    135          but if cl_jump imposed labels before, they will be kept afterwards *)
     133       *)
    136134      ∃st2'.
    137135      ∃taa2 : trace_any_any_free … st2 st2'.
    138       (* we ensure no labels are collapsed. Technicality? *)
    139136      (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
    140137      sim_status_rel st1' st2' ∧
    141138      label_rel … st1' st2'
    142     ] prf.
     139    | cl_jump ⇒
     140      (*
     141          st1 → st1'           st1 → st1'--------\
     142          |    /               |                  \
     143          S  S,L       or      S                  S,L
     144          |  /                 |                    \
     145          st2                 st2 →collapsable tal→ st2'
     146      *)
     147      (¬as_costed … st1 (* st1' will necessarily be costed *) ∧
     148       sim_status_rel st1' st2 ∧ label_rel … st1' st2) ∨
     149      (∃st2'.∃tal : trace_any_label … doesnt_end_with_ret st2 st2'.
     150        tal_collapsable … tal ∧
     151        sim_status_rel st1' st2' ∧ label_rel … st1' st2')
     152    ].
    143153
    144154
     
    257267  ].
    258268* #S2 #st12 #st22 #H #I #J % %[|%{(taa_base ??)} %[|%[|%[| %
     269qed.
     270
     271let rec tal_collapsable_eq_flag S fl st1 st2
     272  (tal : trace_any_label S fl st1 st2) on tal :
     273  tal_collapsable ???? tal → fl = doesnt_end_with_ret ≝
     274  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → fl = ?
     275  with
     276  [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_eq_flag ???? tl
     277  | tal_base_not_return _ st2' _ _ K ⇒ λ_.refl …
     278  | _ ⇒ Ⓧ
     279  ].
     280
     281let rec tal_collapsable_split S fl st1 st2
     282  (tal : trace_any_label S fl st1 st2) on tal :
     283  tal_collapsable ???? tal → ∃st2_mid.∃taa : trace_any_any S st1 st2_mid.∃H,I,J.
     284  tal ≃ taa @ tal_base_not_return … st2 H I J ≝
     285  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∃st2_mid,taa,H,I,J.
     286  tal ≃ taa @ tal_base_not_return … st2_mid ? H I J
     287  with
     288  [ tal_step_default fl' st1' st2' st3' H tl I J ⇒ ?
     289  | tal_base_not_return st1' st2' H I J ⇒ ?
     290  | _ ⇒ Ⓧ
     291  ].
     292[ * %{st1'} %{(taa_base …)} %{H} %{I} %{J} %
     293| #coll
     294  elim (tal_collapsable_split … tl coll) #st2_mid * #taa * #H' * #I' *#J'
     295  #EQ %{st2_mid} %{(taa_step … taa)} try assumption
     296  %{H'} %{I'} %{J'} lapply EQ lapply tl >(tal_collapsable_eq_flag … coll) -tl #tl
     297  #EQ >EQ %
     298]
     299qed.
     300
     301lemma tal_collapsable_to_rel_symm : ∀S,fl,st1,st2,tal.
     302tal_collapsable S fl st1 st2 tal → ∀S2,st12,st22,H,I,J.
     303  tal_rel … (tal_base_not_return S2 st12 st22 H I J) tal.
     304#S #fl #st1 #st2 #tal #coll #S2 #st12 #st22 #H #I #J
     305elim (tal_collapsable_split … coll) lapply tal
     306 >(tal_collapsable_eq_flag … coll) -tal #tal
     307#st2_mid * #taa *#H' *#I' *#J' #EQ >EQ % [%]
     308%[|%[|%[|%[|%[| % ]]]]]
    259309qed.
    260310
     
    431481  ]
    432482| (* tal_base_non_return *) whd
    433   cases G #G'
    434   elim (sim_execute … H st1_R_st2 G')
    435   #st2' ** -st2 -st2'
    436   [1,3: #st2 (* taa2 empty → st1' must be not cost_labelled *)
    437     ** whd in ⊢ (%→?); *
    438     [1,3: #ncost #R' #L' %2 /4 by conj/
    439     |*: * #ABS elim (ABS K)
     483  cases G -G #G
     484  lapply (sim_execute … H st1_R_st2)
     485  (* without try it fails... why? *)
     486  try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
     487  [ (* jump to none *)
     488    ** #K' #st1_R_st2' #st1_L_st2' %2 /4 by conj/
     489  | (* jump to some *)
     490    * #st2' * #tal2 ** #tal2_coll #st1_R_st2' #st1_L_st2'
     491    %1
     492    %{st2'} %{tal2} % [ /3 by conj/ ]
     493    @tal_collapsable_to_rel_symm assumption
     494  | (* other *)
     495    #st2' ** -st2 -st2'
     496    [1,3: #st2 (* taa2 empty → st1' must be not cost_labelled *)
     497      ** whd in ⊢ (%→?); *
     498      [1,3: #ncost #R' #L' %2 /4 by conj/
     499      |*: * #ABS elim (ABS K)
     500      ]
     501    |*: #st2 #st2_mid #st2' #taa2 #H2 #I2 *** #st1_R_st2' #st1_L_st2' %1
     502      %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 (or_intror ?? I2) ?))}
     503      [1,3: whd <st1_L_st2' assumption ]
     504      % [1,3: /2 by conj/]
     505      % try @refl %{st2_mid} %{taa2} %{H2} %[2,4: %[2,4: %]]
    440506    ]
    441   |*: #st2 #st2_mid #st2' #taa2 #H2 #I2 *** #st1_R_st2' #st1_L_st2' %1
    442     %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 (or_intror ?? I2) ?))}
    443     [1,3: whd <st1_L_st2' assumption ]
    444     % [1,3: /2 by conj/]
    445     % try @refl %{st2_mid} %{taa2} %{H2} %[2,4: %[2,4: %]]
    446507  ]
    447508| (* tal_base_return *) whd
    448   elim (sim_execute … H st1_R_st2 G)
     509  lapply (sim_execute … H st1_R_st2)
     510  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
    449511  #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
    450512  ***** #ncost #J2 #K2
     
    454516  %[ % | %[|%[|%[|%[| % ]]]]]]]
    455517| (* tal_base_call *) whd
    456   elim (sim_execute … H st1_R_st2 G)
     518  lapply (sim_execute … H st1_R_st2)
     519  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?);
     520  #H elim (H G) -H
    457521  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
    458522  #st1_R_st2_mid #st1_L_st2_after_call
     
    479543  ]
    480544| (* tal_step_call *)
    481   elim (sim_execute … H st1_R_st2 G)
     545  lapply (sim_execute … H st1_R_st2)
     546  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?);
     547  #H elim (H G) -H
    482548  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
    483549  #st1_R_st2_mid #st1_L_st2_after_call
     
    524590  ]
    525591| (* step_default *)
    526   elim (sim_execute … H st1_R_st2 G)
     592  lapply (sim_execute … H st1_R_st2)
     593  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
    527594  #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid
    528595  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid)
     
    740807|*: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: *] #cl
    741808  (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S
    742   elim (sim_execute … ex G' cl)
    743   [1,2: (* jump or other *)
     809  [ (* jump *)
     810    lapply (sim_execute … ex G')
     811    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
     812    [ ** #ncost #G'' #H''
     813      %{st2_mid} %{st2_mid}
     814      %[@(ft_extend_taa … taa)
     815        assumption]
     816      %{(taa_base …)} % [ %{H'' G''} ]
     817      whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
     818      >ft_extend_taa_obs <L'
     819      whd in match (as_label ? st1_mid);
     820      >(not_costed_no_label … ncost) >if_eq >S %
     821    | * #st2' * #tal ** #coll
     822      elim (tal_collapsable_split … coll) #st2_mid' * #taa2
     823      * #K2 * #J2 *#H2 #EQ  #G'' #H''
     824      %{st2'} %{st2'}
     825      %[@(ft_advance_flat … K2 J2)
     826        @(ft_extend_taa … (taa_append_taa … taa taa2))
     827        assumption]
     828      %{(taa_base …)} % [ %{H'' G''} ]
     829      >ft_extend_taa_advance_flat_obs
     830      whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
     831      <S <L' %
     832    ]
     833  | (* other *)
     834    lapply (sim_execute … ex G')
     835    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
    744836    #st2' *#taaf ** #ncost #G'' #H''
    745837    %{st2'} %{st2'}
     
    771863    ]
    772864  |3: (* ret *)
     865    lapply (sim_execute … ex G')
     866    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
    773867    #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
    774868    ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'}
     
    791885    >S >L' %
    792886  |4: (* call *)
     887    lapply (sim_execute … ex G')
     888    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); #H elim (H cl) -H
    793889    * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2'
    794890    * #taa2 * #taa2' ** #ex' #G'' #H''
  • src/joint/Traces.ma

    r2473 r2477  
    9999qed.
    100100
     101definition joint_classify_seq :
     102  ∀p : evaluation_params.state p → joint_seq p (globals … p) → status_class ≝
     103  λp,st,stmt.
     104  match stmt with
     105  [ CALL f args dest ⇒
     106    match function_of_call ?? (ev_genv p) st f with
     107    [ OK fn ⇒
     108      match description_of_function … fn with
     109      [ Internal _ ⇒ cl_call
     110      | External _ ⇒ cl_other
     111      ]
     112    | Error _ ⇒ cl_other
     113    ]
     114  | _ ⇒ cl_other
     115  ].
     116
     117definition joint_classify_step :
     118  ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝
     119  λp,st,stmt.
     120  match stmt with
     121  [ step_seq s ⇒ joint_classify_seq p st s
     122  | COND _ _ ⇒ cl_jump
     123  ].
     124
     125definition joint_classify_final :
     126  ∀p : evaluation_params.joint_fin_step p → status_class ≝
     127  λp,stmt.
     128  match stmt with
     129  [ GOTO _ ⇒ cl_other
     130  | RETURN ⇒ cl_return
     131  | TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *)
     132  ].
     133
    101134definition joint_classify :
    102135  ∀p : evaluation_params.state_pc p → status_class ≝
     
    104137  match fetch_statement ? p … (ev_genv p) (pc … st) with
    105138  [ OK f_s ⇒
    106     let 〈f, s〉 ≝ f_s in
    107     match s with
    108     [ sequential s _ ⇒
    109       match s with
    110       [ step_seq s ⇒
    111         match s with
    112         [ CALL f' args dest ⇒
    113           match function_of_call ?? (ev_genv p) st f' with
    114           [ OK fn ⇒
    115             match description_of_function … fn with
    116             [ Internal _ ⇒ cl_call
    117             | External _ ⇒ cl_other
    118             ]
    119           | Error _ ⇒ cl_other
    120           ]
    121         | _ ⇒ cl_other
    122         ]
    123       | COND _ _ ⇒ cl_jump
    124       ]
    125     | final s ⇒
    126       match s with
    127       [ GOTO _ ⇒ cl_other
    128       | RETURN ⇒ cl_return
    129       | TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *)
    130       ]
     139    match \snd f_s with
     140    [ sequential s _ ⇒ joint_classify_step p st s
     141    | final s ⇒ joint_classify_final p s
    131142    ]
    132143  | Error _ ⇒ cl_other
     
    142153#p #st
    143154whd in match joint_classify; normalize nodelta
    144 lapply (refl … (fetch_statement ? p … (ev_genv p) (pc … st)))
    145 elim (fetch_statement ?????) in ⊢ (???%→%);
     155inversion (fetch_statement ? p … (ev_genv p) (pc … st)) normalize nodelta
    146156[ * #f * [| * [ #lbl || #b #f #args ]]
    147157  [ * [| #a #lbl #next ]
     
    150160      | #op #a #a' | #op #a #a' #arg ||| #a #dpl #dph | #dpl #dph #arg
    151161      | #ext ] #next
    152       [ normalize nodelta
    153         lapply (refl … (function_of_call … (ev_genv p) st f'))
    154         elim (function_of_call ?????) in ⊢ (???%→%);
    155         [ #fn normalize nodelta
    156           lapply (refl … (description_of_function … (ev_genv p) fn))
    157           elim (description_of_function ?? fn) in ⊢ (???%→%); #fd
     162      [ whd in match joint_classify_step; whd in match joint_classify_seq;
     163        normalize nodelta
     164        inversion (function_of_call ?????) normalize nodelta
     165        [ #fn
     166          inversion (description_of_function ?? fn) #fd
    158167          #EQfd
    159168        | #e
     
    166175[|*: #ABS normalize in ABS; destruct(ABS) ]
    167176normalize nodelta #_
    168 %{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd} /3 by conj/
     177%{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd}
     178%{EQfd} %{EQfn} %
    169179qed.
    170180
Note: See TracChangeset for help on using the changeset viewer.