Changeset 2553


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

as_classify changed to a partial function
added a status for tailcalls

Location:
src
Files:
4 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''
  • src/common/StructuredTraces.ma

    r2531 r2553  
    1111  | cl_jump: status_class
    1212  | cl_call: status_class
     13  | cl_tailcall: status_class
    1314  | cl_other: status_class.
    1415
     
    1819  ; as_pc : DeqSet
    1920  ; as_pc_of : as_status → as_pc
    20   ; as_classify : as_status → status_class
     21  ; as_classify : as_status → option status_class
    2122  ; as_label_of_pc : as_pc → option costlabel
    22   ; as_after_return : (Σs:as_status. as_classify s = cl_call) → as_status → Prop
     23  ; as_after_return : (Σs:as_status. as_classify s = Some ? cl_call) → as_status → Prop
    2324  ; as_final: as_status → Prop
    24   ; as_call_ident : (Σs:as_status.as_classify s = cl_call) → ident
     25  ; as_call_ident : (Σs:as_status.as_classify s = Some ? cl_call) → ident
     26  ; as_tailcall_ident : (Σs:as_status.as_classify s = Some ? cl_tailcall) → ident
    2527  }.
    2628
    27 definition as_classifier ≝ λS,s,cl.as_classify S s = cl.
     29definition as_classifier ≝ λS,s,cl.as_classify S s = Some ? cl.
    2830definition as_call ≝ λS,s,f.as_call_ident S s = f.
    2931
     
    187189          as_costed S status_final →
    188190            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
     191  (* A tailcall, which ends the trace like a return. *)
     192  | tal_base_tailcall:
     193      ∀status_pre_fun_call: S.
     194      ∀status_start_fun_call: S.
     195      ∀status_final: S.
     196        as_execute S status_pre_fun_call status_start_fun_call →
     197        as_classifier S status_pre_fun_call cl_tailcall →
     198          trace_label_return S status_start_fun_call status_final →
     199            trace_any_label S ends_with_ret status_pre_fun_call status_final
    189200  (* A call followed by a non-empty trace. *)
    190201  | tal_step_call:
     
    220231 | tal_base_return pre _ _ _ ⇒ [as_pc_of … pre]
    221232 | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
     233 | tal_base_tailcall pre _ _ _ _ _ ⇒ [as_pc_of … pre]
    222234 ].
    223235
     
    255267    tal_unrepeating … tl
    256268  | tal_base_call pre _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace
     269  | tal_base_tailcall pre _ _ _ _ trace ⇒ tlr_unrepeating … trace
    257270  | _ ⇒ True
    258271  ].
     
    284297| #s1 #s2 #EX #CL
    285298| #s1 #s2 #s3 #EX #CL #AF #tlr #CS
     299| #s1 #s2 #s3 #EX #CL #tlr
    286300| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal
    287301| #fl #s1 #s2 #s3 #EX #tal #CL #CS
    288 ] whd in ⊢ (??(λ_.??%?)); % [ 2,4,6,8,10: % | *: skip ]
     302] whd in ⊢ (??(λ_.??%?)); % [2,4,6,8,10,12: % | *: skip ]
    289303qed.
    290304
     
    296310| #start #final #EX #CL #CS % // @(not_costed_no_label ?? CS)
    297311| #pre #start #final #EX #CL #AF #tlr #CS #CS' % // @(not_costed_no_label ?? CS')
     312| #pre #start #final #EX #CL #tlr #CS' % // @(not_costed_no_label ?? CS')
    298313| #fl' #pre #start #after #final #EX #CL #AF #tlr #CS #tal' #CS'
    299314  cases (tal_pc_list_start … tal')
     
    310325  | tac_base:
    311326      ∀status: S.
    312         as_classifier S status cl_call
     327        as_classifier S status cl_call ∨ as_classifier S status cl_tailcall
    313328          trace_any_call S status status
    314329  | tac_step_call:
     
    436451| tal_base_return _ _  _ _ ⇒ I
    437452| tal_base_call _ _ _ _ _ _ _ C ⇒ C
     453| tal_base_tailcall _ _ _ _ _ _ ⇒ I
    438454| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
    439455| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
     
    456472
    457473lemma trace_any_call_call : ∀S,s,s'.
    458   trace_any_call S s s' → as_classifier S s' cl_call.
     474  trace_any_call S s s' → as_classifier S s' cl_call ∨ as_classifier S s' cl_tailcall.
    459475#S #s #s' #T elim T [1,3: //]
    460476#H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 //
     
    616632      tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
    617633      tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2
     634  | tal_base_tailcall st1 st1' st1'' _ prf tlr1 ⇒
     635    fl2 = ends_with_ret ∧
     636    ∃st2mid,G.as_tailcall_ident S2 («st2mid, G») = as_tailcall_ident ? «st1, prf» ∧
     637    ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
     638    ∃tlr2 : trace_label_return ? st2mid' st2'.
     639      tal2 ≃ taa @ (tal_base_tailcall … H G tlr2) ∧ tlr_rel … tlr1 tlr2
    618640  | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒
    619641    ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
     
    636658let rec tal_collapsable_eq_fl S1 fl1 s1 s1'
    637659  (tal1 : trace_any_label S1 fl1 s1 s1') on tal1 :
    638   tal_collapsable … tal1 → fl1 = doesnt_end_with_ret ≝ ?.
    639 cases tal1 -fl1 -s1 -s1' //
    640 [ #s1 #s1' #H #I *
    641 | #s1 #s1' #s1'' #s1''' #s1'''' #H #I #J #tlr #K #tl *
    642 | #fl1 #s1 #s1' #s1'' #H #tl #I #J @(tal_collapsable_eq_fl … tl)
    643 ]
    644 qed.
     660  tal_collapsable … tal1 → fl1 = doesnt_end_with_ret ≝
     661match tal1 return λfl1,s1,s1',tal1.
     662  tal_collapsable S1 fl1 s1 s1' tal1 → fl1 = doesnt_end_with_ret with
     663[ tal_base_not_return _ _ _ _ _ ⇒ λ_.refl …
     664| tal_step_default fl1 _ st1' st1'' _ tl1 _ _ ⇒ tal_collapsable_eq_fl … tl1
     665| _ ⇒ Ⓧ
     666].
    645667
    646668let rec tal_rel_eq_fl S1 fl1 s1 s1' S2 fl2 s2 s2'
     
    651673  | tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ?
    652674  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ?
     675  | tal_base_tailcall st1 st1' st1'' _ _ tlr1 ⇒ let BASE_TC ≝ 0 in ?
    653676  | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?
    654677  | tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ?
    655678  ].
    656679-fl1 -s1 -s1'
    657 [1,2,3: -tal_rel_eq_fl #tal2 * //
     680[1,2,3,4: -tal_rel_eq_fl #tal2 * //
    658681| #tal2 * #s2_mid * #G2 * #call * #taa2 * #s2' *#H2 *
    659682  [ * #EQ1 *#K2 *#tlr2 *#L2 ** #_ #coll #_ >(tal_collapsable_eq_fl … coll) //
     
    691714  | tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ?
    692715  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ?
     716  | tal_base_tailcall st1 st1' st1'' _ _ tlr1 ⇒ let BASE_TC ≝ 0 in ?
    693717  | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?
    694718  | tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ?
    695719  ].
    696720-fl1 -s1 -s1'
    697 [1,2,3: -tal_rel_collapsable #tal2 * *
     721[1,2,3,4: -tal_rel_collapsable #tal2 * *
    698722  #EQ * #s2 * #taa2 *#H *#G *#K #EQ' destruct @taa_append_collapsable %
    699723| #tal2 *
     
    725749  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
    726750  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
     751      flatten_trace_label_return … call_trace
     752  | tal_base_tailcall pre_fun_call start_fun_call final _ _ call_trace ⇒
    727753      flatten_trace_label_return … call_trace
    728754  | tal_base_return the_status _ _ _ ⇒ [ ]
     
    819845  | tal_base_return st1 st1' H G ⇒ ?
    820846  | tal_base_call st1 st1' st1'' H G K tlr1 L ⇒ ?
     847  | tal_base_tailcall st1 st1' st1'' H G tlr1 ⇒ ?
    821848  | tal_step_call fl1 st1 st1' st1'' st1''' H G K tlr1 L tl1 ⇒ ?
    822849  | tal_step_default fl1 st1 st1' st1'' H tl1 G K ⇒ ?
     
    843870  >EQ1 >EQ2 normalize nodelta #_ #_
    844871  >(tal_rel_to_traces_same_flatten … H_tal) @refl
    845 |2,3,4,5,6:
    846   [1,2,3: * #EQ destruct(EQ)]
    847   [1,2,3,4: * #st_mid [1,2:|*: * #G' * #call ] * #taa
     872|2,3,4,5,6,7:
     873  [1,2,3,4: * #EQ destruct(EQ)]
     874  [1,2,3,4,5: * #st_mid [1,2:|*: * #G' * #call ] * #taa
    848875    [ *#H' *#G' *#K' #EQ
    849876    | *#H' *#G' #EQ
    850877    | *#st_mid' *#H' * [|*#st2_mid''] *#K' *#tlr2 *#L'
    851878      [|*#tl2 *] * #EQ #H_tlr [| #H_tl]
     879    | *#st_mid' *#H' *#tlr2 * #EQ #H_tlr
    852880    | *#st_fun *#H' *
    853881      [*#fl_EQ destruct(fl_EQ) |* #st2_mid ] *#K' *#tlr2 *#L'
     
    858886  ]
    859887  [1,2: %
    860   |3: @(tlr_rel_to_traces_same_flatten … H_tlr)
    861   |4,5: <map_append
     888  |3,5: @(tlr_rel_to_traces_same_flatten … H_tlr)
     889  |4,6: <map_append
    862890    >(tal_collapsable_flatten … H_tl) >append_nil
    863891    >(tlr_rel_to_traces_same_flatten … H_tlr) %
    864   |6: <map_append
     892  |7: <map_append
    865893    >(tlr_rel_to_traces_same_flatten … H_tlr)
    866894    >(tal_rel_to_traces_same_flatten … H_tl)
  • src/joint/Traces.ma

    r2538 r2553  
    124124
    125125definition joint_classify_final :
    126   ∀p : evaluation_params.joint_fin_step p → status_class ≝
    127   λp,stmt.
     126  ∀p : evaluation_params.state p → joint_fin_step p → status_class ≝
     127  λp,st,stmt.
    128128  match stmt with
    129129  [ GOTO _ ⇒ cl_other
    130130  | RETURN ⇒ cl_return
    131   | TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *)
     131  | TAILCALL _ f args ⇒
     132    match (! bl ← block_of_call … (ev_genv p) f st ;
     133            fetch_function … (ev_genv p) bl) with
     134    [ OK id_fn ⇒
     135      match \snd id_fn with
     136      [ Internal _ ⇒ cl_tailcall
     137      | External _ ⇒ cl_return
     138      ]
     139    | Error _ ⇒ cl_other
     140    ]
    132141  ].
    133142
    134143definition joint_classify :
    135   ∀p : evaluation_params.state_pc p → status_class ≝
     144  ∀p : evaluation_params.state_pc p → option status_class ≝
    136145  λp,st.
    137   match fetch_statement … (ev_genv p) (pc … st) with
    138   [ OK i_f_s ⇒
    139     match \snd i_f_s with
    140     [ sequential s _ ⇒ joint_classify_step p st s
    141     | final s ⇒ joint_classify_final p s
    142     | FCOND _ _ _ _ ⇒ cl_jump
    143     ]
    144   | Error _ ⇒ cl_other
     146  ! 〈i,f,s〉 ← res_to_opt … (fetch_statement … (ev_genv p) (pc … st)) ;
     147  match s with
     148  [ sequential s _ ⇒ Some ? (joint_classify_step p st s)
     149  | final s ⇒ Some ? (joint_classify_final p st s)
     150  | FCOND _ _ _ _ ⇒ Some ? cl_jump
    145151  ].
    146152
     
    179185
    180186lemma joint_classify_call : ∀p : evaluation_params.∀st.
    181   joint_classify p st = cl_call →
     187  joint_classify p st = Some ? cl_call →
    182188  ∃i_f,f',args,dest,next,bl,i',fd'.
    183189  fetch_statement … (ev_genv p) (pc … st) =
     
    187193#p #st
    188194whd in match joint_classify; normalize nodelta
    189 inversion (fetch_statement … (ev_genv p) (pc … st)) normalize nodelta
    190 [2: #e #_ #ABS destruct(ABS) ]
     195inversion (fetch_statement … (ev_genv p) (pc … st))
     196[2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
    191197* #i_f * [2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
    192   normalize in ⊢ (%→?); #ABS destruct(ABS) ]
    193 @cond_call_other
    194 [ #a #lbl #nxt #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
    195 |3: #s #no_call #nxt #_ whd in match joint_classify_step;
    196   normalize nodelta >(no_call_other … no_call) #ABS destruct(ABS)
    197 ]
    198 #f' #args #dest #nxt #fetch
     198>m_return_bind normalize nodelta
     199  [3: whd in match joint_classify_final; normalize nodelta
     200    generalize in ⊢ (??(?? (match % with [ _ ⇒ ? | _ ⇒ ?]))?→?); * [* #i' * #fd | #e ]
     201    normalize nodelta ]
     202  #ABS destruct(ABS) ]
     203@cond_call_other [ #a #lbl | #f' #args #dest | #s #s_no_call ] #nxt #fetch >m_return_bind
     204normalize nodelta
     205[ normalize in ⊢ (%→?); #ABS destruct(ABS)
     206|3: whd in match joint_classify_step;
     207  normalize nodelta >(no_call_other … s_no_call) #ABS destruct(ABS)
     208]
    199209whd in match joint_classify_step; whd in match joint_classify_seq;
    200210normalize nodelta
     
    215225
    216226definition joint_after_ret : ∀p:evaluation_params.
    217   (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝
     227  (Σs : state_pc p.joint_classify p s = Some ? cl_call) → state_pc p → Prop ≝
    218228λp,s1,s2.
    219229match fetch_statement … (ev_genv p) (pc … s1) with
     
    228238
    229239definition joint_call_ident : ∀p:evaluation_params.
    230   (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝
     240  (Σs : state_pc p.joint_classify p s = Some ? cl_call) → ident ≝
    231241(* this is a definition without a dummy ident :
    232242λp,st.
     
    283293].
    284294
     295definition joint_tailcall_ident : ∀p:evaluation_params.
     296  (Σs : state_pc p.joint_classify p s = Some ? cl_tailcall) → ident ≝
     297λp,st.
     298let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
     299match fetch_statement … (ev_genv p) (pc … st) with
     300[ OK x ⇒
     301  match \snd x with
     302  [ final s ⇒
     303    match s with
     304    [ TAILCALL _ f' args ⇒
     305      match
     306        (! bl ← block_of_call … (ev_genv p) f' st;
     307         fetch_internal_function … (ev_genv p) bl) with
     308      [ OK i_f ⇒ \fst i_f
     309      | _ ⇒ dummy
     310      ]
     311    | _ ⇒ dummy
     312    ]
     313  | _ ⇒ dummy
     314  ]
     315| _ ⇒ dummy
     316].
     317
    285318definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?.
    286319*#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim
     
    342375   (* as_after_return ≝ *) (joint_after_ret p)
    343376   (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) (exit p) s ≠ None ?)
    344    (* as_call_ident ≝ *) (joint_call_ident p).
     377   (* as_call_ident ≝ *) (joint_call_ident p)
     378   (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).
  • src/joint/lineariseProof.ma

    r2551 r2553  
    10241024*)
    10251025
    1026 axiom symbol_for_block_transf :
     1026lemma symbol_for_block_match:
     1027    ∀M:matching.∀initV,initW.
     1028     (∀v,w. match_var_entry M v w →
     1029      size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
     1030    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
     1031    ∀MATCH:match_program … M p p'.
     1032    ∀b: block.
     1033    symbol_for_block … (globalenv … initW p') b =
     1034    symbol_for_block … (globalenv … initV p) b.
     1035* #A #B #V #W #match_fn #match_var #initV #initW #H
     1036#p #p' * #Mvars #Mfn #Mmain
     1037#b
     1038whd in match symbol_for_block; normalize nodelta
     1039whd in match globalenv in ⊢ (???%); normalize nodelta
     1040whd in match (globalenv_allocmem ????);
     1041change with (add_globals ?????) in match (foldl ?????);
     1042>(proj1 … (add_globals_match … initW … Mvars))
     1043[ % |*:]
     1044[ * #idr #v * #idr' #w #MVE %
     1045  [ inversion MVE
     1046    #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct %
     1047  | @(H … MVE)
     1048  ]
     1049| @(matching_fns_get_same_blocks … Mfn)
     1050  #f #g @match_funct_entry_id
     1051]
     1052qed.
     1053
     1054lemma symbol_for_block_transf :
    10271055 ∀A,B,V,init.∀prog_in : program A V.
    10281056 ∀trans : ∀vars.A vars → B vars.
    10291057 let prog_out ≝ transform_program … prog_in trans in
    1030  ∀bl, i.
    1031  symbol_for_block … (globalenv … init prog_in) bl = Some ? i →
    1032  symbol_for_block … (globalenv … init prog_out) bl = Some ? i.
     1058 ∀bl.
     1059 symbol_for_block … (globalenv … init prog_out) bl =
     1060 symbol_for_block … (globalenv … init prog_in) bl.
     1061#A #B #V #iV #p #tf @(symbol_for_block_match … (transform_program_match … tf ?))
     1062#v0 #w0 * //
     1063qed.
    10331064
    10341065lemma fetch_function_transf :
     
    10471078 #H @('bind_inversion H) -H #fd #eq_find_funct
    10481079 whd in ⊢ (??%?→?); #EQ destruct(EQ)
    1049  >(symbol_for_block_transf A B … eq_symbol_for_block) >m_return_bind
     1080 >(symbol_for_block_transf … trans) >eq_symbol_for_block >m_return_bind
    10501081 >(find_funct_ptr_transf A B …  eq_find_funct) %
    10511082qed.
     
    12801311normalize //
    12811312qed.
    1282 check pc_of_label
     1313
    12831314lemma fetch_statement_sigma_commute:
    12841315  ∀p,p',graph_prog,pc,f,fn,stmt.
     
    12881319  fetch_statement (make_sem_graph_params p p') …
    12891320    (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 →
    1290 (*  All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma
     1321  All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma
    12911322      (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl).
    12921323      pc_of_label (make_sem_lin_params p p') …
     
    12941325          (pc_block pc)
    12951326          lbl = return sigma_pc … prf)
    1296     (stmt_explicit_labels … stmt) ∧ *)
     1327    (stmt_explicit_labels … stmt) ∧
    12971328  match stmt with
    12981329  [  sequential s nxt ⇒
     
    13511382#lin_pt #lin_pt_spec #EQ whd in EQ : (??%?); destruct(EQ)
    13521383lapply(stmt_at_sigma_commute ???????? (good fn) ??? graph_stmt)
    1353 [@lin_pt_spec|@(pi2 … (\fst (linearise_int_fun … fn)))|] * #H1 (* #H2 %
    1354 [ @In_All
    1355   #lab #lab_in
    1356   lapply (All_In ??? lab H1 ?)
    1357   [ @Exists_append_r assumption ]
    1358   inversion (sigma graph_fun lab) [#_ * #ABS @⊥ @ABS %]
    1359   #lin_pt #EQsigma #_
    1360   %
    1361   [ @hide_prf whd %
    1362   | whd in match sigma_pc; normalize nodelta
    1363     @opt_safe_elim #pc_lin
    1364   ] whd in match sigma_pc_opt;
    1365   normalize nodelta >(eqZb_false … Hbl) >fetchfn normalize nodelta
    1366   >m_return_bind >point_of_pc_of_point >EQsigma
    1367   #EQ whd in EQ : (??%?); destruct(EQ)
    1368   whd in match pc_of_label; normalize nodelta
    1369   >(fetch_internal_function_transf … fetchfn) >m_return_bind
    1370   inversion (point_of_label ????)
    1371   [2: #lin_pt' #EQ lapply (all_labels_in … EQ) >EQsigma
    1372     #EQ' destruct % ]
    1373   change with (If ? then with prf do ? else ? = ? → ?)   
    1374   @If_elim <(lin_code_has_label … (mk_lin_params p))
    1375   [ #_ whd in ⊢ (??%?→?); #EQ destruct ]
    1376   #ABS cases (absurd ?? ABS)
    1377   lapply (pi2 … (\fst (linearise_int_fun … graph_fun)) … )
    1378   [2:
    1379   normalize nodelta
    1380  
    1381   >m_return_bind whd in ⊢ (?(??%?));
    1382     % #ABS destruct(ABS)
    1383    
    1384       >(eqZb_false … Hbl) normalize nodelta >fetchfn
    1385     >m_return_bind >point_of_pc_of_point inversion(sigma graph_fun lab) in lab_spec;
    1386     [ #_ * #ABS @⊥ @ABS %] #linear_pt #linear_pt_spec #_ >m_return_bind
    1387     whd in match pc_of_label; normalize nodelta
    1388     >(fetch_internal_function_transf … fetchfn) >m_return_bind
    1389 
    1390 ] lapply H2 *)
    1391 cases (stmt) in H1; [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
     1384[@lin_pt_spec|@(pi2 … (\fst (linearise_int_fun … fn)))|] * #H1 #H2 %
     1385[ cases stmt in H2;
     1386  [ * [#s|#a#lbl]#nxt | #s | *]
     1387  normalize nodelta
     1388  [ * #stmt_at_EQ #_ | ** #stmt_at_EQ #_ | #stmt_at_EQ ]
     1389  cases (pi2 … (\fst (linearise_int_fun … fn)) … stmt_at_EQ)
     1390  #H #_
     1391  [1,2,4: @(All_mp … H) #lbl @(pc_of_label_sigma_commute … good … fetchfn)
     1392  |3: cases H -H #H #_ %{I} @(pc_of_label_sigma_commute … good … fetchfn) @H
     1393  ]
     1394]
     1395cases (stmt) in H1 H2; [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
    13921396#all_labels_spec #H3 whd in match fetch_statement; normalize nodelta
    13931397>pc_block_sigma_commute
     
    14601464  | >H3 >m_return_bind %
    14611465]
    1462 qed. 
     1466qed.
    14631467
    14641468
     
    14681472qed.
    14691473
     1474lemma res_to_opt_preserve : ∀X,Y,P,F,m,n.
     1475  res_preserve X Y P F m n → opt_preserve X Y P F (res_to_opt … m) (res_to_opt … n).
     1476#X #Y #P #F #m #n #H #x #EQ
     1477cases (H x ?)
     1478[ #prf #EQ' %{prf} >EQ' %
     1479| cases m in EQ; normalize #x #EQ destruct %
     1480]
     1481qed.
     1482
     1483lemma sigma_pc_exit :
     1484  ∀p,p',graph_prog,sigma,pc,prf.
     1485  let exit ≝ mk_program_counter «mk_block Code (-1), refl …» one in
     1486  pc = exit →
     1487  sigma_pc p p' graph_prog sigma pc prf = exit.
     1488#p #p' #graph_prog #sigma #pc #prf
     1489whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc'
     1490#EQ1 #EQ2 destruct
     1491whd in match sigma_pc_opt in EQ1; whd in EQ1 : (??%?);
     1492destruct %
     1493qed.
     1494
     1495(* this should make things easier for ops using memory (where pc cant happen) *)
     1496definition bv_no_pc : beval → Prop ≝
     1497λbv.match bv with [ BVpc _ _ ⇒ False | _ ⇒ True ].
     1498
     1499lemma bv_pc_other :
     1500  ∀P : beval → Prop.
     1501  (∀pc,p.P (BVpc pc p)) →
     1502  (∀bv.bv_no_pc bv → P bv) →
     1503  ∀bv.P bv.
     1504#P #H1 #H2 * /2/ qed.
     1505
     1506lemma sigma_bv_no_pc : ∀p,p',graph_prog,sigma,bv,prf.
     1507  bv_no_pc bv →
     1508  sigma_beval p p' graph_prog sigma bv prf = bv.
     1509#p #p' #graph_prog #sigma *
     1510[|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ]
     1511#prf * whd in match sigma_beval; normalize nodelta
     1512@opt_safe_elim #bv' normalize #EQ destruct(EQ) %
     1513qed.
     1514
     1515lemma bv_no_pc_wf : ∀p,p',graph_prog,sigma,bv.
     1516bv_no_pc bv → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?.
     1517#p #p' #graph_prog #sigma *
     1518[|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] *
     1519% whd in ⊢ (??%?→?); #ABS destruct(ABS) qed.
     1520
     1521lemma Byte_of_val_inv : ∀bv,e,by.Byte_of_val e bv = return by → bv = BVByte by.
     1522* [|| #a #b #c |#p | #p | #p #pa | #p #pa ] #e #by
     1523  whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.
     1524
     1525lemma sigma_pc_no_exit :
     1526  ∀p,p',graph_prog,sigma,pc,prf.
     1527  let exit ≝ mk_program_counter «mk_block Code (-1), refl …» one in
     1528  pc ≠ exit →
     1529  sigma_pc p p' graph_prog sigma pc prf ≠ exit.
     1530#p #p' #graph_prog #sigma #pc #prf
     1531@(eqZb_elim (block_id (pc_block pc)) (-1))
     1532[ #Hbl
     1533  whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc'
     1534  whd in match sigma_pc_opt; normalize nodelta
     1535  >Hbl whd in ⊢ (??%?→?); #EQ destruct(EQ) // ]
     1536#NEQ #_ inversion (sigma_pc ??????)
     1537** #r #id #EQr #off #EQ
     1538lapply (pc_block_sigma_commute …prf) >EQ #EQ' >EQ'
     1539% #ABS destruct(ABS) cases NEQ #H @H -H
     1540cases (pc_block ?) in e0; * #r #id' #EQ'' >EQ'' #EQ''' destruct(EQ''') %
     1541qed.
    14701542
    14711543definition linearise_status_rel:
     
    14911563>EQ2
    14921564whd in ⊢ (%→%);
     1565whd in match (exit ?);
     1566letin exit_pc ≝ (mk_program_counter «mk_block Code (-1), refl …» one)
    14931567#H lapply (opt_to_opt_safe … H)
    14941568@opt_safe_elim -H #res #_ whd in match is_final; normalize nodelta
     
    14961570#H  @('bind_inversion H) -H
    14971571** #id #int_f #stmt
    1498 #stmt_spec lapply(fetch_statement_sigma_commute ???????? good (proj1 … prf) stmt_spec)
     1572#stmt_spec cases (fetch_statement_sigma_commute ???????? good (proj1 … prf) stmt_spec)
    14991573cases stmt in stmt_spec; -stmt normalize nodelta
    1500 [1,3: [ #a #b #_| #a #b #c #d #e] #_ #ABS whd in ABS : (???%); destruct(ABS)]
    1501 #fin_step cases(fin_step) -fin_step normalize nodelta
    1502 [1,3: [#l| #a #b #c] #_ #_ #ABS whd in ABS: (???%); destruct(ABS)]
    1503 #fetch_graph_spec #fetch_lin_spec
     1574[1,3: [ #a #b #_| #a #b #c #d #e] #_ #_ #ABS whd in ABS : (???%); destruct(ABS)]
     1575* normalize nodelta
     1576[1,3: [#l| #a #b #c] #_ #_ #_ #ABS whd in ABS: (???%); destruct(ABS)]
     1577#fetch_graph_spec #_ #fetch_lin_spec
    15041578#H >fetch_lin_spec >m_return_bind normalize nodelta
    1505 @('bind_inversion H) -H #state_pc #state_pc_spec
    1506 elim(pop_frame_commute
    1507   p p' graph_prog sigma gss ? id int_f ? (hide_prf … (proj2 … prf)) … state_pc_spec)
    1508 #wf_state_pc normalize nodelta #sigma_state_pc_commute >sigma_state_pc_commute
    1509 >m_return_bind @eq_program_counter_elim normalize nodelta
    1510 [2: #_ #EQ whd in EQ : (???%); destruct(EQ)] #state_pc_spec #H
    1511 @eq_program_counter_elim normalize nodelta
    1512 [2: * #ABS @⊥ @ABS whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
    1513     @opt_safe_elim #next_pc @eqZb_elim normalize nodelta >state_pc_spec
    1514     [2: * #ABS1 @⊥ @ABS1 normalize %] #_ #EQ whd in EQ : (??%?); destruct(EQ) %
    1515 |   #_ @('bind_inversion H) -H #list_val #list_val_spec 
    1516 elim(read_result_commute p p' graph_prog sigma gss ? ? ? ? ? list_val_spec)
    1517 [2: @hide_prf @(proj2 … prf)] #wf_lm #EQ >EQ -EQ >m_return_bind
    1518 whd in match Word_of_list_beval in ⊢ (% → ?); normalize nodelta
    1519 #H @('bind_inversion H) -H * #b1 #l1 #b1_l1_spec #H
    1520 cases list_val in list_val_spec wf_lm b1_l1_spec; -list_val normalize nodelta
    1521 [ #_ #l #ABS whd in ABS : (???%); destruct(ABS)]
    1522 #b2 #l2 #b2_l2_spec #wf_b2_l2 #H1 @('bind_inversion H1) -H1
    1523 #bt whd in match Byte_of_val; normalize nodelta
    1524 cases (b2) in b2_l2_spec wf_b2_l2; -b2 normalize nodelta
    1525 [1,2,3,5,6,7: [||#a #b #c | #p | #p #p'] #a #b [6: #_ #a] #ABS whd in ABS : (???%); destruct(ABS)]
    1526 #by #by_l2_spec #wf_by_l2 #EQ whd in EQ : (???%); destruct(EQ) #EQ whd in EQ : (???%);
    1527 destruct(EQ) @('bind_inversion H) -H * #by1 #l3
    1528 cases l1 in by_l2_spec wf_by_l2; -l1 normalize nodelta [ #_ #a #ABS whd in ABS : (???%); destruct(ABS)]
    1529 #val #l1 #b1_val_l1_spec #wf_b1_val_l1 #H @('bind_inversion H) -H #by1
    1530 cases val in b1_val_l1_spec wf_b1_val_l1; -val
    1531 [1,2,3,5,6,7: [||#a #b #c | #p | #p #p'] #a #b [6: #_ #a] whd in match Byte_of_val; normalize nodelta
    1532 #ABS whd in ABS : (???%); destruct(ABS)]
    1533 #by2 #b1_by2_l1_spec #wf_b1_by2_l1 whd in match Byte_of_val; normalize nodelta
    1534 #EQ whd in EQ : (???%); destruct(EQ) #EQ whd in EQ : (???%); destruct(EQ)
    1535 #H @('bind_inversion H) -H * #by2 #l2
    1536 cases(l3) in b1_by2_l1_spec wf_b1_by2_l1; -l3 normalize nodelta
    1537 [#_ #a #ABS whd in ABS : (???%); destruct(ABS)]
    1538 #val #l1 #b1_by1_val_l1_spec #wf_b1_by1_val_l1 #H @('bind_inversion H) -H
    1539 #by3 cases val in b1_by1_val_l1_spec wf_b1_by1_val_l1; -val normalize nodelta
    1540 [1,2,3,5,6,7: [||#a #b #c | #p | #p #p'] #a #b [6: #_ #a] #ABS whd in ABS : (??%%); destruct(ABS)] 
    1541 #by3 #b1_by1_by3_l1_spec #wf_b1_by1_by3_l1 #EQ whd in EQ : (???%); destruct(EQ)
    1542 #EQ whd in EQ : (???%); destruct(EQ) #H @('bind_inversion H) -H *
    1543 #by3 #l1 cases l2 in  b1_by1_by3_l1_spec  wf_b1_by1_by3_l1; -l2 normalize nodelta
    1544 [#_ #a #ABS whd in ABS : (???%); destruct(ABS)]
    1545 #val #l2 #_ #wf_b1_by1_by2_val #H @('bind_inversion H) -H #by4
    1546 cases val in wf_b1_by1_by2_val; -val normalize nodelta
    1547 [1,2,3,5,6,7: [|| #a #b #c |#p | #p #p'|#p #pa] #a #ABS whd in ABS : (???%); destruct(ABS)]
    1548 #by5 #wf_list #EQ whd in EQ : (???%); destruct(EQ) #EQ whd in EQ : (???%); destruct(EQ)  cases l1 in wf_list; -l1 normalize nodelta [2: #val #l #a #ABS whd in ABS : (???%); destruct(ABS)]
    1549 #wf_list #EQ whd in EQ : (???%); destruct(EQ)
    1550 @opt_safe_elim #l #H normalize in H; destruct(H) normalize % #ABS destruct(ABS)
     1579letin graph_ge ≝ (ev_genv (graph_prog_params p p' graph_prog stack_sizes))
     1580letin lin_ge ≝ (ev_genv (lin_prog_params p p' (linearise p graph_prog) stack_sizes))
     1581cut (preserving … res_preserve …
     1582       (sigma_state … gss)
     1583       (λl.λ_ : True.l)
     1584       (λst.
     1585          do st' ← pop_frame … graph_ge id int_f st;
     1586          if eq_program_counter (pc … st') exit_pc then
     1587          do vals ← read_result … graph_ge (joint_if_result … int_f) st ;
     1588            Word_of_list_beval vals
     1589          else
     1590            Error ? [ ])
     1591       (λst.
     1592          do st' ← pop_frame … lin_ge id (\fst (linearise_int_fun … int_f)) st;
     1593          if eq_program_counter (pc … st') exit_pc then
     1594          do vals ← read_result … lin_ge (joint_if_result … (\fst (linearise_int_fun … int_f))) st ;
     1595            Word_of_list_beval vals
     1596          else
     1597            Error ? [ ]))
     1598[ #st #prf @mfr_bind [3: @pop_frame_commute |*:]
     1599  #st' #prf' @eq_program_counter_elim 
     1600  [ #EQ_pc >(sigma_pc_exit … EQ_pc) normalize nodelta
     1601    @mfr_bind [3: @read_result_commute |*:]
     1602    #lbv #prf_lbv @opt_safe_elim #lbv' #EQ_lbv'
     1603    @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe …
     1604        (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉))
     1605    [
     1606    | * -lbv -lbv' #by1 #lbv #lbv_prf
     1607      @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe …
     1608        (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉))
     1609    [ @opt_safe_elim #lbv' #EQ_lbv'
     1610    |* -lbv #by2 #lbv #lbv_prf
     1611      @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe …
     1612        (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉))
     1613    [ @opt_safe_elim #lbv' #EQ_lbv'
     1614    |* -lbv #by3 #lbv #lbv_prf
     1615      @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe …
     1616        (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉))
     1617    [ @opt_safe_elim #lbv' #EQ_lbv'
     1618    |* -lbv #by4 * [2: #by5 #tl #lbv_prf @res_preserve_error ]
     1619      #lbv_prf @mfr_return %
     1620    ]]]]
     1621    cases lbv in EQ_lbv';
     1622    try (#H @res_preserve_error)
     1623    -lbv #by1 #lbv #H @('bind_inversion H) -H #by1' #EQby1'
     1624    #H @('bind_inversion H) -H #tl' #EQtl'
     1625    whd in ⊢ (??%?→?); #EQ destruct(EQ)
     1626    @(mfr_bind … (λby.λ_:True.by))
     1627    [1,3,5,7: #by #EQ %{I} >(Byte_of_val_inv … EQ) in EQby1';
     1628      whd in ⊢ (??%%→?); #EQ destruct(EQ) %
     1629    |*: #by1 * @mfr_return_eq
     1630      change with (m_list_map ????? = ?) in EQtl';
     1631      [1,3,5,7: %
     1632      |*: @opt_safe_elim #lbv''
     1633      ] >EQtl' #EQ destruct %
     1634    ]
     1635  | #_ @res_preserve_error
     1636  ]
     1637]
     1638#PRESERVE
     1639cases (PRESERVE … (proj2 … prf) … H) *
     1640#EQ >EQ % whd in ⊢ (??%?→?); #ABS destruct(ABS)
    15511641qed.
    15521642
     
    15651655#EQ >EQ //
    15661656qed.*)
    1567 
    1568 (* this should make things easier for ops using memory (where pc cant happen) *)
    1569 definition bv_no_pc : beval → Prop ≝
    1570 λbv.match bv with [ BVpc _ _ ⇒ False | _ ⇒ True ].
    1571 
    1572 lemma bv_pc_other :
    1573   ∀P : beval → Prop.
    1574   (∀pc,p.P (BVpc pc p)) →
    1575   (∀bv.bv_no_pc bv → P bv) →
    1576   ∀bv.P bv.
    1577 #P #H1 #H2 * /2/ qed.
    1578 
    1579 lemma sigma_bv_no_pc : ∀p,p',graph_prog,sigma,bv,prf.
    1580   bv_no_pc bv →
    1581   sigma_beval p p' graph_prog sigma bv prf = bv.
    1582 #p #p' #graph_prog #sigma *
    1583 [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ]
    1584 #prf * whd in match sigma_beval; normalize nodelta
    1585 @opt_safe_elim #bv' normalize #EQ destruct(EQ) %
    1586 qed.
    1587 
    1588 lemma bv_no_pc_wf : ∀p,p',graph_prog,sigma,bv.
    1589 bv_no_pc bv → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?.
    1590 #p #p' #graph_prog #sigma *
    1591 [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] *
    1592 % whd in ⊢ (??%?→?); #ABS destruct(ABS) qed.
    15931657
    15941658lemma is_push_sigma_commute :
     
    16241688qed.
    16251689
    1626 lemma byte_of_val_inv :
    1627   ∀e,bv,v.Byte_of_val e bv = return v → bv = BVByte v.
    1628 #e *
    1629 [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] #v
    1630 whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.
    1631 
    1632 lemma bit_of_val_inv :
     1690lemma Bit_of_val_inv :
    16331691  ∀e,bb,v.Bit_of_val e bb = return v → bb = BBbit v.
    16341692#e *
     
    16541712#v #EQ %{I}
    16551713>sigma_bv_no_pc try assumption
    1656 >(byte_of_val_inv … EQ) %
     1714>(Byte_of_val_inv … EQ) %
    16571715qed.
    16581716
     
    16681726[2: #by * @mfr_return % whd in ⊢ (??%%→?); #EQ destruct(EQ) ]
    16691727#v #EQ %{I} >sigma_bv_no_pc try assumption
    1670 >(byte_of_val_inv … EQ) %
     1728>(Byte_of_val_inv … EQ) %
    16711729qed.
    16721730
     
    19862044 qed.
    19872045
    1988 lemma eval_seq_no_call_no_goto :
     2046lemma eval_seq_no_call_no_goto_ok :
    19892047 ∀p,p',graph_prog.
    19902048 let lin_prog ≝ linearise p graph_prog in
     
    20192077[ whd whd in ⊢ (??%?); >EQfetch' normalize nodelta
    20202078  whd in match joint_classify_step; normalize nodelta
    2021   @no_call_other assumption
     2079  >no_call_other try % assumption
    20222080| whd whd in match eval_state; normalize nodelta >EQfetch' >m_return_bind
    20232081  whd in match eval_statement_no_pc; normalize nodelta
     
    20302088qed.
    20312089
    2032 lemma eval_seq_no_call_goto :
     2090lemma eval_seq_no_call_goto_ok :
    20332091 ∀p,p',graph_prog.
    20342092 let lin_prog ≝ linearise p graph_prog in
     
    20462104  (succ_pc (make_sem_graph_params p p') …
    20472105    (pc … st) nxt) in
    2048  (? : Prop) →
     2106 ∀prf'.
    20492107 fetch_statement (make_sem_lin_params p p') …
    20502108   (globalenv_noinit … lin_prog)
    20512109     (succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) =
    20522110   return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 →
     2111 pc_of_label (make_sem_lin_params p p') ?
     2112                (globalenv_noinit ? (linearise p … graph_prog))
     2113                (pc_block (pc … st))
     2114                nxt = return sigma_pc p p' graph_prog sigma
     2115    (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' →
    20532116 ∃prf''.
    20542117 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
     
    20572120 bool_to_Prop (taaf_non_empty … taf).
    20582121#p #p' #graph_prog #stack_sizes #sigma #gss #st #st' #f #fn #stmt #nxt #stmt_no_call
    2059 #prf #EQfetch' #EQeval #prf' #EQsucc_pc
     2122#prf #EQfetch' #EQeval #prf' #EQsucc_pc #EQ_pc_of_label
    20602123cases (eval_seq_no_pc_sigma_commute … gss … EQeval) [2: @(proj2 … prf)]
    20612124#prf'' #EQeval'
    20622125% [ @hide_prf % assumption ]
    2063 %{(taaf_step … (taa_base …) …)} [3: % ]
    2064 [ whd whd in ⊢ (??%?); >EQfetch' normalize nodelta
     2126%{(taaf_step … (taa_step … (taa_base …)) …)} [7: % ]
     2127[4: whd whd in ⊢ (??%?); >EQfetch' normalize nodelta
    20652128  whd in match joint_classify_step; normalize nodelta
    2066   @no_call_other assumption
    2067 | whd whd in match eval_state; normalize nodelta >EQfetch' >m_return_bind
     2129  >no_call_other try % assumption
     2130|3: whd whd in match eval_state; normalize nodelta >EQfetch' in ⊢ (??%?);
     2131  >m_return_bind in ⊢ (??%?);
    20682132  whd in match eval_statement_no_pc; normalize nodelta
    2069   >EQeval' >m_return_bind
     2133  >EQeval' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
    20702134  whd in match eval_statement_advance; normalize nodelta
    2071   >no_call_advance [2: assumption ]
    2072   whd in match (next ???);
    2073   >EQsucc_pc %
     2135  >no_call_advance in ⊢ (??%?); [2: assumption ]
     2136  whd in match (next ???) in ⊢ (??%?);
     2137  >EQsucc_pc in ⊢ (??%?); %
     2138|1: whd whd in ⊢ (??%?); >EQsucc_pc %
     2139|5: %* #H @H -H whd in ⊢ (??%?);  >EQsucc_pc %
     2140|2: whd whd in match eval_state; normalize nodelta
     2141  >EQsucc_pc >m_return_bind >m_return_bind whd in match eval_statement_advance;
     2142  normalize nodelta whd in match goto; normalize nodelta
     2143  whd in match (pc_block ?); >pc_block_sigma_commute
     2144  >EQ_pc_of_label %
     2145|*:
    20742146]
    20752147qed.
    20762148
    2077 
    2078  
    2079 
    2080   [ assumption
    2081   | assu
    2082  
     2149lemma eval_call_ok :
     2150 ∀p,p',graph_prog.
     2151 let lin_prog ≝ linearise p graph_prog in
     2152 ∀stack_sizes.
     2153 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
     2154 ∀st,st',f,fn,called,args,dest,nxt.
     2155 ∀prf : well_formed_state_pc … gss st.
    20832156  fetch_statement (make_sem_lin_params p p') …
    2084           (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
    2085               return 〈f, \fst (linearise_int_fun … fn),
    2086                       sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧
    2087           ∃prf'.
    2088             let nxt_pc ≝  in
    2089             let sigma_nxt ≝  in
    2090             (nxt_pc = sigma_nxt ∨ fetch_statement (make_sem_lin_params p p') …
    2091              (globalenv_noinit … lin_prog) nxt_pc =
    2092              return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉)
     2157    (globalenv_noinit ? lin_prog) (pc … (sigma_state_pc … st prf)) =
     2158      return 〈f, \fst (linearise_int_fun … fn),
     2159        sequential … (CALL (mk_lin_params p) … called args dest ) it〉 →
     2160   eval_seq_advance ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes))
     2161      (CALL … called args dest) nxt st = return st' →
     2162(* let st_pc' ≝ mk_state_pc ? st'
     2163  (succ_pc (make_sem_graph_params p p') …
     2164    (pc … st) nxt) in
     2165 ∀prf'.
     2166 fetch_statement (make_sem_lin_params p p') …
     2167   (globalenv_noinit … lin_prog)
     2168     (succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) =
     2169   return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 →
     2170 pc_of_label (make_sem_lin_params p p') ?
     2171                (globalenv_noinit ? (linearise p … graph_prog))
     2172                (pc_block (pc … st))
     2173                nxt = return sigma_pc p p' graph_prog sigma
     2174    (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' →*)
     2175  let st2_pre_call ≝ sigma_state_pc … gss st prf in
     2176  ∃is_call, is_call'.
     2177  ∃prf'.
     2178  let st2_after_call ≝ sigma_state_pc … gss st' prf' in
     2179  joint_call_ident (lin_prog_params … (linearise … graph_prog) stack_sizes) «st2_pre_call, is_call'» =
     2180  joint_call_ident (graph_prog_params … graph_prog stack_sizes) «st, is_call» ∧
     2181  eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes))
     2182    st2_pre_call = return st2_after_call.
     2183cases daemon
     2184qed.
     2185
     2186lemma eval_goto_ok :
     2187lemma eval_tailcall_ok :
     2188lemma eval_cond_cond_ok :
     2189lemma eval_cond_fcond_ok :
     2190lemma eval_return_ok :
     2191
    20932192
    20942193inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
Note: See TracChangeset for help on using the changeset viewer.