Changeset 2436 for src/common


Ignore:
Timestamp:
Nov 6, 2012, 4:13:00 PM (7 years ago)
Author:
tranquil
Message:

small changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2421 r2436  
    3131     necessary for as_after_return (typically just the program counter)
    3232     maybe what function is called too? *)
    33   ; call_rel : ∀f.(Σs.as_classifier S1 s (cl_call f)) →
    34                   (Σs.as_classifier S2 s (cl_call f)) → Prop
     33  ; call_rel : (Σs.as_classifier S1 s cl_call) →
     34               (Σs.as_classifier S2 s cl_call) → Prop
    3535  ; sim_final :
    3636    ∀st1,st2.sem_rel st1 st2 → as_final … st1 ↔ as_final … st2
     
    4949
    5050definition ret_rel ≝ λS1,S2.λR : status_rel S1 S2.λs1,s2.
    51   ∀f,s1_pre,s2_pre.call_rel … R f s1_pre s2_pre →
    52                    as_after_return S1 «s1_pre, ex_intro … (pi2 … s1_pre)» s1 →
    53                    as_after_return S2 «s2_pre, ex_intro … (pi2 … s2_pre)» s2.
     51  ∀s1_pre,s2_pre.call_rel … R s1_pre s2_pre →
     52                 as_after_return S1 s1_pre s1 →
     53                 as_after_return S2 s2_pre s2.
    5454
    5555(* the equivalent of a collapsable trace_any_label where we do not force
     
    7676  { sim_status_rel :> status_rel S1 S2
    7777  ; sim_execute :
    78     ∀st1,st1',c,st2.as_execute S1 st1 st1' →
     78    ∀st1,cl,st1',st2.as_execute S1 st1 st1' →
    7979    sim_status_rel st1 st2 →
    80     ∀prf : as_classifier S1 st1 c.
    81     match c return λc.as_classifier S1 st1 c → ? with
    82     [ cl_call f ⇒ λprf.
     80    ∀prf : as_classifier S1 st1 cl.
     81    match cl return λc.as_classifier S1 st1 c → ? with
     82    [ cl_call ⇒ λprf.
    8383      (*
    8484           st1' ------------S----------\
     
    9090           st2 →taa→ st2_pre_call
    9191      *)
    92       ∃st2_pre_call.call_rel ?? sim_status_rel f «st1, prf» st2_pre_call ∧
     92      ∃st2_pre_call.
     93      as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
     94      call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
    9395      ∃st2_after_call,st2'.
    9496      ∃taa2 : trace_any_any … st2 st2_pre_call.
     
    188190  on tal1 :
    189191  tal_rel … tal1 tal2 →
    190   tal_rel … tal1 (taa2 @ tal2) ≝ ?.
    191 cases tal1 -fl1 -st1 -st1'
    192 [ #H1 #H2 #H3 #H4 #H5 *#K1 *#K2 *#K3 *#K4 *#K5 *#K6 #EQ
    193 | #H1 #H2 #H3 #H4 *#K1 *#K2 *#K3 *#K4 *#K5 #EQ
    194 | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 *#K1 *#K2 *#K3 *#K4 *#K5 *
    195   [*#K6 *#K7 *#K8 *#K9 *#K10 * #EQ #EQ'
    196   |*#K6 *#K7 *#K8 *#K9 *#K10 *#K11 *#K12 ** #EQ #EQ' #coll
    197   ]
    198 | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12
    199   *#K2 *#K3 *#K4 *#K5 *
    200   [*#EQ_fl *#K6 *#K7 *#K8 *#K9 *#K10 ** #EQ #coll #EQ'
    201   |*#K6 *#K7 *#K8 *#K9 *#K10 *#K11 *#K12 ** #EQ #EQ' #EQ''
    202   ]
    203 | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 whd in ⊢ (%→%); @(taa_append_tal_rel … H6)
     192  tal_rel … tal1 (taa2 @ tal2) ≝
     193match tal1 return λfl1,st1,st1',tal1.? with
     194  [ tal_base_not_return st1 st1' _ _ _ ⇒ ?
     195  | tal_base_return st1 st1' _ _ ⇒ ?
     196  | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ ?
     197  | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ ?
     198  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ ?
     199  ].
     200[ * #EQfl *#st2mid *#taa2' *#H2 *#G2 *#K2 #EQ
     201| * #EQfl *#st2mid *#taa2' *#H2 *#G2 #EQ
     202| * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
     203  [ *#K2 *#tlr2 *#L2 * #EQ #EQ'
     204  | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #coll
     205  ]
     206| * #st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
     207  [ * #EQfl *#K2 *#tlr2 *#L2 ** #EQ #coll #EQ'
     208  | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #EQ''
     209  ]
     210| whd in ⊢ (%→%); @(taa_append_tal_rel … tl1)
    204211]
    205212destruct
    206213<associative_taa_append_tal
    207   [1,2,3,4:% try @refl] %{K2} %{(taa_append_taa … taa2 K3)}
    208   [1,2,3: % [2,4,6: % [2: % [2:%] |4:% |6: %1 %{K6} %{K7} %{K8} %{K9} %{K10} %{EQ'} % ]]
    209   |*: %{K4} %{K5}
    210     [1,3: %2 %{K6} %{K7} %{K8} %{K9} %{K10} %{K11} %{K12}
    211     | %1 %{(refl …)} %{K6} %{K7} %{K8} %{K9} %{K10}
    212     ] /3 by conj/
     214  [1,2,3,4:%{(refl …)}] %{st2mid}
     215  [1,2:|*: %{G2} %{EQcall} ]
     216  %{(taa_append_taa … taa2 taa2')}
     217  [1,2: %{H2} %{G2} [%{K2}] %
     218  |*: %{st2mid'} %{H2}
     219    [1,3: %1 [|%{(refl …)}] |*: %2 %{st2mid''} ]
     220    %{K2} %{tlr2} %{L2} [3,4: %{tl2} ] /3 by conj/
    213221  ]
    214222qed.
     
    217225  on tal : as_costed … st2 ≝
    218226  match tal return λfl,st1,st2,tal.fl = doesnt_end_with_ret → as_costed ? st2 with
    219   [ tal_step_call fl' _ _ st1' st2' _ _ _ _ _ _ tl ⇒ λprf.tal_end_costed ? st1' st2' (tl⌈trace_any_label ????↦?⌉)
     227  [ tal_step_call fl' _ _ st1' st2' _ _ _ _ _ tl ⇒ λprf.tal_end_costed ? st1' st2' (tl⌈trace_any_label ????↦?⌉)
    220228  | tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ λprf.tal_end_costed ? st1'st2' (tl⌈trace_any_label ????↦?⌉)
    221229  | tal_base_not_return _ st2' _ _ K ⇒ λ_.K
    222230  | tal_base_return _ _ _ _ ⇒ λprf.⊥
    223   | tal_base_call _ _ st2' _ _ _ _ _ K ⇒ λ_.K
     231  | tal_base_call _ _ st2' _ _ _ _ K ⇒ λ_.K
    224232  ] (refl …).
    225233[ destruct
     
    390398  [ tal_base_not_return st1' st1'' H G K ⇒ ?
    391399  | tal_base_return st1' st1'' H G ⇒ ?
    392   | tal_base_call st1_pre_call st1_after_call st1' H f G K tlr1 L ⇒ ?
    393   | tal_step_call fl1' st1' st1'' st1''' st1'''' H f G L tlr1 K tl1 ⇒ ?
     400  | tal_base_call st1_pre_call st1_after_call st1' H G K tlr1 L ⇒ ?
     401  | tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ?
    394402  | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ?
    395403  ].
     
    446454| (* tal_base_call *) whd
    447455  elim (sim_execute … R … H st1_R_st2 G)
    448   * #st2_pre_call #G2 * #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
     456  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
    449457  #st1_R_st2_mid #st1_L_st2_after_call
    450458  elim (status_simulation_produce_tlr ?? R ???? tlr1 taa2' st1_R_st2_mid st1_L_st2_after_call)
     
    456464  #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S %1
    457465  %{st2'}
    458   [ %{(taa2 @ tal_base_call ???? H2 ? G2 ? tlr2 ?)}
     466  [ %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)}
    459467    [3: % [ % assumption ]
    460       % [%] %[|%[|%[|%[| %1 %[|%[|%[|%[|%[| %{S} % ]]]]]]]]]
     468      % [%] %[|%[| %{EQcall} %[|%[|%[| %1 %[|%[|%[| %{S} % ]]]]]]]]
    461469    ]
    462   | %{(taa2 @ tal_step_call ?????? H2 ? G2 ? tlr2 ncost (taa2'' @ tal_base_not_return … I2 (or_intror ?? J2) ?))}
     470  | %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (taa2'' @ tal_base_not_return … I2 (or_intror ?? J2) ?))}
    463471    [3: % [ % assumption ]
    464       % [%] %[|%[|%[|%[| %2 %[|%[|%[|%[|%[|%[|%[| % [ %{S} % ] /2 by taa_append_collapsable, I/
    465       ]]]]]]]]]]]
     472      % [%] %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| % [ %{S} % ] /2 by taa_append_collapsable, I/
     473      ]]]]]]]]]]
    466474    ]
    467475  ]
     
    471479| (* tal_step_call *)
    472480  elim (sim_execute … R … H st1_R_st2 G)
    473   * #st2_pre_call #G2 * #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
     481  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
    474482  #st1_R_st2_mid #st1_L_st2_after_call
    475483  elim (status_simulation_produce_tlr ?? R ???? tlr1 taa2' st1_R_st2_mid st1_L_st2_after_call)
     
    480488  cases fl1' in tl1; #tl1 *
    481489  [ #st2'' * #st2''' * #tl2 * #taa2''' **** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S'
    482     %[|%[| %{(taa2 @ tal_step_call ?????? H2 ? G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
     490    %[|%[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
    483491    [4: %{taa2'''} % [ /4 by conj/ ]
    484       %[|%[|%[|%[| %2 %[|%[|%[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]]
     492      %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
    485493    ]]] 
    486494  | *#st2'' *#tl2 ** #st1_R_st2'' #st1_L_st2'' #S' %1
    487     %[| %{(taa2 @ tal_step_call ?????? H2 ? G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
     495    %[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
    488496    [4: % [ /2 by conj/ ]
    489       %[|%[|%[|%[| %2 %[|%[|%[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]]
     497      %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
    490498    ]]
    491499  | lapply S lapply tlr2 lapply st1_Rret_st2' lapply st1_L_st2' lapply st1_R_st2'
     
    493501    [ #st2' * #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
    494502      *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost %1
    495       %[| %{(taa2 @ tal_base_call ???? H2 ? G2 ? tlr2 ?)}
     503      %[| %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)}
    496504      [3: % [ /2 by conj/ ]
    497       %[|%[|%[|%[| %1 %{(refl …)} %[|%[|%[|%[|%[| %{S} %{tl1_coll} % ]]]]]]]]]]]
     505      %[|%[| %{EQcall} %[|%[|%[| %1 %{(refl …)} %[|%[|%[| %{S} %{tl1_coll} % ]]]]]]]]]]
    498506    | #st2_after_ret #st2_after_ret' #st2' #hd #I2' #J2' #ncost
    499507      #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
    500508      *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost' %1
    501       %[| %{(taa2 @ tal_step_call ?????? H2 ? G2 ? tlr2 ncost (hd @ tal_base_not_return ??? I2' (or_intror ?? J2') ?))}
     509      %[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (hd @ tal_base_not_return ??? I2' (or_intror ?? J2') ?))}
    502510      [3: % [ /2 by conj/ ]
    503         %[|%[|%[|%[| %2 %[|%[|%[|%[|%[|%[|%[| %{S} % [%] @taa_append_tal_rel /2 by tal_collapsable_to_rel/
    504         ]]]]]]]]]]]
     511        %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [%] @taa_append_tal_rel /2 by tal_collapsable_to_rel/
     512        ]]]]]]]]]]
    505513      ]]
    506514    ]
     
    545553  flat_trace S start st2 stack
    546554| ft_advance_call :
    547   ∀st1,st2,stack,f.flat_trace S start st1 stack → as_execute S st1 st2 →
    548   as_classifier ? st1 (cl_call f) →
    549   flat_trace S start st2 (f :: stack)
     555  ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 →
     556  ∀prf : as_classifier ? st1 cl_call.
     557  flat_trace S start st2 (as_call_ident ? «st1, prf» :: stack)
    550558| ft_advance_ret :
    551559  ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
     
    597605  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
    598606  ft_observables_aux (add @ acc) … pre1
    599 | ft_advance_call st1_mid st1' stack f pre1 _ _
     607| ft_advance_call st1_mid st1' stack pre1 _ prf
    600608  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
    601   let add ≝ add @ [IEVcall f] in
     609  let add ≝ add @ [IEVcall (as_call_ident ? «st1_mid, prf»)] in
    602610  ft_observables_aux (add @ acc) … pre1
    603611| ft_advance_ret st1_mid st1' stack f pre1 _ _ ⇒
     
    613621#acc #S #st1 #st2 #stack #ft lapply acc -acc elim ft -st2 -stack
    614622[ // ]
    615 #st2 #st3 [2,3: #f ] #stack #pre #H #G #IH #acc
     623#st2 #st3 #stack [3: #f ] #pre #H #G #IH #acc
    616624whd in ⊢ (??%(??%?));
    617625>IH >IH >append_nil //
     
    636644  ∀ft : flat_trace S st1 st2 stack.
    637645  ∀taa : trace_any_any S st2 st3.
    638   ∀f.∀H : as_execute S st3 st4.∀G.
    639   ft_observables … (ft_advance_call … f (ft_extend_taa … ft taa) H G) =
    640     ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l) @ [IEVcall f].
    641 #S #st1 #st2 #stack #st3 #st4 #ft #taa #f #H #G
     646  ∀H : as_execute S st3 st4.∀G.
     647  ft_observables … (ft_advance_call … (ft_extend_taa … ft taa) H G) =
     648  ft_observables … ft @
     649  option_to_list … (!l←as_label … st2;return IEVcost l) @
     650  [IEVcall (as_call_ident … «st3, G»)].
     651#S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G
    642652whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
    643653>ft_extend_taa_obs
    644 lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
    645 [ #st2 * #ft #H >append_nil %
    646 | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
     654lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
     655[ #st2 * #ft #H #G >append_nil %
     656| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G
    647657  whd in match (as_label ? st3); >(not_costed_no_label … K)
    648658  normalize nodelta //
     
    727737#S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #H #G elim ft1 -st1' -stack
    728738[ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] %
    729 |*: #st1_mid #st1' #stack [2,3: #f] #ft1 #ex [3: *] #cl
     739|*: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: *] #cl
    730740  (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S
    731741  elim (sim_execute … ex G' cl)
     
    759769      >S >L' %
    760770    ]
    761   |3: (* call *)
    762     * #st2_pre_call #cl' * #_ * #st2_after_call * #st2'
    763     * #taa2 * #taa2' ** #ex' #G'' #H''
    764     %{st2_after_call} %{st2'}
    765     %[@(ft_advance_call … ex' cl')
    766       @(ft_extend_taa … (taa_append_taa … taa taa2))
    767       assumption]
    768     %{taa2'}
    769     % [ %{H'' G''} ]
    770     >ft_extend_taa_advance_call_obs
    771     whd in ⊢ (??%?);
    772     >ft_observables_aux_def >append_nil
    773     >S >L' %
    774   |4: (* ret *)
     771  |3: (* ret *)
    775772    #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
    776773    ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'}
     
    792789    ]
    793790    >S >L' %
    794   ]
    795 ]
    796 qed.
     791  |4: (* call *)
     792    * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2'
     793    * #taa2 * #taa2' ** #ex' #G'' #H''
     794    %{st2_after_call} %{st2'}
     795    lapply (refl_jmeq … (ft_advance_call … ft1 ex cl))
     796    generalize in match (ft_advance_call … ft1 ex cl) in ⊢ (????%→%);
     797    <EQcall in ⊢ (%→???%%→%);
     798    #ft1' #EQft1'
     799    %[@(ft_advance_call … ex' cl')
     800      @(ft_extend_taa … (taa_append_taa … taa taa2))
     801      assumption]
     802    %{taa2'}
     803    % [ %{H'' G''} ]
     804    >ft_extend_taa_advance_call_obs
     805    lapply EQft1' lapply ft1' -ft1'
     806    >EQcall in ⊢ (%→???%%→%);
     807    #ft1' #EQft1' destruct (EQft1')
     808    whd in ⊢ (??%?);
     809    >ft_observables_aux_def >append_nil
     810    >S >L' %
     811  ]
     812]
     813qed.
Note: See TracChangeset for help on using the changeset viewer.