Ignore:
Timestamp:
Dec 12, 2012, 2:43:03 PM (8 years ago)
Author:
tranquil
Message:

as_classify changed to a partial function
added a status for tailcalls

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2540 r2553  
    8282    sim_status_rel st1 st2 →
    8383    match as_classify … st1 with
    84     [ cl_call ⇒ ∀prf.
    85       (*
    86            st1' ------------S----------\
    87             ↑ \                         \
    88            st1 \--L--\                   \
    89             | \       \                   \
    90             S  \-C-\  st2_after_call →taa→ st2'
    91             |       \     ↑
    92            st2 →taa→ st2_pre_call
    93       *)
    94       ∃st2_pre_call.
    95       as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
    96       call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
    97       ∃st2_after_call,st2'.
    98       ∃taa2 : trace_any_any … st2 st2_pre_call.
    99       ∃taa2' : trace_any_any … st2_after_call st2'.
    100       as_execute … st2_pre_call st2_after_call ∧
    101       sim_status_rel st1' st2' ∧
    102       label_rel … st1' st2_after_call
    103     | cl_return ⇒
    104       (*
    105            st1
    106           / ↓
    107          | st1'----------S,L------------\
    108          S   \                           \
    109           \   \-----R-------\            |     
    110            \                 |           |
    111            st2 →taa→ st2_ret |           |
    112                         ↓   /            |
    113                    st2_after_ret →taaf→ st2'
    114 
    115          we also ask that st2_after_ret be not labelled if the taaf tail is
    116          not empty
    117       *)
    118       ∃st2_ret,st2_after_ret,st2'.
    119       ∃taa2 : trace_any_any … st2 st2_ret.
    120       ∃taa2' : trace_any_any_free … st2_after_ret st2'.
    121       (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
    122       as_classifier … st2_ret cl_return ∧
    123       as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
    124       ret_rel … sim_status_rel st1' st2_after_ret ∧
    125       label_rel … st1' st2'
    126     | cl_other ⇒
    127         (*         
    128         st1 → st1'
    129           |      \
    130           S      S,L
    131           |        \
    132          st2 →taaf→ st2'
    133          
    134          the taaf can be empty (e.g. tunneling) but we ask it must not be the
    135          case when both st1 and st1' are labelled (we would be able to collapse
    136          labels otherwise)
    137        *)
    138       ∃st2'.
    139       ∃taa2 : trace_any_any_free … st2 st2'.
    140       (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
    141       sim_status_rel st1' st2' ∧
    142       label_rel … st1' st2'
    143     | cl_jump ⇒
    144       (* just like cl_other, but with a hypothesis more *)
    145       as_costed … st1' →
    146       ∃st2'.
    147       ∃taa2 : trace_any_any_free … st2 st2'.
    148       (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
    149       sim_status_rel st1' st2' ∧
    150       label_rel … st1' st2'
     84    [ None ⇒ True
     85    | Some cl ⇒
     86      match cl with
     87      [ cl_call ⇒ ∀prf.
     88        (*
     89             st1' ------------S----------\
     90              ↑ \                         \
     91             st1 \--L--\                   \
     92              | \       \                   \
     93              S  \-C-\  st2_after_call →taa→ st2'
     94              |       \     ↑
     95             st2 →taa→ st2_pre_call
     96        *)
     97        ∃st2_pre_call.
     98        as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
     99        call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
     100        ∃st2_after_call,st2'.
     101        ∃taa2 : trace_any_any … st2 st2_pre_call.
     102        ∃taa2' : trace_any_any … st2_after_call st2'.
     103        as_execute … st2_pre_call st2_after_call ∧
     104        sim_status_rel st1' st2' ∧
     105        label_rel … st1' st2_after_call
     106      | cl_tailcall ⇒ ∀prf.
     107        (*
     108             st1' ------------S----------\
     109              ↑ \                         \
     110             st1 \--L--\                   \
     111              |         \                   \
     112              S         st2_after_call →taa→ st2'
     113              |             ↑
     114             st2 →taa→ st2_pre_call
     115        *)
     116        ∃st2_pre_call.
     117        as_tailcall_ident ? st2_pre_call = as_tailcall_ident ? («st1, prf») ∧
     118        ∃st2_after_call,st2'.
     119        ∃taa2 : trace_any_any … st2 st2_pre_call.
     120        ∃taa2' : trace_any_any … st2_after_call st2'.
     121        as_execute … st2_pre_call st2_after_call ∧
     122        sim_status_rel st1' st2' ∧
     123        label_rel … st1' st2_after_call
     124      | cl_return ⇒
     125        (*
     126             st1
     127            / ↓
     128           | st1'----------S,L------------\
     129           S   \                           \
     130            \   \-----R-------\            |     
     131             \                 |           |
     132             st2 →taa→ st2_ret |           |
     133                          ↓   /            |
     134                     st2_after_ret →taaf→ st2'
     135
     136           we also ask that st2_after_ret be not labelled if the taaf tail is
     137           not empty
     138        *)
     139        ∃st2_ret,st2_after_ret,st2'.
     140        ∃taa2 : trace_any_any … st2 st2_ret.
     141        ∃taa2' : trace_any_any_free … st2_after_ret st2'.
     142        (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
     143        as_classifier … st2_ret cl_return ∧
     144        as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
     145        ret_rel … sim_status_rel st1' st2_after_ret ∧
     146        label_rel … st1' st2'
     147      | cl_other ⇒
     148          (*         
     149          st1 → st1'
     150            |      \
     151            S      S,L
     152            |        \
     153           st2 →taaf→ st2'
     154           
     155           the taaf can be empty (e.g. tunneling) but we ask it must not be the
     156           case when both st1 and st1' are labelled (we would be able to collapse
     157           labels otherwise)
     158         *)
     159        ∃st2'.
     160        ∃taa2 : trace_any_any_free … st2 st2'.
     161        (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
     162        sim_status_rel st1' st2' ∧
     163        label_rel … st1' st2'
     164      | cl_jump ⇒
     165        (* just like cl_other, but with a hypothesis more *)
     166        as_costed … st1' →
     167        ∃st2'.
     168        ∃taa2 : trace_any_any_free … st2 st2'.
     169        (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
     170        sim_status_rel st1' st2' ∧
     171        label_rel … st1' st2'
     172      ]
    151173    ].
    152174
     
    202224  | tal_base_return st1 st1' _ _ ⇒ ?
    203225  | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ ?
     226  | tal_base_tailcall st1 st1' st1'' _ prf tlr1 ⇒ ?
    204227  | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ ?
    205228  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ ?
     
    211234  | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #coll
    212235  ]
     236| * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *#tlr2 * #EQ #EQ'
    213237| * #st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
    214238  [ * #EQfl *#K2 *#tlr2 *#L2 ** #EQ #coll #EQ'
     
    219243destruct
    220244<associative_taa_append_tal
    221   [1,2,3,4:%{(refl …)}] %{st2mid}
     245  [1,2,3,4,5:%{(refl …)}] %{st2mid}
    222246  [1,2:|*: %{G2} %{EQcall} ]
    223247  %{(taa_append_taa … taa2 taa2')}
    224248  [1,2: %{H2} %{G2} [%{K2}] %
     249  |5: %{st2mid'} %{H2} %{tlr2} % //
    225250  |*: %{st2mid'} %{H2}
    226251    [1,3: %1 [|%{(refl …)}] |*: %2 %{st2mid''} ]
     
    229254qed.
    230255
     256(*
     257check trace_any_label_label
    231258let rec tal_end_costed S st1 st2 (tal : trace_any_label S doesnt_end_with_ret st1 st2)
    232259  on tal : as_costed … st2 ≝
     
    242269]
    243270qed.
     271*)
    244272
    245273lemma taa_end_not_costed : ∀S,s1,s2.∀taa : trace_any_any S s1 s2.
     
    451479  | tal_base_return st1' st1'' H G ⇒ ?
    452480  | tal_base_call st1_pre_call st1_after_call st1' H G K tlr1 L ⇒ ?
     481  | tal_base_tailcall st1_pre_call st1_after_call st1' H G tlr1 ⇒ ?
    453482  | tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ?
    454483  | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ?
     
    485514  lapply (sim_execute … H st1_R_st2)
    486515  (* without try it fails... why? *)
    487   try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?);
     516  try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); normalize nodelta
    488517  [ #H lapply (H K) -H ] *
    489518  #st2' ** -st2 -st2'
     
    502531| (* tal_base_return *) whd
    503532  lapply (sim_execute … H st1_R_st2)
    504   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
     533  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); *
    505534  #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
    506535  ***** #ncost #J2 #K2
     
    511540| (* tal_base_call *) whd
    512541  lapply (sim_execute … H st1_R_st2)
    513   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?);
     542  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?);
    514543  #H elim (H G) -H
    515544  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
     
    538567  |*: whd <st1_L_st2' assumption
    539568  ]
     569| (* tal_base_tailcall *) whd
     570  lapply (sim_execute … H st1_R_st2)
     571  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?);
     572  #H elim (H G) -H
     573  * #st2_pre_call #G2 * #EQcall * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
     574  #st1_R_st2_mid #st1_L_st2_after_call
     575  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
     576  #st2_after_ret * #st2' * #tlr2 * #taa2''
     577  * #props #S
     578  %{st2_after_ret} %{st2'}
     579  %{(taa2 @ tal_base_tailcall ???? H2 G2 tlr2)}
     580  %{taa2''}
     581  %{props}
     582  % [%] %[|%[| %{EQcall} %[|%[|%[|%[| %{S} % ]]]]]]
    540583| (* tal_step_call *)
    541584  lapply (sim_execute … H st1_R_st2)
    542   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?);
     585  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?);
    543586  #H elim (H G) -H
    544587  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
     
    585628    ]
    586629  |3,6: @if_else_True whd in ⊢ (?%); <st1_L_st2' assumption
    587   |*: whd <st1_L_st2'' @(tal_end_costed … tl1)
     630  |*: whd <st1_L_st2'' @(trace_any_label_label … tl1)
    588631  ]
    589632| (* step_default *)
    590633  lapply (sim_execute … H st1_R_st2)
    591   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
     634  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); *
    592635  #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid
    593636  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid)
     
    603646  | (* can't happen *)
    604647    *** #_ #L' elim (absurd ?? K)
    605     whd >st1_L_st2_mid <L' @(tal_end_costed … tl1)
     648    whd >st1_L_st2_mid <L' @(trace_any_label_label … tl1)
    606649  ]
    607650  @if_else_True whd in ⊢ (?%); <st1_L_st2_mid assumption
     
    622665  ∀prf : as_classifier ? st1 cl_call.
    623666  flat_trace S start st2 (as_call_ident ? «st1, prf» :: stack)
     667| ft_advance_tailcall :
     668  ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
     669  ∀prf : as_classifier ? st1 cl_tailcall.
     670  flat_trace S start st2 (as_tailcall_ident ? «st1, prf» :: stack)
    624671| ft_advance_ret :
    625672  ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
     
    664711| IEVcost : costlabel → intensional_event
    665712| IEVcall : ident → intensional_event
     713| IEVtailcall : ident → ident → intensional_event
    666714| IEVret : ident → intensional_event.
    667715
     
    677725  let add ≝ add @ [IEVcall (as_call_ident ? «st1_mid, prf»)] in
    678726  ft_observables_aux (add @ acc) … pre1
     727| ft_advance_tailcall st1_mid st1' stack f pre1 _ prf ⇒
     728  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
     729  let add ≝ add @ [IEVtailcall f (as_tailcall_ident ? «st1_mid, prf»)] in
     730  ft_observables_aux (add @ acc) … pre1
    679731| ft_advance_ret st1_mid st1' stack f pre1 _ _ ⇒
    680732  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
     
    689741#acc #S #st1 #st2 #stack #ft lapply acc -acc elim ft -st2 -stack
    690742[ // ]
    691 #st2 #st3 #stack [3: #f ] #pre #H #G #IH #acc
     743#st2 #st3 #stack [3,4: #f ] #pre #H #G #IH #acc
    692744whd in ⊢ (??%(??%?));
    693745>IH >IH >append_nil //
     
    718770  [IEVcall (as_call_ident … «st3, G»)].
    719771#S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G
     772whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
     773>ft_extend_taa_obs
     774lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
     775[ #st2 * #ft #H #G >append_nil %
     776| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G
     777  >(not_costed_no_label … K)
     778  normalize nodelta //
     779]
     780qed.
     781
     782lemma ft_extend_taa_advance_tailcall_obs : ∀S,st1,st2,stack,f,st3,st4.
     783  ∀ft : flat_trace S st1 st2 (f :: stack).
     784  ∀taa : trace_any_any S st2 st3.
     785  ∀H : as_execute S st3 st4.∀G.
     786  ft_observables … (ft_advance_tailcall … (ft_extend_taa … ft taa) H G) =
     787  ft_observables … ft @
     788  option_to_list … (!l←as_label … st2;return IEVcost l) @
     789  [IEVtailcall f (as_tailcall_ident … «st3, G»)].
     790#S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G
    720791whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
    721792>ft_extend_taa_obs
     
    805876#S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 -st1' -stack
    806877[ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] %
    807 |*: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: * [*]] #cl [#ncost_st1']
     878|*: #st1_mid #st1' #stack [3,4: #f] #ft1 #ex [3: * [*]] #cl [#ncost_st1']
    808879  (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S
    809880  [1,2: (* other/jump *)
    810881    lapply (sim_execute … ex G')
    811     try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?);
     882    try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); normalize nodelta
    812883    [ #H lapply (H ncost_st1') -H ] *
    813884    #st2' *#taaf ** #ncost #G'' #H''
     
    838909      >S >L' %
    839910    ]
    840   |3: (* ret *)
     911  |3: (* tailcall *)
    841912    lapply (sim_execute … ex G')
    842     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
     913    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); #H elim (H cl) -H
     914    * #st2_pre_call #cl' * #EQcall * #st2_after_call * #st2'
     915    * #taa2 * #taa2' ** #ex' #G'' #H''
     916    lapply (refl_jmeq … (ft_advance_tailcall … ft1 ex cl))
     917    generalize in match (ft_advance_tailcall … ft1 ex cl) in ⊢ (????%→%);
     918    <EQcall in ⊢ (%→???%%→%);
     919    #ft1' #EQft1'
     920    %{st2_after_call} %{st2'}
     921    %[@(ft_advance_tailcall … f … ex' cl')
     922      @(ft_extend_taa … (taa_append_taa … taa taa2))
     923      assumption]
     924    %{taa2'}
     925    % [ %{H'' G''} ]
     926    >ft_extend_taa_advance_tailcall_obs
     927    lapply EQft1' lapply ft1' -ft1'
     928    >EQcall in ⊢ (%→???%%→%);
     929    #ft1' #EQft1' destruct (EQft1')
     930    whd in ⊢ (??%?);
     931    >ft_observables_aux_def >append_nil
     932    >S >L' %
     933  |4: (* ret *)
     934    lapply (sim_execute … ex G')
     935    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); *
    843936    #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
    844937    ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'}
     
    860953    ]
    861954    >S >L' %
    862   |4: (* call *)
     955  |5: (* call *)
    863956    lapply (sim_execute … ex G')
    864     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); #H elim (H cl) -H
     957    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); #H elim (H cl) -H
    865958    * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2'
    866959    * #taa2 * #taa2' ** #ex' #G'' #H''
Note: See TracChangeset for help on using the changeset viewer.