Changeset 2421


Ignore:
Timestamp:
Oct 30, 2012, 4:18:20 PM (7 years ago)
Author:
tranquil
Message:

added simulation of flat prefix, and comments to explain the code

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2413 r2421  
    1515include "common/StructuredTraces.ma".
    1616
     17(* We work with two relations on states in parallel, as well as two derived ones.
     18   sem_rel is the classic semantic relation between states, keeping track of
     19   memory and how program counters are mapped between languages.
     20   call_rel keeps track of what pcs corresponding calls have and just that:
     21   this is different than corresponance between program counters in sem_rel when
     22   CALL f ↦ instr* CALL f instr* *)
     23
    1724record status_rel
    1825  (S1 : abstract_status)
     
    2431     necessary for as_after_return (typically just the program counter)
    2532     maybe what function is called too? *)
    26   ; call_rel : (Σs.∃f.as_classifier S1 s (cl_call f)) →
    27                (Σs.∃f.as_classifier S2 s (cl_call f)) → Prop
     33  ; call_rel : ∀f.(Σs.as_classifier S1 s (cl_call f)) →
     34                  (Σs.as_classifier S2 s (cl_call f)) → Prop
    2835  ; sim_final :
    2936    ∀st1,st2.sem_rel st1 st2 → as_final … st1 ↔ as_final … st2
    3037  }.
    3138
    32 (* if we later genralise, we should move this inside status_rel *)
     39(* The two derived relations are
     40   label_rel which tells that the two states are colabelled
     41   ret_rel which tells that two return states are in relation: the idea is that
     42   it happens when "going back" through as_after_return on one side we get
     43   a pair of call_rel related states, then we enjoy as_after_return also on the
     44   other. Roughly call_rel will store just enough information so that we can
     45   advance locally on a return step and build structured traces any way *)
     46
     47(* if we later generalise, we should move this inside status_rel *)
    3348definition label_rel ≝ λS1,S2,st1,st2.as_label S1 st1 = as_label S2 st2.
    3449
    3550definition ret_rel ≝ λS1,S2.λR : status_rel S1 S2.λs1,s2.
    36   ∀s1_pre,s2_pre.as_after_return S1 s1_pre s1 → call_rel … R s1_pre s2_pre →
    37                  as_after_return S2 s2_pre s2.
    38 
    39 (* the equivalent of a collapsable trace_any_label where we do not forse
     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.
     54
     55(* the equivalent of a collapsable trace_any_label where we do not force
    4056   costedness of the lookahead status *)
    4157inductive trace_any_any_free (S : abstract_status) : S → S → Type[0] ≝
     
    5167].
    5268
    53 (* notice: labels and semantic relation between states are not in sync *)
     69(* the base property we ask for simulation to work depends on the status_class
     70   S will mark semantic relation, C call relation, L label relation, R return relation *)
     71
    5472record status_simulation
    5573  (S1 : abstract_status)
     
    6078    ∀st1,st1',c,st2.as_execute S1 st1 st1' →
    6179    sim_status_rel st1 st2 →
    62     ∀prf : as_classifier S1 st1 c. (* <-- watch out, different from status_simulation *)
     80    ∀prf : as_classifier S1 st1 c.
    6381    match c return λc.as_classifier S1 st1 c → ? with
    64     [ cl_call _ ⇒ λprf.
    65       ∃st2_pre_call.call_rel ?? sim_status_rel «st1, ex_intro … prf» st2_pre_call ∧
     82    [ cl_call f ⇒ λprf.
     83      (*
     84           st1' ------------S----------\
     85            ↑ \                         \
     86           st1 \--L--\                   \
     87            | \       \                   \
     88            S  \-C-\  st2_after_call →taa→ st2'
     89            |       \     ↑
     90           st2 →taa→ st2_pre_call
     91      *)
     92      ∃st2_pre_call.call_rel ?? sim_status_rel f «st1, prf» st2_pre_call ∧
    6693      ∃st2_after_call,st2'.
    6794      ∃taa2 : trace_any_any … st2 st2_pre_call.
     
    7198      label_rel … st1' st2_after_call
    7299    | cl_return ⇒ λ_.
     100      (*
     101           st1
     102          / ↓
     103         | st1'----------S,L------------\
     104         S   \                           \
     105          \   \-----R-------\            |     
     106           \                 |           |
     107           st2 →taa→ st2_ret |           |
     108                        ↓   /            |
     109                   st2_after_ret →taaf→ st2'
     110
     111         we also ask that st2_after_ret be not labelled if the taaf tail is
     112         not empty
     113      *)
    73114      ∃st2_ret,st2_after_ret,st2'.
    74115      ∃taa2 : trace_any_any … st2 st2_ret.
    75116      ∃taa2' : trace_any_any_free … st2_after_ret st2'.
    76117      (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
    77       as_classifier … st2_ret cl_return (* is it really important? *)
     118      as_classifier … st2_ret cl_return
    78119      as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
    79120      ret_rel … sim_status_rel st1' st2_after_ret ∧
    80121      label_rel … st1' st2'
    81122    | _ ⇒ λ_.
    82       (* this allows to freely exchange cl_other and cl_jump,
     123      (*
     124         st1 → st1'
     125          |      \
     126          S      S,L
     127          |        \
     128         st2 →taaf→ st2'
     129         
     130         the taaf can be empty (e.g. tunneling) but we ask it must not be the
     131         case when both st1 and st1' are labelled (we would be able to collapse
     132         labels otherwise)
     133         also notice that this allows to freely exchange cl_other and cl_jump,
    83134         but if cl_jump imposed labels before, they will be kept afterwards *)
    84135      ∃st2'.
    85136      ∃taa2 : trace_any_any_free … st2 st2'.
    86137      (* we ensure no labels are collapsed. Technicality? *)
    87       (if taaf_non_empty … taa2 then True else ¬as_costed … st1) ∧
     138      (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
    88139      sim_status_rel st1' st2' ∧
    89140      label_rel … st1' st2'
    90141    ] prf
    91142  }.
     143
     144
     145(* some useful lemmas *)
    92146
    93147let rec taa_append_taa S st1 st2 st3
     
    174228qed.
    175229
     230lemma taa_end_not_costed : ∀S,s1,s2.∀taa : trace_any_any S s1 s2.
     231  if taa_non_empty … taa then ¬as_costed … s2 else True.
     232#S #s1 #s2 #taa elim taa -s1 -s2 normalize nodelta
     233[ #s1 %
     234| #s1 #s2 #s3 #H #G #K #tl lapply K lapply H cases tl -s2 -s3
     235  [ #s2 #H #K #_ assumption
     236  | #s2 #s3 #s4 #H' #G' #K' #tl' #H #K #I @I
     237  ]
     238]
     239qed.
     240
    176241let rec tal_collapsable_to_rel S fl st1 st2
    177242  (tal : trace_any_label S fl st1 st2) on tal :
     
    215280
    216281let rec status_simulation_produce_tlr S1 S2 (R : status_simulation S1 S2)
     282(* we start from this situation
     283     st1 →→→→tlr→→→→ st1'
     284      | \
     285      L  \---S--\
     286      |          \
     287   st2_lab →taa→ st2   (the taa preamble is in general either empty or given
     288                        by the preceding call)
     289   
     290   and we produce
     291     st1 →→→→tlr→→→→ st1'
     292             \\      /  \
     293             //     R    \-L,S-\
     294             \\     |           \
     295   st2_lab →tlr→ st2_mid →taaf→ st2'
     296*)
    217297  st1 st1' st2_lab st2
    218298  (tlr1 : trace_label_return S1 st1 st1')
     
    230310 ]
    231311and status_simulation_produce_tll S1 S2 (R : status_simulation S1 S2)
     312(* we start from this situation
     313     st1 →→→→tll→→→ st1'
     314      | \
     315      L  \---S--\
     316      |          \
     317   st2_lab →taa→ st2
     318   
     319   and if the tll is a returning one we produce a diagram like the one for tlr,
     320   otherwise a simpler:
     321     st1 →→→→tll→→→→ st1'
     322             \\       |
     323             //      L,S
     324             \\       |
     325   st2_lab →→→tll→→→ st2'
     326*)
    232327  fl st1 st1' st2_lab st2
    233328  (tll1 : trace_label_label S1 fl st1 st1')
     
    250345  ]
    251346and status_simulation_produce_tal S1 S2 (R : status_simulation S1 S2)
     347(* we start from this situation
     348     st1 →→tal→→ st1'
     349      |
     350      S
     351      |
     352     st2
     353   
     354   and if the tal is a returning one we produce a diagram like the one for tlr,
     355   otherwise we allow for two possibilities:
     356   either
     357
     358     st1 →→tal→→ st1'
     359            \\    |
     360            //   L,S
     361            \\    |
     362     st2 →→tal→→ st2'
     363
     364   or we do not advance from st2:
     365
     366     st1 →→tal→→ st1'  collapsable, and st1 uncosted
     367                /
     368         /-L,S-/
     369        /
     370     st2
     371*)
    252372  fl st1 st1' st2
    253373  (tal1 : trace_any_label S1 fl st1 st1')
     
    306426  #st2' ** -st2 -st2'
    307427  [1,3: #st2 (* taa2 empty → st1' must be not cost_labelled *)
    308     ** whd in ⊢ (%→?); #ncost #R' #L' %2 /4 by conj/
     428    ** whd in ⊢ (%→?); *
     429    [1,3: #ncost #R' #L' %2 /4 by conj/
     430    |*: * #ABS elim (ABS K)
     431    ]
    309432  |*: #st2 #st2_mid #st2' #taa2 #H2 #I2 *** #st1_R_st2' #st1_L_st2' %1
    310433    %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 (or_intror ?? I2) ?))}
     
    323446| (* tal_base_call *) whd
    324447  elim (sim_execute … R … H st1_R_st2 G)
    325   * #st2_pre_call * #f #G2 * #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
     448  * #st2_pre_call #G2 * #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
    326449  #st1_R_st2_mid #st1_L_st2_after_call
    327450  elim (status_simulation_produce_tlr ?? R ???? tlr1 taa2' st1_R_st2_mid st1_L_st2_after_call)
     
    348471| (* tal_step_call *)
    349472  elim (sim_execute … R … H st1_R_st2 G)
    350   * #st2_pre_call * #f #G2 * #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
     473  * #st2_pre_call #G2 * #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
    351474  #st1_R_st2_mid #st1_L_st2_after_call
    352475  elim (status_simulation_produce_tlr ?? R ???? tlr1 taa2' st1_R_st2_mid st1_L_st2_after_call)
     
    393516| (* step_default *)
    394517  elim (sim_execute … R … H st1_R_st2 G)
    395   #st2_mid *#taa2 ** #cost #st1_R_st2_mid #st1_L_st2_mid
     518  #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid
    396519  lapply (status_simulation_produce_tal … tl1 st1_R_st2_mid)
    397520  cases fl1' in tl1; #tl1 *
     
    404527      [2: % [/2 by conj/] @taaf_append_tal_rel @G ]
    405528    ]
    406   | lapply st1_L_st2_mid lapply st1_R_st2_mid lapply cost
    407     cases taa2 -st2_mid -st2
    408     [ #st2 #cost #_ #_ *#H #G %2 %{H cost} ]
    409     #st2 #st2_mid' #st2_mid #hd #H2 #I2 * #st1_R_st2_mid #st1_L_st2_mid
    410     *** #H #G #K #L %1
    411     %[| %{(hd @ tal_base_not_return ??? H2 (or_intror ?? I2) ?)}
    412     [2: % [/2 by conj/] @taa_append_tal_rel @tal_collapsable_to_rel assumption
    413     |1: whd <G @(tal_end_costed … tl1)
    414     ]]
     529  | (* can't happen *)
     530    *** #_ #L' elim (absurd ?? K)
     531    whd >st1_L_st2_mid <L' @(tal_end_costed … tl1)
    415532  ]
    416533  @if_else_True whd in ⊢ (?%); <st1_L_st2_mid assumption
    417534]
    418535qed.
     536
     537(* finite flat traces, with recursive structure right to left. The list of
     538   identifiers represents the call stack *)
     539
     540inductive flat_trace (S : abstract_status) (start : S) : S → list ident → Type[0] ≝
     541| ft_start : flat_trace S start start [ ]
     542| ft_advance_flat :
     543  ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 →
     544  (as_classifier ? st1 cl_jump ∨ as_classifier ? st1 cl_other) →
     545  flat_trace S start st2 stack
     546| 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)
     550| ft_advance_ret :
     551  ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
     552  as_classifier ? st1 cl_return →
     553  flat_trace S start st2 stack.
     554
     555let rec ft_extend_taa S st1 st2 stack st3 (ft : flat_trace S st1 st2 stack)
     556  (taa : trace_any_any S st2 st3)
     557on taa : flat_trace S st1 st3 stack ≝
     558match taa return λst2,st3,taa.flat_trace ?? st2 ? → flat_trace ?? st3 ? with
     559[ taa_base s ⇒ λacc.acc
     560| taa_step st1 st2 st3 H G _ tl ⇒
     561  λacc.ft_extend_taa ????? (ft_advance_flat ????? acc H (or_intror … G)) tl
     562] ft.
     563
     564lemma ft_extend_extend_taa : ∀S,st1,st2,stack,st3,st4,ft,taa1,taa2.
     565  ft_extend_taa S st1 st3 stack st4 (ft_extend_taa ?? st2 ?? ft taa1) taa2 =
     566  ft_extend_taa … ft (taa_append_taa … taa1 taa2).
     567#S #st1 #st2 #stack #st3 #st4 #ft #taa1 lapply ft elim taa1 -st2 -st3 normalize
     568/2/
     569qed.
     570
     571definition ft_extend_taaf ≝ λS,st1,st2,stack,st3.λft : flat_trace S st1 st2 stack.
     572  λtaaf : trace_any_any_free S st2 st3.
     573  match taaf return λst2,st3,taaf.flat_trace ?? st2 ? → flat_trace ?? st3 ? with
     574  [ taaf_base s ⇒ λft.ft
     575  | taaf_step s1 s2 s3 pre H G ⇒
     576    λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_intror … G)
     577  ] ft.
     578
     579definition option_to_list : ∀A.option A → list A ≝ λA,x.
     580  match x with
     581  [ Some x ⇒ [x]
     582  | None ⇒ [ ]
     583  ].
     584
     585(* the observables of a flat trace (for the moment, only labels, calls and returns) *)
     586
     587inductive intensional_event : Type[0] ≝
     588| IEVcost : costlabel → intensional_event
     589| IEVcall : ident → intensional_event
     590| IEVret : ident → intensional_event.
     591
     592let rec ft_observables_aux acc S st st' stack
     593  (ft : flat_trace S st st' stack) on ft : list intensional_event ≝
     594match ft with
     595[ ft_start ⇒ acc
     596| ft_advance_flat st1_mid st1' stack pre1 _ _ ⇒
     597  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
     598  ft_observables_aux (add @ acc) … pre1
     599| ft_advance_call st1_mid st1' stack f pre1 _ _ ⇒
     600  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
     601  let add ≝ add @ [IEVcall f] in
     602  ft_observables_aux (add @ acc) … pre1
     603| ft_advance_ret st1_mid st1' stack f pre1 _ _ ⇒
     604  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
     605  let add ≝ add @ [IEVret f] in
     606  ft_observables_aux (add @ acc) … pre1
     607].
     608
     609definition ft_observables ≝ ft_observables_aux [ ].
     610
     611lemma ft_observables_aux_def : ∀acc,S,st1,st2,stack,ft.
     612  ft_observables_aux acc S st1 st2 stack ft = ft_observables … ft @ acc.
     613#acc #S #st1 #st2 #stack #ft lapply acc -acc elim ft -st2 -stack
     614[ // ]
     615#st2 #st3 [2,3: #f ] #stack #pre #H #G #IH #acc
     616whd in ⊢ (??%(??%?));
     617>IH >IH >append_nil //
     618qed.
     619
     620lemma ft_extend_taa_obs : ∀S,st1,st2,stack,st3,ft,taa.
     621  ft_observables … (ft_extend_taa S st1 st2 stack st3 ft taa) =
     622    ft_observables … ft @
     623    if taa then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ].
     624#S #st1 #st2 #stack #st3 #ft #taa lapply ft elim taa -st2 -st3
     625[ #st2 #ft >append_nil % ]
     626#st2 #st3 #st4 #H #K #G #taa #IH #ft
     627normalize in ⊢ (??(?????%)?); >IH
     628-IH lapply G lapply H cases taa -st3 -st4 normalize nodelta
     629[ #st3 #H #G
     630| #st3 #st4 #st5 #ex #H' #G' #taa #H #G
     631  whd in match (as_label ? st3); >(not_costed_no_label … G)
     632] >append_nil whd in ⊢ (??%?); >ft_observables_aux_def >append_nil %
     633qed.
     634
     635lemma ft_extend_taa_advance_call_obs : ∀S,st1,st2,stack,st3,st4.
     636  ∀ft : flat_trace S st1 st2 stack.
     637  ∀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
     642whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
     643>ft_extend_taa_obs
     644lapply 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
     647  whd in match (as_label ? st3); >(not_costed_no_label … K)
     648  normalize nodelta //
     649]
     650qed.
     651
     652lemma ft_extend_taa_advance_ret_obs : ∀S,st1,st2,stack,f,st3,st4.
     653  ∀ft : flat_trace S st1 st2 (f :: stack).
     654  ∀taa : trace_any_any S st2 st3.
     655  ∀H : as_execute S st3 st4.∀G.
     656  ft_observables … (ft_advance_ret … (ft_extend_taa … ft taa) H G) =
     657    ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l) @ [IEVret f].
     658#S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G
     659whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
     660>ft_extend_taa_obs
     661lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
     662[ #st2 * #ft #H >append_nil %
     663| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
     664  whd in match (as_label ? st3); >(not_costed_no_label … K)
     665  normalize nodelta //
     666]
     667qed.
     668
     669lemma ft_extend_taa_advance_flat_obs : ∀S,st1,st2,stack,st3,st4.
     670  ∀ft : flat_trace S st1 st2 stack.
     671  ∀taa : trace_any_any S st2 st3.
     672  ∀H : as_execute S st3 st4.∀G.
     673  ft_observables … (ft_advance_flat … (ft_extend_taa … ft taa) H G) =
     674    ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l).
     675#S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G
     676whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
     677>ft_extend_taa_obs
     678lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
     679[ #st2 * #ft #H >append_nil %
     680| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
     681  whd in match (as_label ? st3); >(not_costed_no_label … K)
     682  normalize nodelta >append_nil //
     683]
     684qed.
     685
     686lemma ft_extend_taaf_obs : ∀S,st1,st2,stack,st3,ft,taaf.
     687  ft_observables … (ft_extend_taaf S st1 st2 stack st3 ft taaf) =
     688    ft_observables … ft @
     689    if taaf_non_empty … taaf then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ].
     690#S #st1 #st2 #stack #st3 #ft #taa lapply ft cases taa -st2 -st3
     691[ #st2 #ft >append_nil % ]
     692#st2 #st3 #st4 #taa #H normalize nodelta #G #ft
     693@ft_extend_taa_advance_flat_obs
     694qed.
     695
     696(* little helper to avoid splitting equal cases *)
     697lemma if_eq : ∀b,A.∀x : A.if b then x else x = x. * // qed-.
     698
     699theorem status_simulation_produce_ft :
     700(* from
     701
     702  st1 →→→ft→→→ st1'
     703   |
     704  R,L
     705   |
     706  st2
     707
     708  we produce
     709 
     710  st1 →→→ft→→→ st1'-------\
     711         //      \         \
     712         \\       L         S
     713         //       |          \
     714  st2 →→→ft→→→ st2_lab →taa→ st2'
     715 
     716  so that from any tlr or tll following st1' we can produce the corresponding
     717  structured trace from st2_lab using the previous result
     718*)
     719  ∀S1,S2.
     720  ∀R : status_simulation S1 S2.
     721  ∀st1,st1',stack,st2.∀ft1 : flat_trace S1 st1 st1' stack.
     722  label_rel … st1 st2 → R st1 st2 →
     723  ∃st2_lab,st2'.
     724  ∃ft2 : flat_trace S2 st2 st2_lab stack.
     725  ∃taa : trace_any_any S2 st2_lab st2'.
     726  label_rel … st1' st2_lab ∧ R st1' st2' ∧ ft_observables … ft1 = ft_observables … ft2.
     727#S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #H #G elim ft1 -st1' -stack
     728[ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] %
     729|*: #st1_mid #st1' #stack [2,3: #f] #ft1 #ex [3: *] #cl
     730  (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S
     731  elim (sim_execute … ex G' cl)
     732  [1,2: (* jump or other *)
     733    #st2' *#taaf ** #ncost #G'' #H''
     734    %{st2'} %{st2'}
     735    %[1,3:
     736      @(ft_extend_taaf … taaf)
     737      @(ft_extend_taa … taa)
     738      assumption]
     739    %{(taa_base …)}
     740    % [1,3: %{H'' G''} ]
     741    whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
     742    lapply ncost lapply taa lapply H'' cases taaf -st2_mid -st2'
     743    [1,3: #st2' #H'' #taa * #ncost
     744      >ft_extend_taa_obs <L'
     745      [1,3: whd in match (as_label ? st1_mid);
     746        >(not_costed_no_label … ncost) >if_eq >S %
     747      |*: lapply L' lapply H'' lapply S lapply ft2 cases taa -st2_lab -st2'
     748        [1,3: #st2' #ft2 #S #H'' #L' >append_nil
     749          whd in match (as_label ??); >not_costed_no_label
     750          [1,3: >append_nil @S ]
     751          whd in ⊢ (?%); >L' <H'' assumption
     752        |*: normalize nodelta #st2_mid #st2_mid' #st2' #_ #_ #_ #taa #ft2 #S #_ #_
     753          >S %
     754        ]
     755      ]
     756    |*: #st2_mid #st2_mid' #st2' #taa' #ex' #cl' #_ #taa *
     757      whd in ⊢ (???(?????%));
     758      >ft_extend_extend_taa >ft_extend_taa_advance_flat_obs
     759      >S >L' %
     760    ]
     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 *)
     775    #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
     776    ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'}
     777    %[@(ft_extend_taaf … taa2')
     778      @(ft_advance_ret … f … ex' cl')
     779      @(ft_extend_taa … (taa_append_taa … taa taa2))
     780      assumption]
     781    %{(taa_base …)}
     782    % [ %{H'' G''} ]
     783    >ft_extend_taaf_obs
     784    >ft_extend_taa_advance_ret_obs
     785    whd in ⊢ (??%?);
     786    >ft_observables_aux_def >append_nil
     787    lapply ncost cases taa2' -st2_after_ret -st2'
     788    [ #st2' * >append_nil
     789    | #st2_after_ret #st2_after_ret' #st2' #taa2' #ex'' #cl'' #ncost
     790      whd in match (as_label ? st2_after_ret); >(not_costed_no_label … ncost)
     791      >if_eq >append_nil
     792    ]
     793    >S >L' %
     794  ]
     795]
     796qed.
Note: See TracChangeset for help on using the changeset viewer.