Changeset 3145 for src/common


Ignore:
Timestamp:
Apr 15, 2013, 4:31:50 PM (7 years ago)
Author:
tranquil
Message:
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
Location:
src/common
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r3096 r3145  
    1414
    1515include "common/StructuredTraces.ma".
     16include "common/FlatTraces.ma".
    1617
    1718(* We work with two relations on states in parallel, as well as two derived ones.
     
    149150    ]
    150151; sim_final :
    151   ∀st1,st2,res.as_result S1 st1 = Some ? res → sim_status_rel st1 st2 →
    152   as_result S2 st2 = Some ? res
     152  ∀st1,st2.as_result S1 st1 = as_result S2 st2
    153153}.
    154154
     
    160160; sim_step_final :> status_simulation S1 S2 R
    161161}.
    162 
    163 (* some useful lemmas *)
    164 
    165 let rec taa_append_tal_rel S1 fl1 st1 st1'
    166   (tal1 : trace_any_label S1 fl1 st1 st1')
    167   S2 st2 st2mid fl2 st2'
    168   (taa2 : trace_any_any S2 st2 st2mid)
    169   (tal2 : trace_any_label S2 fl2 st2mid st2')
    170   on tal1 :
    171   tal_rel … tal1 tal2 →
    172   tal_rel … tal1 (taa2 @ tal2) ≝
    173 match tal1 return λfl1,st1,st1',tal1.? with
    174   [ tal_base_not_return st1 st1' _ _ _ ⇒ ?
    175   | tal_base_return st1 st1' _ _ ⇒ ?
    176   | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ ?
    177   | tal_base_tailcall st1 st1' st1'' _ prf tlr1 ⇒ ?
    178   | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ ?
    179   | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ ?
    180   ].
    181 [ * #EQfl *#st2mid *#taa2' *#H2 *#G2 *#K2 #EQ
    182 | * #EQfl *#st2mid *#taa2' *#H2 *#G2 #EQ
    183 | * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
    184   [ *#K2 *#tlr2 *#L2 * #EQ #EQ'
    185   | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #coll
    186   ]
    187 | * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *#tlr2 * #EQ #EQ'
    188 | * #st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
    189   [ * #EQfl *#K2 *#tlr2 *#L2 ** #EQ #coll #EQ'
    190   | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #EQ''
    191   ]
    192 | whd in ⊢ (%→%); @(taa_append_tal_rel … tl1)
    193 ]
    194 destruct
    195 <associative_taa_append_tal
    196   [1,2,3,4,5:%{(refl …)}] %{st2mid}
    197   [1,2:|*: %{G2} %{EQcall} ]
    198   %{(taa_append_taa … taa2 taa2')}
    199   [1,2: %{H2} %{G2} [%{K2}] %
    200   |5: %{st2mid'} %{H2} %{tlr2} % //
    201   |*: %{st2mid'} %{H2}
    202     [1,3: %1 [|%{(refl …)}] |*: %2 %{st2mid''} ]
    203     %{K2} %{tlr2} %{L2} [3,4: %{tl2} ] /3 by conj/
    204   ]
    205 qed.
    206162
    207163(*
     
    222178*)
    223179
    224 lemma taa_end_not_costed : ∀S,s1,s2.∀taa : trace_any_any S s1 s2.
    225   if taa_non_empty … taa then ¬as_costed … s2 else True.
    226 #S #s1 #s2 #taa elim taa -s1 -s2 normalize nodelta
    227 [ #s1 %
    228 | #s1 #s2 #s3 #H #G #K #tl lapply K lapply H cases tl -s2 -s3
    229   [ #s2 #H #K #_ assumption
    230   | #s2 #s3 #s4 #H' #G' #K' #tl' #H #K #I @I
    231   ]
    232 ]
    233 qed.
    234 
    235 let rec tal_collapsable_to_rel S fl st1 st2
    236   (tal : trace_any_label S fl st1 st2) on tal :
    237   tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
    238   tal_rel … tal (tal_base_not_return S2 st12 st22 H I J) ≝
    239   match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
    240   tal_rel … tal (tal_base_not_return S2 st12 st22 H I J)
    241   with
    242   [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_to_rel ???? tl
    243   | tal_base_not_return _ st2' _ _ K ⇒ ?
    244   | _ ⇒ Ⓧ
    245   ].
    246 * #S2 #st12 #st22 #H #I #J % %[|%{(taa_base ??)} %[|%[|%[| %
    247 qed.
    248 
    249 let rec tal_collapsable_eq_flag S fl st1 st2
    250   (tal : trace_any_label S fl st1 st2) on tal :
    251   tal_collapsable ???? tal → fl = doesnt_end_with_ret ≝
    252   match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → fl = ?
    253   with
    254   [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_eq_flag ???? tl
    255   | tal_base_not_return _ st2' _ _ K ⇒ λ_.refl …
    256   | _ ⇒ Ⓧ
    257   ].
    258 
    259 let rec tal_collapsable_split S fl st1 st2
    260   (tal : trace_any_label S fl st1 st2) on tal :
    261   tal_collapsable ???? tal → ∃st2_mid.∃taa : trace_any_any S st1 st2_mid.∃H,I,J.
    262   tal ≃ taa @ tal_base_not_return … st2 H I J ≝
    263   match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∃st2_mid,taa,H,I,J.
    264   tal ≃ taa @ tal_base_not_return … st2_mid ? H I J
    265   with
    266   [ tal_step_default fl' st1' st2' st3' H tl I J ⇒ ?
    267   | tal_base_not_return st1' st2' H I J ⇒ ?
    268   | _ ⇒ Ⓧ
    269   ].
    270 [ * %{st1'} %{(taa_base …)} %{H} %{I} %{J} %
    271 | #coll
    272   elim (tal_collapsable_split … tl coll) #st2_mid * #taa * #H' * #I' *#J'
    273   #EQ %{st2_mid} %{(taa_step … taa)} try assumption
    274   %{H'} %{I'} %{J'} lapply EQ lapply tl >(tal_collapsable_eq_flag … coll) -tl #tl
    275   #EQ >EQ %
    276 ]
    277 qed.
    278 
    279 lemma tal_collapsable_to_rel_symm : ∀S,fl,st1,st2,tal.
    280 tal_collapsable S fl st1 st2 tal → ∀S2,st12,st22,H,I,J.
    281   tal_rel … (tal_base_not_return S2 st12 st22 H I J) tal.
    282 #S #fl #st1 #st2 #tal #coll #S2 #st12 #st22 #H #I #J
    283 elim (tal_collapsable_split … coll) lapply tal
    284  >(tal_collapsable_eq_flag … coll) -tal #tal
    285 #st2_mid * #taa *#H' *#I' *#J' #EQ >EQ % [%]
    286 %[|%[|%[|%[|%[| % ]]]]]
    287 qed.
    288 
    289 lemma taaf_append_tal_rel : ∀S1,fl1,st1,st1',S2,fl2,st2_pre,st2,st2',tal1,taaf2,H,tal2.
    290   tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2' tal1 tal2 →
    291   tal_rel … tal1 (taaf_append_tal S2 st2_pre … taaf2 H tal2).
    292 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 * -H7 -H8 normalize
    293 [ // |3: #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 generalize in match (? : False); * ]
    294 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24
    295 change with (taa_step ???? ??? (taa_base ??) @ H23) in match (tal_step_default ?????????);
    296 /2 by taa_append_tal_rel/
    297 qed.
    298180
    299181(* little helpers *)
     
    306188
    307189let rec status_simulation_produce_tlr S1 S2 R
     190(* NB: the axiomatized part about unrepeatingness is imprecise, as further
     191  hypotheses are surely needed for the taa prefix. Left for when it is
     192  rendered more precise. *)
    308193(* we start from this situation
    309194     st1 →→→→tlr→→→→ st1'
     
    325210  (taa2_pre : trace_any_any S2 st2_lab st2)
    326211  (sim_execute : status_simulation S1 S2 R)
    327   on tlr1 : R st1 st2 → label_rel … st1 st2_lab →
     212  on tlr1 : tlr_unrepeating … tlr1 → R st1 st2 → label_rel … st1 st2_lab →
    328213  ∃st2_mid.∃st2'.
    329214  ∃tlr2 : trace_label_return S2 st2_lab st2_mid.
     
    331216  (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
    332217  R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
    333   tlr_rel … tlr1 tlr2
     218  tlr_rel … tlr1 tlr2 ∧ tlr_unrepeating … tlr2
    334219 match tlr1 with
    335220 [ tlr_base st1 st1' tll1 ⇒ ?
     
    356241  (taa2_pre : trace_any_any S2 st2_lab st2)
    357242  (sim_execute : status_simulation S1 S2 R)
    358    on tll1 : R st1 st2 → label_rel … st1 st2_lab →
     243   on tll1 : tll_unrepeating … tll1 → R st1 st2 → label_rel … st1 st2_lab →
    359244    match fl with
    360245    [ ends_with_ret ⇒
     
    364249      (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
    365250      R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
    366       tll_rel … tll1 tll2
     251      tll_rel … tll1 tll2 ∧ tll_unrepeating … tll2
    367252    | doesnt_end_with_ret ⇒
    368253      ∃st2'.∃tll2 : trace_label_label S2 doesnt_end_with_ret st2_lab st2'.
    369       R st1' st2' ∧ label_rel … st1' st2' ∧ tll_rel … tll1 tll2
     254      R st1' st2' ∧ label_rel … st1' st2' ∧ tll_rel … tll1 tll2 ∧
     255      tll_unrepeating … tll2
    370256    ] ≝
    371257  match tll1 with
     
    401287  (tal1 : trace_any_label S1 fl st1 st1')
    402288  (sim_execute : status_simulation S1 S2 R)
    403    on tal1 : R st1 st2 →
     289   on tal1 : tal_unrepeating … tal1 → R st1 st2 →
    404290    match fl with
    405291    [ ends_with_ret ⇒
     
    409295      (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
    410296      R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
    411       tal_rel … tal1 tal2
     297      tal_rel … tal1 tal2 ∧ tal_unrepeating … tal2
    412298    | doesnt_end_with_ret ⇒
    413299      (∃st2'.∃tal2 : trace_any_label S2 doesnt_end_with_ret st2 st2'.
    414        R st1' st2' ∧ label_rel … st1' st2' ∧ tal_rel … tal1 tal2) ∨
     300       R st1' st2' ∧ label_rel … st1' st2' ∧ tal_rel … tal1 tal2 ∧
     301       tal_unrepeating … tal2) ∨
    415302      (* empty *)
    416303      (R st1' st2 ∧ label_rel … st1' st2 ∧ tal_collapsable … tal1 ∧ ¬as_costed … st1)
     
    424311  | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ?
    425312  ].
    426 #st1_R_st2
    427 [1,2,3: #st1_L_st2_lab ]
     313#unrpt #st1_R_st2
     314[1,2,3: #st1_L_st2_lab]
    428315[ (* tlr_base *)
    429   elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
     316  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute unrpt st1_R_st2 st1_L_st2_lab)
    430317  #st2_mid * #st2' * #tll2 #H
    431318  %{st2_mid} %{st2'} %{(tlr_base … tll2)} @H
    432319| (* tlr_step *)
    433   elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
    434   #st2_mid * #tll2 ** #H1 #H2 #H3
    435   elim (status_simulation_produce_tlr … tl1 (taa_base …) sim_execute H1 H2)
    436   #st2_mid' * #st2' * #tl2 * #taa2 * #H4 #H5
     320  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute (proj1 … unrpt) st1_R_st2 st1_L_st2_lab)
     321  #st2_mid * #tll2 *** #H1 #H2 #H3 #H4
     322  elim (status_simulation_produce_tlr … tl1 (taa_base …) sim_execute (proj2 … unrpt) H1 H2)
     323  #st2_mid' * #st2' * #tl2 * #taa2 ** #H5 #H6 #H7
    437324  %{st2_mid'} %{st2'} %{(tlr_step … tll2 tl2)} %{taa2}
    438   %{H4} %{H3 H5}
     325  % [ %{H5} %{H3 H6} | %{H4 H7} ]
    439326| (* tll_base *)
    440   lapply (status_simulation_produce_tal … st2 tal1 sim_execute st1_R_st2)
     327  lapply (status_simulation_produce_tal … st2 tal1 sim_execute unrpt st1_R_st2)
    441328  cases fl1' in tal1; normalize nodelta #tal1 *
    442329  [3: * #_ #ABS elim (absurd … H ABS) ]
    443   [ #st2_mid ] * #st2' * #tal2 [* #taa2 ] * #H1 #H2
     330  [ #st2_mid ] * #st2' * #tal2 [* #taa2 ] ** #H1 #H2 #unrpt'
    444331  [%{st2_mid}] %{st2'} %{(tll_base … (taa_append_tal … taa2_pre tal2) ?)}
    445332  [1,3: whd <st1_L_st2_lab assumption
    446   |*: [%{taa2} ] %{H1} %
    447     [1,3: change with (opt_safe ??? = opt_safe ???)
    448       @opt_safe_elim #a #EQ1
    449       @opt_safe_elim #b <st1_L_st2_lab >EQ1 #EQ2  destruct %
    450     |*: @taa_append_tal_rel assumption
    451     ]
     333  |*: [%{taa2} ] %
     334    [1,3: %{H1} %
     335      [1,3: change with (opt_safe ??? = opt_safe ???)
     336        @opt_safe_elim #a #EQ1
     337        @opt_safe_elim #b <st1_L_st2_lab >EQ1 #EQ2  destruct %
     338      |*: @taa_append_tal_rel assumption
     339      ]
     340    |*: whd (* unrepeatingness... *) cases daemon
     341    ]
    452342  ]
    453343| (* tal_base_non_return *) whd
     
    467357    %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 ??))}
    468358    [1,4: %1{I2} |7,10: %2{I2} |2,5: assumption |8,11: whd <st1_L_st2' assumption ]
    469     % /2 by conj/
    470     % try @refl %{st2_mid} %{taa2} %{H2} %[2,4,6,8: %[2,4,6,8: %]]
     359    %
     360    [1,3,5,7:
     361      % /2 by conj/
     362      % try @refl %{st2_mid} %{taa2} %{H2} %[2,4,6,8: %[2,4,6,8: %]]
     363    |*: (* unrepeatingness... *) cases daemon
     364    ]
    471365  ]
    472366| (* tal_base_return *) whd
     
    477371  #st1_Rret_st2' #st1_Rret_st2' #st1_L_st2'
    478372  %[2,4:%[2,4: %{(taa_append_tal … taa2 (tal_base_return … K2 J2))} %{taa2'}
    479   % [ /4 by conj/ ]
    480   %[ % | %[|%[|%[|%[| % ]]]]]]]
     373  %
     374  [ % [ /4 by conj/ ]
     375    %[ % | %[|%[|%[|%[| % ]]]]]
     376  |*: (* unrepeatingness... *) cases daemon
     377  ]]]
    481378| (* tal_base_call *) whd
    482379  lapply (sim_execute … H st1_R_st2)
     
    485382  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
    486383  #st1_R_st2_mid #st1_L_st2_after_call
    487   elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
     384  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute unrpt st1_R_st2_mid st1_L_st2_after_call)
    488385  #st2_after_ret * #st2' * #tlr2 * #taa2'' lapply tlr2 cases taa2'' -st2_after_ret -st2'
    489   [ #st2' #tlr2 *****
     386  [ #st2' #tlr2 ******
    490387  |*: #st2_after_ret #st2_after_ret' #st2' #taa2''
    491     #I2 #J2 [2: #K2 ] #tlr2 **** #ncost
    492   ]
    493   #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S %1
     388    #I2 #J2 [2: #K2 ] #tlr2 ***** #ncost
     389  ]
     390  #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S #unrpt' %1
    494391  %{st2'}
    495392  [ %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)}
    496     [3: % [ % assumption ]
    497       % [%] %[|%[| %{EQcall} %[|%[|%[| %1 %[|%[|%[| %{S} % ]]]]]]]]
     393    [3: %
     394      [ % [ % assumption ]
     395        % [%] %[|%[| %{EQcall} %[|%[|%[| %1 %[|%[|%[| %{S} % ]]]]]]]]
     396      |  (* unrepeatingness... *) cases daemon
     397      ]
    498398    ]
    499399  |*: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (taa2'' @ tal_base_not_return … I2 ??))}
    500400    [2: %1{J2} |6: %2{J2}
    501     |4,8: % try (% assumption)
    502       % [1,3:%] %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4:
    503         % [1,3: %{S} % ] /2 by taa_append_collapsable, I/
    504       ]]]]]]]]]]
     401    |4,8: %
     402      [1,3: % try (% assumption)
     403        % [1,3:%] %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4:
     404          % [1,3: %{S} % ] /2 by taa_append_collapsable, I/
     405        ]]]]]]]]]]
     406      |*: (* unrepeatingness... *) cases daemon
     407      ]
    505408    ]
    506409  ]
     
    514417  * #st2_pre_call #G2 * #EQcall * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
    515418  #st1_R_st2_mid #st1_L_st2_after_call
    516   elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
     419  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute unrpt st1_R_st2_mid st1_L_st2_after_call)
    517420  #st2_after_ret * #st2' * #tlr2 * #taa2''
    518   * #props #S
     421  ** #props #S #unrpt'
    519422  %{st2_after_ret} %{st2'}
    520423  %{(taa2 @ tal_base_tailcall ???? H2 G2 tlr2)}
    521424  %{taa2''}
    522   %{props}
    523   % [%] %[|%[| %{EQcall} %[|%[|%[|%[| %{S} % ]]]]]]
     425  %
     426  [ %{props}
     427    % [%] %[|%[| %{EQcall} %[|%[|%[|%[| %{S} % ]]]]]]
     428  | (* unrepeatingness... *) cases daemon
     429  ]
    524430| (* tal_step_call *)
    525431  lapply (sim_execute … H st1_R_st2)
     
    528434  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
    529435  #st1_R_st2_mid #st1_L_st2_after_call
    530   elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
     436  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute (proj2 … unrpt) st1_R_st2_mid st1_L_st2_after_call)
    531437  #st2_after_ret * #st2' * #tlr2 * #taa2''
    532   ****
    533   #taa_ncost #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S
    534   lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2')
     438  *****
     439  #taa_ncost #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S #unrpt'
     440  lapply (status_simulation_produce_tal … tl1 sim_execute (proj2 … (proj1 … unrpt)) st1_R_st2')
    535441  cases fl1' in tl1; #tl1 *
    536   [ #st2'' * #st2''' * #tl2 * #taa2''' **** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S'
     442  [ #st2'' * #st2''' * #tl2 * #taa2''' ***** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S' #unrpt''
    537443    %[|%[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
    538     [4: %{taa2'''} % [ /4 by conj/ ]
    539       %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
     444    [4: %{taa2'''} %
     445      [ % [ /4 by conj/ ]
     446        %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
     447      | (* unrepeatingness... *) cases daemon
     448      ]
    540449    ]]]
    541   | *#st2'' *#tl2 ** #st1_R_st2'' #st1_L_st2'' #S' %1
     450  | *#st2'' *#tl2 *** #st1_R_st2'' #st1_L_st2'' #S' #unrpt'' %1
    542451    %[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
    543     [4: % [ /2 by conj/ ]
    544       %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
     452    [4: %
     453      [ % [ /2 by conj/ ]
     454        %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
     455      | (* unrepeatingness... *) cases daemon
     456      ]
    545457    ]]
    546458  | lapply S lapply tlr2 lapply st1_Rret_st2' lapply st1_L_st2' lapply st1_R_st2'
     
    549461      *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost %1
    550462      %[| %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)}
    551       [3: % [ /2 by conj/ ]
    552       %[|%[| %{EQcall} %[|%[|%[| %1 %{(refl …)} %[|%[|%[| %{S} %{tl1_coll} % ]]]]]]]]]]
     463      [3: %
     464        [ % [ /2 by conj/ ]
     465          %[|%[| %{EQcall} %[|%[|%[| %1 %{(refl …)} %[|%[|%[| %{S} %{tl1_coll} % ]]]]]]]]
     466        | (* unrepeatingness... *) cases daemon
     467      ]]]
    553468    |*: #st2_after_ret #st2_after_ret' #st2' #hd #I2' #J2' [2: #K2'] #ncost
    554469      #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
     
    556471      %[2,4: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (hd @ tal_base_not_return ??? I2' ??))}
    557472      [2: %1{J2'} |6: %2{J2'}
    558       |4,8: % [1,3: /2 by conj/]
    559         %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4:
    560           %{S} % [1,3:%] @taa_append_tal_rel /2 by tal_collapsable_to_rel/
    561         ]]]]]]]]]]
     473      |4,8: %
     474        [ % [1,3: /2 by conj/]
     475          %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4:
     476            %{S} % [1,3:%] @taa_append_tal_rel /2 by tal_collapsable_to_rel/
     477          ]]]]]]]]]]
     478        |*: (* unrepeatingness... *) cases daemon
     479        ]
    562480      ]]
    563481    ]
     
    575493  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
    576494  #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid
    577   lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid)
     495  lapply (status_simulation_produce_tal … tl1 sim_execute (proj2 … unrpt) st1_R_st2_mid)
    578496  cases fl1' in tl1; #tl1 *
    579   [ #st2_mid' *#st2' *#tal2 *#taa2' * #H #G
     497  [ #st2_mid' *#st2' *#tal2 *#taa2' ** #H #G #unrpt'
    580498    %[|%[| %{(taaf_append_tal … taa2 ? tal2)}
    581       [2: %{taa2'} % [/4 by conj/ ] @taaf_append_tal_rel @G ]
     499      [2: %{taa2'} %
     500        [ % [/4 by conj/ ] @taaf_append_tal_rel @G
     501        |  (* unrepeatingness... *) cases daemon
     502        ]
     503      ]
    582504    ]]
    583   | *#st2' *#tal2 *#H #G %1
     505  | *#st2' *#tal2 ** #H #G #unrpt' %1
    584506    %[| %{(taaf_append_tal … taa2 ? tal2)}
    585       [2: % [/2 by conj/] @taaf_append_tal_rel @G ]
     507      [2: %
     508        [ % [/2 by conj/] @taaf_append_tal_rel @G
     509        | (* unrepeatingness... *) cases daemon
     510        ]
     511      ]
    586512    ]
    587513  | (* can't happen *)
     
    592518]
    593519qed.
    594 
    595 definition is_cl_jump : ∀S : abstract_status.S → bool ≝
    596 λS,s.match as_classify … s with [ cl_jump ⇒ true | _ ⇒ false ].
    597 
    598 definition enforce_costedness : ∀S : abstract_status.S → S → Prop ≝
    599 λS,s1,s2.if is_cl_jump … s1 then as_costed … s2 else True.
    600 
    601 (* finite flat traces, with recursive structure right to left. The list of
    602    identifiers represents the call stack *)
    603 inductive flat_trace (S : abstract_status) (start : S) : S → Type[0] ≝
    604 | ft_start : flat_trace S start start
    605 | ft_advance :
    606   ∀st1,st2.flat_trace S start st1 → as_execute S st1 st2 →
    607   enforce_costedness … st1 st2 → flat_trace S start st2.
    608 
    609 (*
    610   ((as_classifier ? st1 cl_jump ∧ as_costed … st2) ∨ as_classifier ? st1 cl_other) →
    611   flat_trace S start st2 stack
    612 | ft_advance_call :
    613   ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 →
    614   ∀prf : as_classifier ? st1 cl_call.
    615   flat_trace S start st2 (as_call_ident ? «st1, prf» :: stack)
    616 | ft_advance_tailcall :
    617   ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
    618   ∀prf : as_classifier ? st1 cl_tailcall.
    619   flat_trace S start st2 (as_tailcall_ident ? «st1, prf» :: stack)
    620 | ft_advance_ret :
    621   ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
    622   as_classifier ? st1 cl_return →
    623   flat_trace S start st2 stack.
    624 *)
    625 
    626 let rec ft_extend_taa S st1 st2 st3 (ft : flat_trace S st1 st2)
    627   (taa : trace_any_any S st2 st3)
    628 on taa : flat_trace S st1 st3 ≝
    629 match taa return λst2,st3,taa.flat_trace ?? st2 → flat_trace ?? st3 with
    630 [ taa_base s ⇒ λacc.acc
    631 | taa_step st1 st2 st3 H G _ tl ⇒
    632   λacc.ft_extend_taa ???? (ft_advance ???? acc H ?) tl
    633 ] ft.
    634 @hide_prf whd whd in match is_cl_jump; normalize nodelta >G % qed.
    635 
    636 lemma ft_extend_extend_taa : ∀S,st1,st2,st3,st4,ft,taa1,taa2.
    637   ft_extend_taa S st1 st3 st4 (ft_extend_taa … st2 … ft taa1) taa2 =
    638   ft_extend_taa … ft (taa_append_taa … taa1 taa2).
    639 #S #st1 #st2 #st3 #st4 #ft #taa1 lapply ft elim taa1 -st2 -st3 normalize
    640 /2/
    641 qed.
    642 
    643 definition ft_extend_taaf ≝ λS,st1,st2,st3.λft : flat_trace S st1 st2.
    644   λtaaf : trace_any_any_free S st2 st3.
    645   match taaf return λst2,st3,taaf.flat_trace ?? st2 → flat_trace ?? st3 with
    646   [ taaf_base s ⇒ λft.ft
    647   | taaf_step s1 s2 s3 pre H G ⇒
    648     λft.ft_advance … (ft_extend_taa … ft pre) H ?
    649   | taaf_step_jump s1 s2 s3 pre H G K ⇒
    650     λft.ft_advance … (ft_extend_taa … ft pre) H ?
    651   ] ft.
    652 @hide_prf whd whd in match is_cl_jump; normalize nodelta >G // qed.
    653 
    654 definition option_to_list : ∀A.option A → list A ≝ λA,x.
    655   match x with
    656   [ Some x ⇒ [x]
    657   | None ⇒ [ ]
    658   ].
    659 
    660 (*
    661 let rec ft_stack S st st' (ft : flat_trace S st st') on ft : list ident ≝
    662 match ft with
    663 [ ft_start ⇒ [ ]
    664 | ft_advance st1_mid st1' pre1 _ _ ⇒
    665   match as_classify … st1_mid return λx.as_classifier … st1_mid x → ? with
    666   [ cl_call ⇒ λprf.
    667     let id ≝ as_call_ident ? «st1_mid, prf» in
    668     id :: ft_stack … pre1
    669   | cl_tailcall ⇒ λprf.
    670     let id ≝ as_tailcall_ident ? «st1_mid, prf» in
    671     match ft_stack … pre1 with
    672     [ nil ⇒ (* should never happen in correct programs *)
    673       [id]
    674     | cons _ stack' ⇒
    675       id :: stack'
    676     ]
    677   | cl_return ⇒ λ_.
    678     match ft_stack … pre1 with
    679     [ nil ⇒ (* should never happen in correct programs *)
    680       [ ]
    681     | cons _ stack' ⇒ stack'
    682     ]
    683   | _ ⇒ λ_.ft_stack … pre1
    684   ] (refl …)
    685 ].
    686 *)
    687 
    688 (* the observables of a flat trace (for the moment, only labels, calls and returns) *)
    689 (* inefficient, but used only in correctness proofs *)
    690 let rec ft_stack_observables S st st'
    691   (ft : flat_trace S st st') on ft : list ident × (list intensional_event) ≝
    692 match ft with
    693 [ ft_start ⇒ 〈[ ], [ ]〉
    694 | ft_advance st1_mid st1' pre1 _ _ ⇒
    695   let 〈stack, tr〉 ≝ ft_stack_observables … pre1 in
    696   let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
    697   match as_classify … st1_mid return λx.as_classifier … st1_mid x → ? with
    698   [ cl_call ⇒ λprf.
    699     let id ≝ as_call_ident ? «st1_mid, prf» in
    700     let tr' ≝ tr @ add @ [IEVcall id] in
    701     〈id :: stack, tr'〉
    702   | cl_tailcall ⇒ λprf.
    703     let id ≝ as_tailcall_ident ? «st1_mid, prf» in
    704     match stack with
    705     [ nil ⇒ (* should never happen in correct programs *)
    706       〈[ ], tr @ add〉
    707     | cons f stack' ⇒
    708       let tr' ≝ tr @ add @ [IEVtailcall f id] in
    709       〈id :: stack', tr'〉
    710     ]
    711   | cl_return ⇒ λ_.
    712     match stack with
    713     [ nil ⇒ (* should never happen in correct programs *)
    714       〈[ ], tr @ add〉
    715     | cons f stack' ⇒
    716       let tr' ≝ tr @ add @ [IEVret f] in
    717       〈stack', tr'〉
    718     ]
    719   | _ ⇒ λ_.〈stack, tr @ add〉
    720   ] (refl …)
    721 ].
    722 
    723 definition ft_observables ≝ λS,st1,st2,ft.\snd (ft_stack_observables S st1 st2 ft).
    724 definition ft_stack ≝ λS,st1,st2,ft.\fst (ft_stack_observables S st1 st2 ft).
    725 
    726 definition ft_current_function : ∀S,st1,st2.flat_trace S st1 st2 → option ident ≝
    727 λS,st1,st2,ft.
    728 match ft_stack … ft with [ nil ⇒ None ? | cons hd _ ⇒ Some ? hd ].
    729 
    730 lemma status_class_dep_match_elim :
    731 ∀A : Type[0].∀P : A → Prop.
    732 ∀cl,c_call,c_return,c_tailcall,c_other,c_jump.
    733 (∀prf : cl = cl_call.P (c_call prf)) →
    734 (∀prf : cl = cl_return.P (c_return prf)) →
    735 (∀prf : cl = cl_tailcall.P (c_tailcall prf)) →
    736 (∀prf : cl = cl_other.P (c_other prf)) →
    737 (∀prf : cl = cl_jump.P (c_jump prf)) →
    738 P (match cl return λx.cl = x → ? with
    739    [ cl_call ⇒ c_call
    740    | cl_return ⇒ c_return
    741    | cl_tailcall ⇒ c_tailcall
    742    | cl_other ⇒ c_other
    743    | cl_jump ⇒ c_jump
    744    ] (refl …)).
    745 #A #P * normalize // qed.
    746 
    747 lemma status_class_dep_match_rewrite :
    748 ∀A : Type[0].
    749 ∀cl,c_call,c_return,c_tailcall,c_other,c_jump.
    750 ∀cl'.
    751 ∀prf : cl = cl'.
    752 match cl return λx.cl = x → A with
    753  [ cl_call ⇒ c_call
    754  | cl_return ⇒ c_return
    755  | cl_tailcall ⇒ c_tailcall
    756  | cl_other ⇒ c_other
    757  | cl_jump ⇒ c_jump
    758  ] (refl …) =
    759 match cl' return λx.cl = x → A with
    760  [ cl_call ⇒ c_call
    761  | cl_return ⇒ c_return
    762  | cl_tailcall ⇒ c_tailcall
    763  | cl_other ⇒ c_other
    764  | cl_jump ⇒ c_jump
    765  ] prf.
    766 #A * #c1 #c2 #c3 #c4 #c5 * #prf destruct % qed.
    767 
    768 lemma pair_elim' :
    769   ∀A,B,C : Type[0].∀T : A → B → C.∀t : A × B.
    770   ∀P : (A×B) → C → Prop.
    771   P 〈\fst t, \snd t〉 (T (\fst t) (\snd t)) →
    772   P t (let 〈a, b〉 ≝ t in T a b).
    773 #A #B #C #T * // qed.
    774 
    775 lemma ft_extend_taa_obs : ∀S,st1,st2,st3,ft,taa.
    776   ft_stack_observables … (ft_extend_taa S st1 st2 st3 ft taa) =
    777     〈ft_stack … ft, ft_observables … ft @
    778     if taa then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ]〉.
    779 #S #st1 #st2 #st3 #ft #taa lapply ft elim taa -st2 -st3
    780 [ #st2 #ft >append_nil @eq_pair_fst_snd ]
    781 #st2 #st3 #st4 #H #K #G #taa #IH #ft
    782 whd in ⊢ (??(????%)?); >IH normalize nodelta
    783 -IH lapply G lapply H cases taa -st3 -st4 normalize nodelta
    784 [ #st3 #H #G
    785 | #st3 #st4 #st5 #ex #H' #G' #taa #H #G
    786   >(not_costed_no_label … G)
    787 ]
    788 >append_nil whd in ⊢ (??(???%%)(????(??%?)));
    789 whd in match (ft_stack_observables ????) ;
    790 @(pair_elim' … (ft_stack_observables … ft))
    791 >(status_class_dep_match_rewrite … K) %
    792 qed.
    793 
    794 lemma ft_extend_taa_advance_obs : ∀S,st1,st2,st3,st4.
    795   ∀ft : flat_trace S st1 st2.
    796   ∀taa : trace_any_any S st2 st3.
    797   ∀H : as_execute S st3 st4.∀G.
    798   ft_stack_observables … (ft_advance … (ft_extend_taa … ft taa) H G) =
    799   (let add ≝ option_to_list … (! l ← as_label … st2 ; return IEVcost l) in
    800    let 〈stack, tr〉 ≝ ft_stack_observables … ft in
    801    match as_classify … st3 return λx.as_classifier … st3 x → ? with
    802     [ cl_call ⇒ λprf.
    803       let id ≝ as_call_ident ? «st3, prf» in
    804       let tr' ≝ tr @ add @ [IEVcall id] in
    805       〈id :: ft_stack … ft, tr'〉
    806     | cl_tailcall ⇒ λprf.
    807       let id ≝ as_tailcall_ident ? «st3, prf» in
    808       match stack with
    809       [ nil ⇒ (* should never happen in correct programs *)
    810         〈[ ], tr @ add〉
    811       | cons f stack' ⇒
    812         let tr' ≝ tr @ add @ [IEVtailcall f id] in
    813         〈id :: stack', tr'〉
    814       ]
    815     | cl_return ⇒ λ_.
    816       match stack with
    817       [ nil ⇒ (* should never happen in correct programs *)
    818         〈[ ], tr @ add〉
    819       | cons f stack' ⇒
    820         let tr' ≝ tr @ add @ [IEVret f] in
    821         〈stack', tr'〉
    822       ]
    823     | _ ⇒ λ_.〈stack, tr @ add〉
    824     ] (refl …)).
    825 #S #st1 #st2 #st3 #st4 #ft #taa #H #G normalize nodelta
    826 whd in ⊢ (??%?); @pair_elim' @pair_elim' normalize nodelta
    827 @status_class_dep_match_elim #prf
    828 @status_class_dep_match_elim #prf'
    829 try(@⊥ >prf in prf'; #prf' -prf destruct @False)
    830 >ft_extend_taa_obs whd in match ft_stack; whd in match ft_observables; normalize nodelta
    831 [2,3: cases (\fst (ft_stack_observables … ft)) normalize nodelta [2,4: #f #stack']]
    832 @eq_f >associative_append @eq_f
    833 lapply prf lapply prf' lapply (taa_end_not_costed … taa)
    834 cases taa -st3 -st2 normalize nodelta
    835 [1,3,5,7,9,11,13: #st2 * #prf #prf' % ]
    836 #st2 #st2' #st3 #H' #G' #K' #taa' #K #prf #prf'
    837 >(not_costed_no_label … K) try % >append_nil %
    838 qed.
    839 
    840 lemma ft_extend_taaf_obs : ∀S,st1,st2,st3,ft,taaf.
    841   ft_stack_observables … (ft_extend_taaf S st1 st2 st3 ft taaf) =
    842     〈ft_stack … ft,
    843      ft_observables … ft @
    844       if taaf_non_empty … taaf then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ]〉.
    845 #S #st1 #st2 #st3 #ft #taa lapply ft cases taa -st2 -st3
    846 [ #st2 #ft >append_nil @eq_pair_fst_snd ]
    847 #st2 #st3 #st4 #taa #H normalize nodelta #G [2: #K ] #ft
    848 whd in match ft_extend_taaf; normalize nodelta
    849 >ft_extend_taa_advance_obs @pair_elim'
    850 >(status_class_dep_match_rewrite … G) %
    851 qed.
    852 
    853 (*
    854 lemma ft_extend_taaf_advance_obs : ∀S,st1,st2,st3,st4.
    855   ∀ft : flat_trace S st1 st2.
    856   ∀taaf : trace_any_any_free S st2 st3.
    857   ∀H : as_execute S st3 st4.∀G.
    858   ft_stack_observables … (ft_advance … (ft_extend_taaf … ft taaf) H G) =
    859   (let add ≝ option_to_list … (! l ← as_label … st2 ; return IEVcost l) in
    860    let 〈stack, tr〉 ≝ ft_stack_observables … ft in
    861    match as_classify … st3 return λx.as_classifier … st3 x → ? with
    862     [ cl_call ⇒ λprf.
    863       let id ≝ as_call_ident ? «st3, prf» in
    864       let tr' ≝ tr @ add @ [IEVcall id] in
    865       〈id :: ft_stack … ft, tr'〉
    866     | cl_tailcall ⇒ λprf.
    867       let id ≝ as_tailcall_ident ? «st3, prf» in
    868       match stack with
    869       [ nil ⇒ (* should never happen in correct programs *)
    870         〈[ ], tr @ add〉
    871       | cons f stack' ⇒
    872         let tr' ≝ tr @ add @ [IEVtailcall f id] in
    873         〈id :: stack', tr'〉
    874       ]
    875     | cl_return ⇒ λ_.
    876       match stack with
    877       [ nil ⇒ (* should never happen in correct programs *)
    878         〈[ ], tr @ add〉
    879       | cons f stack' ⇒
    880         let tr' ≝ tr @ add @ [IEVret f] in
    881         〈stack', tr'〉
    882       ]
    883     | _ ⇒ λ_.〈stack, tr @ add〉
    884     ] (refl …)).
    885 #S #st1 #st2 #st3 #st4 #ft #taaf lapply ft cases taaf
    886 whd in match ft_extend_taaf; normalize nodelta
    887 [ #st #ft #H #G whd in ⊢ (??%?); @pair_elim' normalize nodelta % ]
    888 #st2 #st2' #st3 #taa' #H' #G' [2: #K' ] #ft #H #G
    889 whd in ⊢ (??%?); >ft_extend_taa_advance_obs normalize nodelta
    890 @(pair_elim' … (ft_stack_observables … ft)) normalize nodelta
    891 >(status_class_dep_match_rewrite … G') normalize nodelta
    892 @status_class_dep_match_elim #prf
    893 @status_class_dep_match_elim #prf'
    894 try(@⊥ >prf in prf'; #prf' -prf destruct @False)
    895 [ >associative_append
    896 whd in match ft_stack; whd in match ft_observables; normalize nodelta
    897 [2,3: cases (\fst (ft_stack_observables … ft)) normalize nodelta [2,4: #f #stack']]
    898 @eq_f >associative_append @eq_f
    899 lapply prf lapply prf' lapply G
    900 cases taaf -st3 -st2 normalize nodelta
    901 [1,4,7,10,13,16,19: #st2 #_ #prf #prf' % ]
    902 
    903 >(not_costed_no_label … K) try % >append_nil %
    904 qed.
    905 *)
    906520
    907521(* little helper to avoid splitting equal cases *)
     
    1068682qed.
    1069683
     684definition call_stack_from_obs : list intensional_event → list ident ≝
     685let f ≝ λacc,ev.match ev with
     686  [ IEVcall id ⇒ id :: acc
     687  | IEVret _ ⇒ match acc with [ nil ⇒ [ ] | cons _ tl ⇒ tl ]
     688  | IEVtailcall _ id ⇒ match acc with [ nil ⇒ [ ] | cons _ tl ⇒ id :: tl ]
     689  | _ ⇒ acc
     690  ] in
     691foldl ?? f [ ].
     692
     693lemma ft_stack_from_observables :
     694∀S1,st1,st1'.∀ft : flat_trace S1 st1 st1'.
     695  ft_stack … ft = call_stack_from_obs … (ft_observables … ft).
     696#S1 #st1 #st1' #ft elim ft -st1'
     697[ % ] #st1' #st1'' #pre #ex #ncost #IH whd in match ft_stack; whd in match ft_observables; normalize nodelta
     698whd in match (ft_stack_observables ????); @pair_elim' normalize nodelta
     699@status_class_dep_match_elim #cl [2,3: inversion (\fst (ft_stack_observables ????))
     700  [2,4: #f #stak' #_ ] #EQ_stack normalize nodelta ] whd in match call_stack_from_obs; normalize nodelta
     701[1,2,5: <associative_append >foldl_append whd in ⊢ (???%); ]
     702>foldl_append cases (as_label ??) [2,4,6,8,10,12,14: #lbl]
     703whd in match option_to_list; normalize nodelta
     704whd in match (foldl ?????);
     705change with (call_stack_from_obs ?) in match (foldl ?????);
     706whd in match ft_stack in IH; whd in match ft_observables; normalize nodelta in IH; <IH
     707try >EQ_stack %
     708qed.
     709 
     710lemma ft_stack_observables_eq : ∀S1,S2,st1,st1',st2,st2'.
     711∀ft1 : flat_trace S1 st1 st1'.∀ft2 : flat_trace S2 st2 st2'.
     712ft_observables … ft1 = ft_observables … ft2 →
     713ft_stack_observables … ft1 = ft_stack_observables … ft2.
     714#S1 #S2 #st1 #st1' #st2 #st2' #ft1 #ft2 #EQ
     715>(eq_pair_fst_snd … (ft_stack_observables … ft1))
     716>(eq_pair_fst_snd … (ft_stack_observables … ft2))
     717change with (〈ft_stack … ft1, ft_observables … ft1〉 = 〈ft_stack … ft2, ft_observables … ft2〉)
     718>ft_stack_from_observables >ft_stack_from_observables >EQ %
     719qed.
     720
     721record ft_and_tlr (S : abstract_status) (prefix, subtrace : list intensional_event)
     722(fn : ident) (st1 : S) : Prop ≝
     723{ st2 : S
     724; st3 : S
     725; ft : flat_trace S st1 st2
     726; tlr : trace_label_return S st2 st3
     727; tlr_unrpt : tlr_unrepeating … tlr
     728; ft_is_prefix : ft_observables … ft = prefix
     729; fn_is_current : ft_current_function … ft = Some ? fn
     730; tlr_is_subtrace : observables_trace_label_return … tlr fn = subtrace
     731}.
     732
    1070733theorem status_simulation_produce_ft_and_tlr :
    1071734∀S1,S2.
    1072735∀R.
    1073 ∀st1,st1',st1'',st2.
    1074 ∀ft1 : flat_trace S1 st1 st1'.
    1075 ∀tlr1 : trace_label_return S1 st1' st1''.
     736∀prefix,subtrace,fn.
     737∀st1,st2.
    1076738status_simulation_with_init S1 S2 R st1 st2 →
    1077 ∃st2',st2'',st2'''.
    1078 ∃ft2 : flat_trace S2 st2 st2'.
    1079 ∃tlr2 : trace_label_return S2 st2' st2''.
    1080 ∃taaf : trace_any_any_free S2 st2'' st2'''.
    1081 (∀x.as_result … st1'' = Some ? x → as_result … st2''' = Some ? x) ∧
    1082 ft_observables … ft1 = ft_observables … ft2 ∧
    1083 tlr_rel … tlr1 tlr2.
    1084 #S1 #S2 #R #st1 #st1' #st1'' #st2 #ft1 #tlr1 * #S #L #simul
     739ft_and_tlr S1 prefix subtrace fn st1 →
     740ft_and_tlr S2 prefix subtrace fn st2.
     741#S1 #S2 #R #pref #subtr #fn #st1 #st2
     742* #S #L #simul *
     743#st1' #st1'' #ft1 #tlr1 #unrpt #EQ1 #EQ2 #EQ3
    1085744cases (status_simulation_produce_ft … ft1 simul S L)
    1086 #st2' * #st2_mid * #ft2 * #taa2 ** #S' #L' #EQ1
    1087 cases (status_simulation_produce_tlr … tlr1 taa2 simul S' L')
    1088 #st2'' * #st2''' * #tlr2 * #taa2' **** #_ #S'' #_ #_ #EQ2
    1089 %{st2'} %{st2''} %{st2'''} %{ft2} %{tlr2} %{taa2'} %{EQ2} %
    1090 [ #res #EQ @(sim_final … simul … EQ S'')
    1091 | whd in ⊢ (??%%); @eq_f assumption
     745#st2' * #st2_mid * #ft2 * #taa2 ** #S' #L' #EQ4
     746cases (status_simulation_produce_tlr … tlr1 taa2 simul unrpt S' L')
     747#st2'' * #st2''' * #tlr2 * #taa2' ***** #_ #S'' #_ #_ #EQ5 #unrpt'
     748%{st2' st2'' ft2 tlr2 unrpt' ???}
     749[ whd in ⊢ (??%?); <EQ4 assumption
     750| whd in ⊢ (??%?); whd in match ft_stack; normalize nodelta <EQ4 assumption
     751| <(tlr_rel_to_traces_same_observables … EQ5) assumption
    1092752]
    1093753qed.
  • src/common/StructuredTraces.ma

    r2869 r3145  
    1414  | cl_tailcall: status_class
    1515  | cl_other: status_class.
     16
     17
     18(* helper lemmas in presence of matches on status_class with dependent types *)
     19lemma status_class_dep_match_elim :
     20∀A : Type[0].∀P : A → Prop.
     21∀cl,c_call,c_return,c_tailcall,c_other,c_jump.
     22(∀prf : cl = cl_call.P (c_call prf)) →
     23(∀prf : cl = cl_return.P (c_return prf)) →
     24(∀prf : cl = cl_tailcall.P (c_tailcall prf)) →
     25(∀prf : cl = cl_other.P (c_other prf)) →
     26(∀prf : cl = cl_jump.P (c_jump prf)) →
     27P (match cl return λx.cl = x → ? with
     28   [ cl_call ⇒ c_call
     29   | cl_return ⇒ c_return
     30   | cl_tailcall ⇒ c_tailcall
     31   | cl_other ⇒ c_other
     32   | cl_jump ⇒ c_jump
     33   ] (refl …)).
     34#A #P * normalize // qed.
     35
     36lemma status_class_dep_match_rewrite :
     37∀A : Type[0].
     38∀cl,c_call,c_return,c_tailcall,c_other,c_jump.
     39∀cl'.
     40∀prf : cl = cl'.
     41match cl return λx.cl = x → A with
     42 [ cl_call ⇒ c_call
     43 | cl_return ⇒ c_return
     44 | cl_tailcall ⇒ c_tailcall
     45 | cl_other ⇒ c_other
     46 | cl_jump ⇒ c_jump
     47 ] (refl …) =
     48match cl' return λx.cl = x → A with
     49 [ cl_call ⇒ c_call
     50 | cl_return ⇒ c_return
     51 | cl_tailcall ⇒ c_tailcall
     52 | cl_other ⇒ c_other
     53 | cl_jump ⇒ c_jump
     54 ] prf.
     55#A * #c1 #c2 #c3 #c4 #c5 * #prf destruct % qed.
     56
     57lemma status_class_dep_match_elim' :
     58∀A : Type[0].∀P : A → Prop.∀Q : status_class → Type[0].
     59∀c_return,c_jump,c_call,c_tailcall,c_other.
     60∀cl.∀d : Q cl.
     61(cl = cl_return → ∀d : Q cl_return. P (c_return d)) →
     62(cl = cl_jump → ∀d : Q cl_jump.P (c_jump d)) →
     63(cl = cl_call → ∀d : Q cl_call.P (c_call d)) →
     64(cl = cl_tailcall → ∀d : Q cl_tailcall.P (c_tailcall d)) →
     65(cl = cl_other → ∀d : Q cl_other.P (c_other d)) →
     66P (match cl return λcl.Q cl → A with
     67   [ cl_return ⇒ c_return
     68   | cl_jump ⇒ c_jump
     69   | cl_call ⇒ c_call
     70   | cl_tailcall ⇒ c_tailcall
     71   | cl_other ⇒ c_other
     72   ] d).
     73#A #P #Q #c1 #c2 #c3 #c4 #c5 * /2 by / qed.
    1674
    1775record abstract_status : Type[1] ≝
     
    60118  λS : abstract_status. λl.∃pc.as_cost_labelled_at S l pc.
    61119
     120(*
    62121definition as_cost_label ≝
    63122  λS : abstract_status. Σl.as_cost_labelled S l.
     
    76135  λS : abstract_status. map … (as_cost_get_label S).
    77136*)
    78 
     137*)
    79138definition as_cost_map ≝
    80   λS : abstract_status. (as_cost_label S) → ℕ.
     139  λS : abstract_status. costlabel → ℕ.
    81140 
    82141definition as_label_safe : ∀a_s : abstract_status.
    83   (Σs : a_s.as_costed ? s) → as_cost_label a_s ≝
    84   λa_s,st_sig.«opt_safe ?? (pi2 … st_sig), ?».
    85 @hide_prf
    86 @opt_safe_elim #c #EQ %{EQ} qed.
    87  
     142  (Σs : a_s.as_costed ? s) → costlabel ≝
     143  λa_s,st_sig.opt_safe ?? (pi2 … st_sig).
     144
     145(* 
    88146definition lift_sigma_map_id :
    89147  ∀A,B : Type[0].∀P_in,P_out : A → Prop.B →
     
    134192]
    135193qed.
    136 
     194*)
    137195
    138196(* structured traces: down to business *)
     
    225283          trace_any_label S end_flag status_pre status_end.
    226284
     285let rec tlr_length St st1 st2 (tlr : trace_label_return St st1 st2) on tlr : ℕ ≝
     286  match tlr with
     287  [ tlr_base _ _ tll ⇒ tll_length … tll
     288  | tlr_step _ _ _ tll tl ⇒ tll_length … tll + tlr_length … tl
     289  ]
     290and tll_length St fl st1 st2 (tll : trace_label_label St fl st1 st2) on tll : ℕ ≝
     291  match tll with
     292  [ tll_base _ _ _ tal _ ⇒ tal_length … tal
     293  ]
     294and tal_length St fl st1 st2 (tal : trace_any_label St fl st1 st2) on tal : ℕ ≝
     295  match tal with
     296  [ tal_step_call _ _ _ _ _ _ _ _ tlr _ tl ⇒ S (tlr_length … tlr + tal_length … tl)
     297  | tal_step_default _ _ _ _ _ tl _ _ ⇒ S (tal_length … tl)
     298  | tal_base_call _ _ _ _ _ _ trace _ ⇒ S (tlr_length … trace)
     299  | tal_base_tailcall _ _ _ _ _ trace ⇒ S (tlr_length … trace)
     300  | tal_base_return _ _ _ _ ⇒ 1
     301  | tal_base_not_return _ _ _ _ _ ⇒ 1
     302  ].
     303
     304
    227305let rec tal_pc_list (S : abstract_status) fl st1 st2 (tal : trace_any_label S fl st1 st2)
    228306  on tal : list (as_pc S) ≝
     
    236314 ].
    237315
     316(* watch out, this length does not count all states but only same-level ones *)
    238317definition as_trace_any_label_length':
    239318    ∀S: abstract_status.
     
    601680    match tll2 with
    602681    [ tll_base fl2 st2 st2 tal2 G ⇒
    603       pi1 … (as_label_safe … («?, H»)) = pi1 … (as_label_safe … («?, G»)) ∧
     682      as_label_safe … («?, H») = as_label_safe … («?, G») ∧
    604683      tal_rel … tal1 tal2
    605684    ]
     
    734813| IEVret : ident → intensional_event.
    735814
    736 (* NB: we don't restrict call idents, because it would need some more tinkering
    737    with abstract_status *)
    738 definition as_emittable : abstract_status → intensional_event → Prop ≝
    739 λS,ev.
    740 match ev with
    741 [ IEVcost c ⇒ as_cost_labelled S c
    742 | _ ⇒ True
    743 ].
    744  
    745 definition as_trace ≝
    746 λS : abstract_status.
    747 Σl : list intensional_event.All … (as_emittable S) l.
    748 
    749 unification hint 0 ≔ S ⊢ as_trace S ≡ Sig (list intensional_event) (λl.All … (as_emittable S) l).
    750 
    751 definition cons_safe : ∀A,P.(Σx.P x) → (Σl.All A P l) → Σl.All A P l ≝
    752 λA,P,x,l.«x::l, conj … (pi2 … x) (pi2 … l)».
    753 
    754 definition append_safe : ∀A,P.(Σl.All A P l) → (Σl.All A P l) → Σl.All A P l ≝
    755 λA,P,l1,l2.«l1@l2,
    756   cic:/matita/cerco/utilities/lists/All_append.def(2) … (pi2 … l1) (pi2 … l2)».
    757 
    758 definition nil_safe : ∀A,P.(Σl.All A P l) ≝ λA,P.«[ ], I».
    759 
    760 interpretation "safe consing" 'vcons hd tl = (cons_safe ?? hd tl).
    761 interpretation "safe appending" 'vappend l1 l2 = (append_safe ?? l1 l2).
    762 interpretation "safe nil" 'vnil = (nil_safe ??).
    763 
    764 definition emittable_cost : ∀S.as_cost_label S → Σev.as_emittable S ev ≝
    765 λS,l.«IEVcost l, pi2 … l».
    766 
    767815let rec observables_trace_label_label
    768816  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
     
    770818      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
    771819      (curr : ident)
    772         on the_trace: as_trace S
     820        on the_trace: list intensional_event
    773821  match the_trace with
    774822  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
    775823      let label ≝ as_label_safe … «?, labelled_proof» in
    776       emittable_cost … label ::: observables_trace_any_label S ends_flag initial final given_trace curr
     824      IEVcost label :: observables_trace_any_label S ends_flag initial final given_trace curr
    777825  ]
    778826and observables_trace_any_label
     
    781829      (the_trace: trace_any_label S trace_ends_flag start_status final_status)
    782830      (curr : ident)
    783         on the_trace: as_trace S
     831        on the_trace: list intensional_event
    784832  match the_trace with
    785   [ tal_base_not_return the_status _ _ _ _ ⇒ [[ ]]
     833  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
    786834  | tal_base_call pre_fun_call start_fun_call final _ cl _ call_trace _ ⇒
    787835      let id ≝ as_call_ident ? «?, cl» in
    788       IEVcall id ::: observables_trace_label_return ??? call_trace id
     836      IEVcall id :: observables_trace_label_return ??? call_trace id
    789837  | tal_base_tailcall pre_fun_call start_fun_call final _ cl call_trace ⇒
    790838      let id ≝ as_tailcall_ident ? «?, cl» in
    791       IEVtailcall curr id ::: observables_trace_label_return … call_trace id
    792   | tal_base_return the_status _ _ _ ⇒ [[ IEVret curr]]
     839      IEVtailcall curr id :: observables_trace_label_return … call_trace id
     840  | tal_base_return the_status _ _ _ ⇒ [ IEVret curr]
    793841  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    794842    _ cl _ call_trace _ final_trace ⇒
     
    796844    let call_cost_trace ≝ observables_trace_label_return … call_trace id in
    797845    let final_cost_trace ≝ observables_trace_any_label … end_flag … final_trace curr in
    798     IEVcall id ::: call_cost_trace @@ final_cost_trace
     846    IEVcall id :: call_cost_trace @ final_cost_trace
    799847  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    800848    observables_trace_any_label … tail_trace curr
     
    805853      (the_trace: trace_label_return S start_status final_status)
    806854      (curr : ident)
    807         on the_trace: as_trace S
     855        on the_trace: list intensional_event
    808856  match the_trace with
    809857  [ tlr_base before after trace_to_lift ⇒
     
    812860    let labelled_cost ≝ observables_trace_label_label … doesnt_end_with_ret … labelled_trace curr in
    813861    let return_cost ≝ observables_trace_label_return … ret_trace curr in
    814         labelled_cost @@ return_cost
    815   ]. % qed.
     862        labelled_cost @ return_cost
     863  ].
    816864 
    817865let rec filter_map X Y (f : X → option Y) (l : list X) on l : list Y ≝
     
    848896#X #Y #f #g #l #H elim l normalize [%] #hd #tl #IH >H @eq_f @IH qed.
    849897
    850 let rec list_distribute_sig_aux X P (l : list X) on l : All X P l → list (Σx.P x) ≝
    851 match l return λl.All X P l → list (Σx.P x) with
    852 [ nil ⇒ λ_.[ ]
    853 | cons hd tl ⇒ λprf.«hd, proj1 … prf» :: list_distribute_sig_aux X P tl (proj2 … prf)
    854 ].
    855 
    856 definition list_distribute_sig : ∀A,P.(Σl.All A P l) → list (Σx.P x) ≝
    857 λA,P,l.list_distribute_sig_aux … l (pi2 … l).
    858 
    859 lemma list_distribute_sig_append:
    860  ∀A,P,l1,l2,prf1,prf2,prf3.
    861   list_distribute_sig A P «l1@l2,prf3» =
    862    list_distribute_sig … «l1,prf1» @ list_distribute_sig … «l2,prf2».
    863  #A #P #l1 whd in match list_distribute_sig; normalize nodelta elim l1 //
    864  #hd #tl #IH normalize #l2 #prf1 #prf2 #prf3 <IH //
    865 qed.
    866 
    867 let rec list_factor_sig X P (l : list (Σx.P x)) on l : Σl.All X P l ≝
    868 match l with
    869 [ nil ⇒ [[ ]]
    870 | cons hd tl ⇒ hd ::: list_factor_sig … tl
    871 ].
    872 
    873 definition costlabels_of_observables : ∀S.as_trace S → list (as_cost_label S) ≝
    874 λS,l.filter_map (Σev.as_emittable S ev) ?
    875   (λev.match ev return λev.as_emittable S ev → option ? with
    876     [ IEVcost c ⇒ λprf.Some ? «c, prf»
    877     | _ ⇒ λ_.None ?
    878     ] (pi2 … ev)) (list_distribute_sig … l).
     898definition costlabels_of_observables : list intensional_event →
     899   list costlabel ≝
     900filter_map ??
     901  (λev.match ev with
     902    [ IEVcost c ⇒ Some ? c
     903    | _ ⇒ None ?
     904    ]).
    879905
    880906axiom costlabels_of_observables_trace_label_return_id_irrelevant:
    881907 ∀S,s1,s2,tr,id1,id2.
    882   costlabels_of_observables S (observables_trace_label_return S s1 s2 tr id1) =
    883   costlabels_of_observables S (observables_trace_label_return S s1 s2 tr id2).
     908  costlabels_of_observables (observables_trace_label_return S s1 s2 tr id1) =
     909  costlabels_of_observables (observables_trace_label_return S s1 s2 tr id2).
    884910
    885911lemma costlabels_of_observables_append:
    886  ∀S:abstract_status. ∀tr1,tr2: as_trace S.
    887   costlabels_of_observables S (tr1 @ tr2) =
    888    costlabels_of_observables … tr1 @ costlabels_of_observables … tr2.
    889 [ #S #tr1 #tr2 whd in match costlabels_of_observables; normalize nodelta
    890   <filter_map_append <list_distribute_sig_append //
    891 | @All_append [ @(pi2 … tr1) | @(pi2 … tr2) ]]
    892 qed.
     912 ∀tr1,tr2.
     913  costlabels_of_observables (tr1 @ tr2) =
     914   costlabels_of_observables … tr1 @ costlabels_of_observables … tr2 ≝
     915filter_map_append ….
    893916
    894917(* JHM: base case now passes the termination checker *)
     
    929952          on the_trace_l:
    930953            tll_rel … the_trace_l the_trace_r →
    931               pi1 … (observables_trace_label_label … the_trace_l curr) =
    932                 pi1 … (observables_trace_label_label … the_trace_r curr)
     954               observables_trace_label_label … the_trace_l curr =
     955                 observables_trace_label_label … the_trace_r curr
    933956  match the_trace_l with
    934957  [ tll_base fl1 st1 st1' tal1 H ⇒
     
    946969          on the_trace_l:
    947970            tal_rel … the_trace_l the_trace_r →
    948               pi1 … (observables_trace_any_label … the_trace_l curr) =
    949                 pi1 … (observables_trace_any_label … the_trace_r curr)
     971              observables_trace_any_label … the_trace_l curr =
     972                observables_trace_any_label … the_trace_r curr
    950973  match the_trace_l with
    951974  [ tal_base_not_return st1 st1' H G K ⇒ ?
     
    964987        on the_trace_l:
    965988          tlr_rel … the_trace_l the_trace_r →
    966             pi1 … (observables_trace_label_return … the_trace_l curr) =
    967               pi1 … (observables_trace_label_return … the_trace_r curr)
     989            observables_trace_label_return … the_trace_l curr =
     990              observables_trace_label_return … the_trace_r curr
    968991  match the_trace_l with
    969992  [ tlr_base before after tll_l ⇒ ?
     
    971994  ]. 
    972995[ * #EQ #H_tal
    973   whd in ⊢ (??%%); @eq_f2 [2: @(tal_rel_to_traces_same_observables … H_tal)]
    974   cases (as_label_safe ??) in EQ; #c1 #H1
    975   cases (as_label_safe ??) #c2 #H2 #EQ destruct %
     996  whd in ⊢ (??%%); @eq_f2 [2: @(tal_rel_to_traces_same_observables … H_tal)] cases EQ %
    976997|2,3,4,5,6,7:
    977998  [1,2,3,4: * #EQ destruct(EQ)]
     
    9861007      [| *#tl2] ** #EQ #H_tl #H_tlr
    9871008    ] >EQ >taa_append_tal_same_observables
    988   | whd in ⊢ (%→??(???%)?); @tal_rel_to_traces_same_observables
     1009  | whd in ⊢ (%→??%?); @tal_rel_to_traces_same_observables
    9891010  ]
    9901011  whd in ⊢ (??%%);
     
    10401061*)
    10411062
    1042 lemma map_pi1_distribute_sig : ∀A,P,l.
    1043   map ?? (pi1 ??) (list_distribute_sig A P l) = pi1 ?? l.
    1044 #A #P * #l elim l -l normalize // qed.
    1045 
    10461063definition flatten_trace_label_return ≝
    10471064  λS,st1,st2.λtlr : trace_label_return S st1 st2.
     
    10641081  let dummy ≝ an_identifier ? one in
    10651082  costlabels_of_observables … (observables_trace_any_label … tll dummy).
    1066 
    1067 lemma lift_cost_map_same_cost_tlr :
    1068   ∀S_in, S_out, dec, m_out, start_in, start_out, end_in, end_out.
    1069   ∀the_trace_in : trace_label_return S_in start_in end_in.
    1070   ∀the_trace_out : trace_label_return S_out start_out end_out.
    1071   tlr_rel … the_trace_in the_trace_out →
    1072   (Σ_{l ∈ flatten_trace_label_return … the_trace_in}
    1073     (lift_cost_map_id … dec m_out l)) =
    1074   (Σ_{l ∈ flatten_trace_label_return … the_trace_out} (m_out l)).
    1075 #S_in #S_out #dec #m_out #start_in #start_out #end_in #end_out
    1076 #tlr_in #tlr_out #H_tlr
    1077 @lift_cost_map_same_cost
    1078 whd in match flatten_trace_label_return; normalize nodelta
    1079 >map_to_filter_map >map_to_filter_map >filter_map_compose
    1080 >filter_map_compose
    1081 cut (∀S.∀x: (Σev.as_emittable S ev).
    1082   ! y ←
    1083     match pi1 ?? x return λx.as_emittable S x → option (Σc.as_cost_labelled S c) with
    1084     [ IEVcost c ⇒ λprf.Some ? «c, prf» | _ ⇒ λ_.None ? ] (pi2 ?? x) ;
    1085   Some ? (pi1 ?? y) =
    1086   ! ev ← Some ? (pi1 ?? x) ;
    1087   match ev with [ IEVcost c ⇒ Some ? c | _ ⇒ None ?])
    1088 [ #S ** [ #c #em | #i * | #i #j * | #i * ] %]
    1089 #EQext >(filter_map_ext_eq … (EQext S_in)) >(filter_map_ext_eq … (EQext S_out))
    1090 <filter_map_compose <filter_map_compose @eq_f
    1091 <map_to_filter_map <map_to_filter_map
    1092 >map_pi1_distribute_sig >map_pi1_distribute_sig
    1093 @(tlr_rel_to_traces_same_observables … H_tlr) %
    1094 qed.
    1095 
    1096 lemma lift_cost_map_same_cost_tll :
    1097   ∀S_in, S_out, dec, m_out, fl_in, fl_out, start_in, start_out, end_in, end_out.
    1098   ∀the_trace_in : trace_label_label S_in fl_in start_in end_in.
    1099   ∀the_trace_out : trace_label_label S_out fl_out start_out end_out.
    1100   tll_rel … the_trace_in the_trace_out →
    1101   (Σ_{l ∈ flatten_trace_label_label … the_trace_in}
    1102     (lift_cost_map_id … dec m_out l)) =
    1103   (Σ_{l ∈ flatten_trace_label_label … the_trace_out} (m_out l)).
    1104 #S_in #S_out #dec #m_out #fl_in #fl_out #start_in #start_out #end_in #end_out
    1105 #tlr_in #tlr_out #H_tlr
    1106 @lift_cost_map_same_cost
    1107 whd in match flatten_trace_label_label; normalize nodelta
    1108 >map_to_filter_map >map_to_filter_map >filter_map_compose
    1109 >filter_map_compose
    1110 cut (∀S.∀x: (Σev.as_emittable S ev).
    1111   ! y ←
    1112     match pi1 ?? x return λx.as_emittable S x → option (Σc.as_cost_labelled S c) with
    1113     [ IEVcost c ⇒ λprf.Some ? «c, prf» | _ ⇒ λ_.None ? ] (pi2 ?? x) ;
    1114   Some ? (pi1 ?? y) =
    1115   ! ev ← Some ? (pi1 ?? x) ;
    1116   match ev with [ IEVcost c ⇒ Some ? c | _ ⇒ None ?])
    1117 [ #S ** [ #c #em | #i * | #i #j * | #i * ] %]
    1118 #EQext >(filter_map_ext_eq … (EQext S_in)) >(filter_map_ext_eq … (EQext S_out))
    1119 <filter_map_compose <filter_map_compose @eq_f
    1120 <map_to_filter_map <map_to_filter_map
    1121 >map_pi1_distribute_sig >map_pi1_distribute_sig
    1122 @(tll_rel_to_traces_same_observables … H_tlr) %
    1123 qed.
    11241083
    11251084(* the equivalent of a collapsable trace_any_label where we do not force
     
    12431202  taaf_step_jump … (taaf_append_taa … taaf1 ? taa) H' I' K'
    12441203] taaf1. @prf qed.
     1204
     1205lemma taa_end_not_costed : ∀S,s1,s2.∀taa : trace_any_any S s1 s2.
     1206  if taa_non_empty … taa then ¬as_costed … s2 else True.
     1207#S #s1 #s2 #taa elim taa -s1 -s2 normalize nodelta
     1208[ #s1 %
     1209| #s1 #s2 #s3 #H #G #K #tl lapply K lapply H cases tl -s2 -s3
     1210  [ #s2 #H #K #_ assumption
     1211  | #s2 #s3 #s4 #H' #G' #K' #tl' #H #K #I @I
     1212  ]
     1213]
     1214qed.
     1215
     1216let rec tal_collapsable_to_rel S fl st1 st2
     1217  (tal : trace_any_label S fl st1 st2) on tal :
     1218  tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
     1219  tal_rel … tal (tal_base_not_return S2 st12 st22 H I J) ≝
     1220  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
     1221  tal_rel … tal (tal_base_not_return S2 st12 st22 H I J)
     1222  with
     1223  [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_to_rel ???? tl
     1224  | tal_base_not_return _ st2' _ _ K ⇒ ?
     1225  | _ ⇒ Ⓧ
     1226  ].
     1227* #S2 #st12 #st22 #H #I #J % %[|%{(taa_base ??)} %[|%[|%[| %
     1228qed.
     1229
     1230let rec tal_collapsable_eq_flag S fl st1 st2
     1231  (tal : trace_any_label S fl st1 st2) on tal :
     1232  tal_collapsable ???? tal → fl = doesnt_end_with_ret ≝
     1233  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → fl = ?
     1234  with
     1235  [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_eq_flag ???? tl
     1236  | tal_base_not_return _ st2' _ _ K ⇒ λ_.refl …
     1237  | _ ⇒ Ⓧ
     1238  ].
     1239
     1240let rec tal_collapsable_split S fl st1 st2
     1241  (tal : trace_any_label S fl st1 st2) on tal :
     1242  tal_collapsable ???? tal → ∃st2_mid.∃taa : trace_any_any S st1 st2_mid.∃H,I,J.
     1243  tal ≃ taa @ tal_base_not_return … st2 H I J ≝
     1244  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∃st2_mid,taa,H,I,J.
     1245  tal ≃ taa @ tal_base_not_return … st2_mid ? H I J
     1246  with
     1247  [ tal_step_default fl' st1' st2' st3' H tl I J ⇒ ?
     1248  | tal_base_not_return st1' st2' H I J ⇒ ?
     1249  | _ ⇒ Ⓧ
     1250  ].
     1251[ * %{st1'} %{(taa_base …)} %{H} %{I} %{J} %
     1252| #coll
     1253  elim (tal_collapsable_split … tl coll) #st2_mid * #taa * #H' * #I' *#J'
     1254  #EQ %{st2_mid} %{(taa_step … taa)} try assumption
     1255  %{H'} %{I'} %{J'} lapply EQ lapply tl >(tal_collapsable_eq_flag … coll) -tl #tl
     1256  #EQ >EQ %
     1257]
     1258qed.
     1259
     1260lemma tal_collapsable_to_rel_symm : ∀S,fl,st1,st2,tal.
     1261tal_collapsable S fl st1 st2 tal → ∀S2,st12,st22,H,I,J.
     1262  tal_rel … (tal_base_not_return S2 st12 st22 H I J) tal.
     1263#S #fl #st1 #st2 #tal #coll #S2 #st12 #st22 #H #I #J
     1264elim (tal_collapsable_split … coll) lapply tal
     1265 >(tal_collapsable_eq_flag … coll) -tal #tal
     1266#st2_mid * #taa *#H' *#I' *#J' #EQ >EQ % [%]
     1267%[|%[|%[|%[|%[| % ]]]]]
     1268qed.
     1269
     1270
     1271let rec taa_append_tal_rel S1 fl1 st1 st1'
     1272  (tal1 : trace_any_label S1 fl1 st1 st1')
     1273  S2 st2 st2mid fl2 st2'
     1274  (taa2 : trace_any_any S2 st2 st2mid)
     1275  (tal2 : trace_any_label S2 fl2 st2mid st2')
     1276  on tal1 :
     1277  tal_rel … tal1 tal2 →
     1278  tal_rel … tal1 (taa2 @ tal2) ≝
     1279match tal1 return λfl1,st1,st1',tal1.? with
     1280  [ tal_base_not_return st1 st1' _ _ _ ⇒ ?
     1281  | tal_base_return st1 st1' _ _ ⇒ ?
     1282  | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ ?
     1283  | tal_base_tailcall st1 st1' st1'' _ prf tlr1 ⇒ ?
     1284  | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ ?
     1285  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ ?
     1286  ].
     1287[ * #EQfl *#st2mid *#taa2' *#H2 *#G2 *#K2 #EQ
     1288| * #EQfl *#st2mid *#taa2' *#H2 *#G2 #EQ
     1289| * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
     1290  [ *#K2 *#tlr2 *#L2 * #EQ #EQ'
     1291  | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #coll
     1292  ]
     1293| * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *#tlr2 * #EQ #EQ'
     1294| * #st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
     1295  [ * #EQfl *#K2 *#tlr2 *#L2 ** #EQ #coll #EQ'
     1296  | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #EQ''
     1297  ]
     1298| whd in ⊢ (%→%); @(taa_append_tal_rel … tl1)
     1299]
     1300destruct
     1301<associative_taa_append_tal
     1302  [1,2,3,4,5:%{(refl …)}] %{st2mid}
     1303  [1,2:|*: %{G2} %{EQcall} ]
     1304  %{(taa_append_taa … taa2 taa2')}
     1305  [1,2: %{H2} %{G2} [%{K2}] %
     1306  |5: %{st2mid'} %{H2} %{tlr2} % //
     1307  |*: %{st2mid'} %{H2}
     1308    [1,3: %1 [|%{(refl …)}] |*: %2 %{st2mid''} ]
     1309    %{K2} %{tlr2} %{L2} [3,4: %{tl2} ] /3 by conj/
     1310  ]
     1311qed.
     1312
     1313lemma taaf_append_tal_rel : ∀S1,fl1,st1,st1',S2,fl2,st2_pre,st2,st2',tal1,taaf2,H,tal2.
     1314  tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2' tal1 tal2 →
     1315  tal_rel … tal1 (taaf_append_tal S2 st2_pre … taaf2 H tal2).
     1316#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 * -H7 -H8 normalize
     1317[ // |3: #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 generalize in match (? : False); * ]
     1318#H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24
     1319change with (taa_step ???? ??? (taa_base ??) @ H23) in match (tal_step_default ?????????);
     1320/2 by taa_append_tal_rel/
     1321qed.
  • src/common/stacksize.ma

    r2755 r3145  
    1515    λf.match stacksizes f with
    1616      [ Some n ⇒ n | None ⇒ 0 (* should never happen *) ] in
    17   let f ≝ λud,acc.
     17  let f ≝ λacc,ud.
    1818    match ud with
    1919    [ up i ⇒
     
    2525      mk_stacksize_info new_stack (maximum acc)
    2626    ] in
    27   foldr ?? f.
     27  foldl ?? f.
     28
     29lemma foldr_append : ∀A,B,f,b,l1,l2.
     30foldr A B f b (l1@l2) = foldr A B f (foldr A B f b l2) l1.
     31#A #B #f #b #l1 elim l1 -l1 [#l2 %]
     32#hd #tl #IH #l2 whd in ⊢ (??%%); >IH %
     33qed.
     34
     35lemma foldl_append : ∀A,B,f,b,l1,l2.
     36foldl A B f b (l1@l2) = foldl A B f (foldl A B f b l1) l2.
     37#A #B #f #b #l1 lapply b -b elim l1 -l1 [#b #l2 %]
     38#hd #tl #IH #b #l2 whd in ⊢ (??%(????%?)); >IH %
     39qed.
     40
     41lemma update_stacksize_info_append :
     42∀ss,info,l1,l2.
     43update_stacksize_info ss info (l1 @ l2) =
     44update_stacksize_info ss (update_stacksize_info ss info l1) l2.
     45#ss #info @foldl_append qed.
    2846
    2947definition extract_call_ud_from_observables :
     
    3250[ IEVcall i ⇒ [up i] | IEVtailcall i j ⇒ [down i; up j] | IEVret i ⇒ [down i] | _ ⇒ [ ]] in
    3351foldr ?? (λev.append ? (f ev)) [ ].
     52
     53lemma extract_call_ud_from_observables_append :
     54∀l1,l2.extract_call_ud_from_observables (l1@l2) =
     55  extract_call_ud_from_observables l1 @ extract_call_ud_from_observables l2.
     56#l1 elim l1 -l1 [ #l2 % ]
     57#hd #tl #IH #l2 whd in ⊢ (??%(??%?)); >associative_append @eq_f @IH qed.
     58
     59lemma update_stacksize_info_max_monotone :
     60∀ss,info,l.maximum info ≤ maximum (update_stacksize_info ss info l).
     61#ss #info #l lapply info elim l -l [ #info % ]
     62* #id #tl #IH #info
     63whd in match (update_stacksize_info ???); normalize nodelta
     64change with (update_stacksize_info ???) in ⊢ (??(?%));
     65@(transitive_le ???? (IH …))
     66[ whd in ⊢ (??%); @(leb_elim (?:ℕ)) #H ] //
     67qed.
    3468
    3569definition extract_call_ud_from_tlr :
Note: See TracChangeset for help on using the changeset viewer.