Changeset 3096 for src/common


Ignore:
Timestamp:
Apr 5, 2013, 6:04:14 PM (7 years ago)
Author:
tranquil
Message:

preliminary work on closing correctness.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2991 r3096  
    3333  ; call_rel : (Σs.as_classifier S1 s cl_call) →
    3434               (Σs.as_classifier S2 s cl_call) → Prop
    35   ; sim_final :
    36     ∀st1,st2.sem_rel st1 st2 → as_final … st1 ↔ as_final … st2
    3735  }.
    3836
     
    5755   S will mark semantic relation, C call relation, L label relation, R return relation *)
    5856
    59 definition status_simulation ≝
    60   λS1 : abstract_status.
    61   λS2 : abstract_status.
    62   λsim_status_rel : status_rel S1 S2.
     57record status_simulation
     58  (S1, S2 : abstract_status)
     59  (sim_status_rel : status_rel S1 S2) : Prop ≝
     60{ one_step_sim :5>
    6361    ∀st1,st1',st2.as_execute S1 st1 st1' →
    6462    sim_status_rel st1 st2 →
     
    149147        sim_status_rel st1' st2' ∧
    150148        label_rel … st1' st2'
    151     ].
    152 
     149    ]
     150; sim_final :
     151  ∀st1,st2,res.as_result S1 st1 = Some ? res → sim_status_rel st1 st2 →
     152  as_result S2 st2 = Some ? res
     153}.
     154
     155record status_simulation_with_init (S1,S2 : abstract_status)
     156  (R : status_rel S1 S2)
     157  (init1 : S1) (init2 : S2) : Prop ≝
     158{ sim_init : R init1 init2
     159; sim_init_labels : label_rel … init1 init2
     160; sim_step_final :> status_simulation S1 S2 R
     161}.
    153162
    154163(* some useful lemmas *)
     
    584593qed.
    585594
     595definition is_cl_jump : ∀S : abstract_status.S → bool ≝
     596λS,s.match as_classify … s with [ cl_jump ⇒ true | _ ⇒ false ].
     597
     598definition enforce_costedness : ∀S : abstract_status.S → S → Prop ≝
     599λS,s1,s2.if is_cl_jump … s1 then as_costed … s2 else True.
     600
    586601(* finite flat traces, with recursive structure right to left. The list of
    587602   identifiers represents the call stack *)
    588 
    589 inductive flat_trace (S : abstract_status) (start : S) : S → list ident → Type[0] ≝
    590 | ft_start : flat_trace S start start [ ]
    591 | ft_advance_flat :
    592   ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 →
     603inductive 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(*
    593610  ((as_classifier ? st1 cl_jump ∧ as_costed … st2) ∨ as_classifier ? st1 cl_other) →
    594611  flat_trace S start st2 stack
     
    605622  as_classifier ? st1 cl_return →
    606623  flat_trace S start st2 stack.
    607 
    608 let rec ft_extend_taa S st1 st2 stack st3 (ft : flat_trace S st1 st2 stack)
     624*)
     625
     626let rec ft_extend_taa S st1 st2 st3 (ft : flat_trace S st1 st2)
    609627  (taa : trace_any_any S st2 st3)
    610 on taa : flat_trace S st1 st3 stack
    611 match taa return λst2,st3,taa.flat_trace ?? st2 ? → flat_trace ?? st3 ? with
     628on taa : flat_trace S st1 st3
     629match taa return λst2,st3,taa.flat_trace ?? st2 → flat_trace ?? st3 with
    612630[ taa_base s ⇒ λacc.acc
    613631| taa_step st1 st2 st3 H G _ tl ⇒
    614   λacc.ft_extend_taa ????? (ft_advance_flat ????? acc H (or_intror … G)) tl
     632  λacc.ft_extend_taa ???? (ft_advance ???? acc H ?) tl
    615633] ft.
    616 
    617 lemma ft_extend_extend_taa : ∀S,st1,st2,stack,st3,st4,ft,taa1,taa2.
    618   ft_extend_taa S st1 st3 stack st4 (ft_extend_taa ?? st2 ?? ft taa1) taa2 =
     634@hide_prf whd whd in match is_cl_jump; normalize nodelta >G % qed.
     635
     636lemma 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 =
    619638  ft_extend_taa … ft (taa_append_taa … taa1 taa2).
    620 #S #st1 #st2 #stack #st3 #st4 #ft #taa1 lapply ft elim taa1 -st2 -st3 normalize
     639#S #st1 #st2 #st3 #st4 #ft #taa1 lapply ft elim taa1 -st2 -st3 normalize
    621640/2/
    622641qed.
    623642
    624 definition ft_extend_taaf ≝ λS,st1,st2,stack,st3.λft : flat_trace S st1 st2 stack.
     643definition ft_extend_taaf ≝ λS,st1,st2,st3.λft : flat_trace S st1 st2.
    625644  λtaaf : trace_any_any_free S st2 st3.
    626   match taaf return λst2,st3,taaf.flat_trace ?? st2 ? → flat_trace ?? st3 ? with
     645  match taaf return λst2,st3,taaf.flat_trace ?? st2 → flat_trace ?? st3 with
    627646  [ taaf_base s ⇒ λft.ft
    628647  | taaf_step s1 s2 s3 pre H G ⇒
    629     λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_intror … G)
     648    λft.ft_advance … (ft_extend_taa … ft pre) H ?
    630649  | taaf_step_jump s1 s2 s3 pre H G K ⇒
    631     λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_introl … (conj … G K))
     650    λft.ft_advance … (ft_extend_taa … ft pre) H ?
    632651  ] ft.
     652@hide_prf whd whd in match is_cl_jump; normalize nodelta >G // qed.
    633653
    634654definition option_to_list : ∀A.option A → list A ≝ λA,x.
     
    638658  ].
    639659
     660(*
     661let rec ft_stack S st st' (ft : flat_trace S st st') on ft : list ident ≝
     662match 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
    640688(* the observables of a flat trace (for the moment, only labels, calls and returns) *)
    641 let rec ft_observables_aux acc S st st' stack
    642   (ft : flat_trace S st st' stack) on ft : list intensional_event ≝
     689(* inefficient, but used only in correctness proofs *)
     690let rec ft_stack_observables S st st'
     691  (ft : flat_trace S st st') on ft : list ident × (list intensional_event) ≝
    643692match ft with
    644 [ ft_start ⇒ acc
    645 | ft_advance_flat st1_mid st1' stack pre1 _ _ ⇒
     693[ ft_start ⇒ 〈[ ], [ ]〉
     694| ft_advance st1_mid st1' pre1 _ _ ⇒
     695  let 〈stack, tr〉 ≝ ft_stack_observables … pre1 in
    646696  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
    647   ft_observables_aux (add @ acc) … pre1
    648 | ft_advance_call st1_mid st1' stack pre1 _ prf ⇒
    649   let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
    650   let add ≝ add @ [IEVcall (as_call_ident ? «st1_mid, prf»)] in
    651   ft_observables_aux (add @ acc) … pre1
    652 | ft_advance_tailcall st1_mid st1' stack f pre1 _ prf ⇒
    653   let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
    654   let add ≝ add @ [IEVtailcall f (as_tailcall_ident ? «st1_mid, prf»)] in
    655   ft_observables_aux (add @ acc) … pre1
    656 | ft_advance_ret st1_mid st1' stack f pre1 _ _ ⇒
    657   let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
    658   let add ≝ add @ [IEVret f] in
    659   ft_observables_aux (add @ acc) … pre1
     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 …)
    660721].
    661722
    662 definition ft_observables ≝ ft_observables_aux [ ].
    663 
    664 lemma ft_observables_aux_def : ∀acc,S,st1,st2,stack,ft.
    665   ft_observables_aux acc S st1 st2 stack ft = ft_observables … ft @ acc.
    666 #acc #S #st1 #st2 #stack #ft lapply acc -acc elim ft -st2 -stack
    667 [ // ]
    668 #st2 #st3 #stack [3,4: #f ] #pre #H #G #IH #acc
    669 whd in ⊢ (??%(??%?));
    670 >IH >IH >append_nil //
    671 qed.
    672 
    673 lemma ft_extend_taa_obs : ∀S,st1,st2,stack,st3,ft,taa.
    674   ft_observables … (ft_extend_taa S st1 st2 stack st3 ft taa) =
    675     ft_observables … ft @
    676     if taa then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ].
    677 #S #st1 #st2 #stack #st3 #ft #taa lapply ft elim taa -st2 -st3
    678 [ #st2 #ft >append_nil % ]
     723definition ft_observables ≝ λS,st1,st2,ft.\snd (ft_stack_observables S st1 st2 ft).
     724definition ft_stack ≝ λS,st1,st2,ft.\fst (ft_stack_observables S st1 st2 ft).
     725
     726definition ft_current_function : ∀S,st1,st2.flat_trace S st1 st2 → option ident ≝
     727λS,st1,st2,ft.
     728match ft_stack … ft with [ nil ⇒ None ? | cons hd _ ⇒ Some ? hd ].
     729
     730lemma 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)) →
     738P (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
     747lemma 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'.
     752match 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 …) =
     759match 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
     768lemma 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
     775lemma 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 ]
    679781#st2 #st3 #st4 #H #K #G #taa #IH #ft
    680 normalize in ⊢ (??(?????%)?); >IH
     782whd in ⊢ (??(????%)?); >IH normalize nodelta
    681783-IH lapply G lapply H cases taa -st3 -st4 normalize nodelta
    682784[ #st3 #H #G
    683785| #st3 #st4 #st5 #ex #H' #G' #taa #H #G
    684786  >(not_costed_no_label … G)
    685 ] >append_nil whd in ⊢ (??%?); >ft_observables_aux_def >append_nil %
    686 qed.
    687 
    688 lemma ft_extend_taa_advance_call_obs : ∀S,st1,st2,stack,st3,st4.
    689   ∀ft : flat_trace S st1 st2 stack.
     787]
     788>append_nil whd in ⊢ (??(???%%)(????(??%?)));
     789whd in match (ft_stack_observables ????) ;
     790@(pair_elim' … (ft_stack_observables … ft))
     791>(status_class_dep_match_rewrite … K) %
     792qed.
     793
     794lemma ft_extend_taa_advance_obs : ∀S,st1,st2,st3,st4.
     795  ∀ft : flat_trace S st1 st2.
    690796  ∀taa : trace_any_any S st2 st3.
    691797  ∀H : as_execute S st3 st4.∀G.
    692   ft_observables … (ft_advance_call … (ft_extend_taa … ft taa) H G) =
    693   ft_observables … ft @
    694   option_to_list … (!l←as_label … st2;return IEVcost l) @
    695   [IEVcall (as_call_ident … «st3, G»)].
    696 #S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G
    697 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
    698 >ft_extend_taa_obs
    699 lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
    700 [ #st2 * #ft #H #G >append_nil %
    701 | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G
    702   >(not_costed_no_label … K)
    703   normalize nodelta //
    704 ]
    705 qed.
    706 
    707 lemma ft_extend_taa_advance_tailcall_obs : ∀S,st1,st2,stack,f,st3,st4.
    708   ∀ft : flat_trace S st1 st2 (f :: stack).
    709   ∀taa : trace_any_any S st2 st3.
     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
     826whd in ⊢ (??%?); @pair_elim' @pair_elim' normalize nodelta
     827@status_class_dep_match_elim #prf
     828@status_class_dep_match_elim #prf'
     829try(@⊥ >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
     833lapply prf lapply prf' lapply (taa_end_not_costed … taa)
     834cases 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 %
     838qed.
     839
     840lemma 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
     848whd in match ft_extend_taaf; normalize nodelta
     849>ft_extend_taa_advance_obs @pair_elim'
     850>(status_class_dep_match_rewrite … G) %
     851qed.
     852
     853(*
     854lemma 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.
    710857  ∀H : as_execute S st3 st4.∀G.
    711   ft_observables … (ft_advance_tailcall … (ft_extend_taa … ft taa) H G) =
    712   ft_observables … ft @
    713   option_to_list … (!l←as_label … st2;return IEVcost l) @
    714   [IEVtailcall f (as_tailcall_ident … «st3, G»)].
    715 #S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G
    716 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
    717 >ft_extend_taa_obs
    718 lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
    719 [ #st2 * #ft #H #G >append_nil %
    720 | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G
    721   >(not_costed_no_label … K)
    722   normalize nodelta //
    723 ]
    724 qed.
    725 
    726 lemma ft_extend_taa_advance_ret_obs : ∀S,st1,st2,stack,f,st3,st4.
    727   ∀ft : flat_trace S st1 st2 (f :: stack).
    728   ∀taa : trace_any_any S st2 st3.
    729   ∀H : as_execute S st3 st4.∀G.
    730   ft_observables … (ft_advance_ret … (ft_extend_taa … ft taa) H G) =
    731     ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l) @ [IEVret f].
    732 #S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G
    733 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
    734 >ft_extend_taa_obs
    735 lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
    736 [ #st2 * #ft #H >append_nil %
    737 | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
    738   >(not_costed_no_label … K)
    739   normalize nodelta //
    740 ]
    741 qed.
    742 
    743 lemma ft_extend_taa_advance_flat_obs : ∀S,st1,st2,stack,st3,st4.
    744   ∀ft : flat_trace S st1 st2 stack.
    745   ∀taa : trace_any_any S st2 st3.
    746   ∀H : as_execute S st3 st4.∀G.
    747   ft_observables … (ft_advance_flat … (ft_extend_taa … ft taa) H G) =
    748     ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l).
    749 #S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G
    750 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
    751 >ft_extend_taa_obs
    752 lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
    753 [ #st2 * #ft #H >append_nil %
    754 | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
    755   >(not_costed_no_label … K)
    756   normalize nodelta >append_nil //
    757 ]
    758 qed.
    759 
    760 lemma ft_extend_taaf_obs : ∀S,st1,st2,stack,st3,ft,taaf.
    761   ft_observables … (ft_extend_taaf S st1 st2 stack st3 ft taaf) =
    762     ft_observables … ft @
    763     if taaf_non_empty … taaf then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ].
    764 #S #st1 #st2 #stack #st3 #ft #taa lapply ft cases taa -st2 -st3
    765 [ #st2 #ft >append_nil % ]
    766 #st2 #st3 #st4 #taa #H normalize nodelta #G [2: #K ] #ft
    767 @ft_extend_taa_advance_flat_obs
    768 qed.
     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
     886whd 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
     889whd 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'
     894try(@⊥ >prf in prf'; #prf' -prf destruct @False)
     895[ >associative_append
     896whd 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
     899lapply prf lapply prf' lapply G
     900cases 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 %
     904qed.
     905*)
    769906
    770907(* little helper to avoid splitting equal cases *)
    771908lemma if_eq : ∀b,A.∀x : A.if b then x else x = x. * // qed-.
     909
     910lemma enforce_costedness_ok : ∀S,s1,s2.enforce_costedness S s1 s2 →
     911as_classifier S s1 cl_jump → as_costed … s2.
     912#S #s1 #s2 whd in ⊢ (%→%→?); whd in match (is_cl_jump ??); #H #G >G in H; #K @K qed.
     913
     914let rec taa_to_taaf S st1 st2 (taa : trace_any_any S st1 st2) on taa :
     915  trace_any_any_free S st1 st2 ≝
     916match taa return λst1,st2,taa.trace_any_any_free S st1 st2 with
     917[ taa_base s ⇒ taaf_base … s
     918| taa_step s1 s2 s3 ex cl ncost tl ⇒
     919  taaf_cons … ex cl (taa_to_taaf … tl) ?
     920]. @if_else_True assumption qed.
     921
     922definition taa_append_taaf : ∀S,st1,st2,st3.
     923  trace_any_any S st1 st2 → trace_any_any_free S st2 st3 →
     924  trace_any_any_free S st1 st3 ≝
     925λS,st1,st2,st3,taa,taaf.
     926match taaf return λst2,st3,taaf.trace_any_any S st1 st2 → trace_any_any_free S st1 st3 with
     927[ taaf_base s ⇒ taa_to_taaf …
     928| taaf_step s1 s2 s3 taa' ex cl ⇒
     929  λtaa.taaf_step … (taa_append_taa … taa taa') ex cl
     930| taaf_step_jump s1 s2 s3 taa' ex cl K ⇒
     931  λtaa.taaf_step_jump … (taa_append_taa … taa taa') ex cl K
     932] taa.
     933
     934lemma taa_to_taaf_non_empty : ∀S,st1,st2,taa.
     935taaf_non_empty … (taa_to_taaf S st1 st2 taa) = taa_non_empty … taa.
     936#S #st1 #st2 #taa elim taa -st1 -st2
     937[ #s % | #s1 #s2 #s3 #ex #cl #ncost #tl #IH
     938  change with (taaf_cons ????????) in match (taa_to_taaf ????);
     939  >taaf_cons_non_empty %
     940qed.
     941
     942lemma taa_append_taaf_non_empty : ∀S,st1,st2,st3,taa,taaf.
     943taaf_non_empty … (taa_append_taaf S st1 st2 st3 taa taaf) =
     944(taa_non_empty … taa ∨ taaf_non_empty … taaf).
     945#S #st1 #st2 #st3 #taa #taaf lapply taa cases taaf -st2 -st3
     946[ #s #taa whd in match (taa_append_taaf ??????); >taa_to_taaf_non_empty
     947  >commutative_orb %
     948|*: #s1 #s2 #s3 #taa' #ex #cl [2: #K] #taa >commutative_orb %
     949]
     950qed.
     951
     952lemma taa_empty_to_eq : ∀S,st1,st2,taa.
     953¬(bool_to_Prop (taa_non_empty S st1 st2 taa)) → st1 = st2.
     954#S #st1 #st2 * // #s1 #s2 #s3 #ex #cl #K #tl * #ABS cases (ABS ?) % qed.
     955
     956lemma taaf_empty_to_eq : ∀S,st1,st2,taaf.
     957¬(bool_to_Prop (taaf_non_empty S st1 st2 taaf)) → st1 = st2.
     958#S #st1 #st2 * // #s1 #s2 #s3 #pre #ex #cl [2: #K ] * #ABS cases (ABS ?) % qed.
    772959
    773960theorem status_simulation_produce_ft :
     
    793980  ∀S1,S2.
    794981  ∀R.
    795   ∀st1,st1',stack,st2.∀ft1 : flat_trace S1 st1 st1' stack.
    796   status_simulation S1 S2 R → label_rel … st1 st2 → R st1 st2 →
     982  ∀st1,st1',st2.∀ft1 : flat_trace S1 st1 st1'.
     983  status_simulation S1 S2 R → R st1 st2 → label_rel … st1 st2 →
    797984  ∃st2_lab,st2'.
    798   ∃ft2 : flat_trace S2 st2 st2_lab stack.
     985  ∃ft2 : flat_trace S2 st2 st2_lab.
    799986  ∃taa : trace_any_any S2 st2_lab st2'.
    800   label_rel … st1' st2_lab ∧ R st1' st2' ∧ ft_observables … ft1 = ft_observables … ft2.
    801 #S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 -st1' -stack
    802 [ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] %
    803 |*: #st1_mid #st1' #stack [3,4: #f] #ft1 #ex [3: * [*]] #cl [#ncost_st1']
    804   (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S
    805   [1,2: (* other/jump *)
    806     lapply (sim_execute … ex G')
    807     try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta
    808     [ #H lapply (H ncost_st1') -H ] *
    809     #st2' *#taaf ** #ncost #G'' #H''
    810     %{st2'} %{st2'}
    811     %[1,3:
    812       @(ft_extend_taaf … taaf)
    813       @(ft_extend_taa … taa)
    814       assumption]
    815     %{(taa_base …)}
    816     % [1,3: %{H'' G''} ]
    817     whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
    818     lapply ncost lapply taa lapply H'' cases taaf -st2_mid -st2'
    819     [1,4: #st2' #H'' #taa * #ncost
    820       >ft_extend_taa_obs <L'
    821       [1,3: >(not_costed_no_label … ncost) >if_eq >S %
    822       |*: lapply L' lapply H'' lapply S lapply ft2 cases taa -st2_lab -st2'
    823         [1,3: #st2' #ft2 #S #H'' #L' >append_nil
    824           >not_costed_no_label
    825           [1,3: >append_nil @S ]
    826           whd in ⊢ (?%); >L' <H'' assumption
    827         |*: normalize nodelta #st2_mid #st2_mid' #st2' #_ #_ #_ #taa #ft2 #S #_ #_
    828           >S %
    829         ]
    830       ]
    831     |*: #st2_mid #st2_mid' #st2' #taa' #ex' #cl' [2,4: #cst ] #_ #taa *
    832       whd in ⊢ (???(?????%));
    833       >ft_extend_extend_taa >ft_extend_taa_advance_flat_obs
    834       >S >L' %
    835     ]
    836   |3: (* tailcall *)
    837     lapply (sim_execute … ex G')
    838     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
    839     * #st2_pre_call #cl' * #EQcall * #st2_after_call * #st2'
    840     * #taa2 * #taa2' ** #ex' #G'' #H''
    841     lapply (refl_jmeq … (ft_advance_tailcall … ft1 ex cl))
    842     generalize in match (ft_advance_tailcall … ft1 ex cl) in ⊢ (????%→%);
    843     <EQcall in ⊢ (%→???%%→%);
    844     #ft1' #EQft1'
    845     %{st2_after_call} %{st2'}
    846     %[@(ft_advance_tailcall … f … ex' cl')
    847       @(ft_extend_taa … (taa_append_taa … taa taa2))
    848       assumption]
    849     %{taa2'}
    850     % [ %{H'' G''} ]
    851     >ft_extend_taa_advance_tailcall_obs
    852     lapply EQft1' lapply ft1' -ft1'
    853     >EQcall in ⊢ (%→???%%→%);
    854     #ft1' #EQft1' destruct (EQft1')
    855     whd in ⊢ (??%?);
    856     >ft_observables_aux_def >append_nil
    857     >S >L' %
    858   |4: (* ret *)
    859     lapply (sim_execute … ex G')
    860     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
    861     #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
    862     ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'}
    863     %[@(ft_extend_taaf … taa2')
    864       @(ft_advance_ret … f … ex' cl')
    865       @(ft_extend_taa … (taa_append_taa … taa taa2))
    866       assumption]
    867     %{(taa_base …)}
    868     % [ %{H'' G''} ]
    869     >ft_extend_taaf_obs
    870     >ft_extend_taa_advance_ret_obs
    871     whd in ⊢ (??%?);
    872     >ft_observables_aux_def >append_nil
    873     lapply ncost cases taa2' -st2_after_ret -st2'
    874     [ #st2' * >append_nil
    875     |*: #st2_after_ret #st2_after_ret' #st2' #taa2' #ex'' #cl'' [2: #cst ] #ncost
    876       >(not_costed_no_label … ncost)
    877       >if_eq >append_nil
    878     ]
    879     >S >L' %
    880   |5: (* call *)
    881     lapply (sim_execute … ex G')
    882     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
    883     * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2'
    884     * #taa2 * #taa2' ** #ex' #G'' #H''
    885     %{st2_after_call} %{st2'}
    886     lapply (refl_jmeq … (ft_advance_call … ft1 ex cl))
    887     generalize in match (ft_advance_call … ft1 ex cl) in ⊢ (????%→%);
    888     <EQcall in ⊢ (%→???%%→%);
    889     #ft1' #EQft1'
    890     %[@(ft_advance_call … ex' cl')
    891       @(ft_extend_taa … (taa_append_taa … taa taa2))
    892       assumption]
    893     %{taa2'}
    894     % [ %{H'' G''} ]
    895     >ft_extend_taa_advance_call_obs
    896     lapply EQft1' lapply ft1' -ft1'
    897     >EQcall in ⊢ (%→???%%→%);
    898     #ft1' #EQft1' destruct (EQft1')
    899     whd in ⊢ (??%?);
    900     >ft_observables_aux_def >append_nil
    901     >S >L' %
    902   ]
     987  R st1' st2' ∧ label_rel … st1' st2_lab ∧ ft_stack_observables … ft1 = ft_stack_observables … ft2.
     988#S1 #S2 #R #st1 #st1' #st2 #ft1 #sim_execute #H #G elim ft1 -st1'
     989[ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] % ]
     990#st1_mid #st1' #ft1 #ex #ncost_st1'
     991(* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #G' #L' #S
     992inversion (as_classify … st1_mid) #cl
     993[2,5: (* other/jump *)
     994  lapply (sim_execute … ex G')
     995  try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta
     996  [ #H lapply (H (enforce_costedness_ok ??? ncost_st1' (jmeq_to_eq … cl))) -H ] *
     997  #st2' *#taaf ** #ncost #H'' #G''
     998  %{st2'} %{st2'}
     999  %[1,3:
     1000    @(ft_extend_taaf … (taa_append_taaf … taa taaf))
     1001    assumption]
     1002  %{(taa_base …)}
     1003  % [1,3: %{H'' G''} ]
     1004  >ft_extend_taaf_obs >taa_append_taaf_non_empty
     1005  whd in match ft_observables; whd in match ft_stack; normalize nodelta
     1006  <S whd in ⊢ (??%?); @pair_elim' normalize nodelta
     1007  >(status_class_dep_match_rewrite … cl) normalize nodelta @eq_f @eq_f
     1008  cases (true_or_false_Prop taa) #Htaa >Htaa
     1009  [2,4: lapply (taa_empty_to_eq … Htaa) #EQ destruct
     1010    cases (true_or_false_Prop (taaf_non_empty … taaf)) #Htaaf
     1011    >Htaaf in ncost ⊢ %;
     1012    [1,3: #_ |*: * #ncost lapply (taaf_empty_to_eq … Htaaf) #EQ destruct ]
     1013  ]
     1014  normalize nodelta in ncost ⊢ %; // >not_costed_no_label //
     1015  whd in ⊢ (?%); >L' <G'' assumption
     1016|4: (* tailcall *)
     1017  lapply (sim_execute … ex G')
     1018  >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
     1019  * #st2_pre_call #cl' * #EQcall * #st2_after_call * #st2'
     1020  * #taa2 * #taa2' ** #ex' #H'' #G''
     1021  %{st2_after_call} %{st2'}
     1022  %[@(ft_advance … ex' ?) [2: @hide_prf normalize >cl' % ]
     1023    @(ft_extend_taa … (taa_append_taa … taa taa2))
     1024    assumption]
     1025  %{taa2'}
     1026  % [ %{H'' G''} ]
     1027  >ft_extend_taa_advance_obs
     1028  whd in ⊢ (??%?); @pair_elim' @pair_elim'
     1029  >(status_class_dep_match_rewrite … cl)
     1030  >(status_class_dep_match_rewrite … cl') normalize nodelta
     1031  >S <EQcall >L' %
     1032|1: (* ret *)
     1033  lapply (sim_execute … ex G')
     1034  >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
     1035  #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
     1036  ***** #ncost #cl' #ex' #H'' #_ #G'' %{st2'} %{st2'}
     1037  %[@(ft_extend_taaf … taa2')
     1038    @(ft_advance … ex' ?) [2: @hide_prf normalize >cl' % ]
     1039    @(ft_extend_taa … (taa_append_taa … taa taa2))
     1040    assumption]
     1041  %{(taa_base …)}
     1042  % [ %{H'' G''} ]
     1043  >ft_extend_taaf_obs whd in match ft_observables; whd in match ft_stack; normalize nodelta
     1044  >ft_extend_taa_advance_obs
     1045  whd in ⊢ (??%?); @pair_elim' @pair_elim' normalize nodelta
     1046  >(status_class_dep_match_rewrite … cl)
     1047  >(status_class_dep_match_rewrite … cl') normalize nodelta
     1048  >S cases (\fst (ft_stack_observables … ft2)) [2: #f #stack']
     1049  normalize nodelta @eq_f >L' >associative_append @eq_f
     1050  cases (true_or_false_Prop (taaf_non_empty … taa2')) #H
     1051  >H in ncost ⊢ %; normalize nodelta [1,3: #ncost |*: lapply (taaf_empty_to_eq … H) #EQ destruct #_ ]
     1052  // >(not_costed_no_label … st2_after_ret) // >append_nil %
     1053|3: (* call *)
     1054  lapply (sim_execute … ex G')
     1055  >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
     1056  * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2'
     1057  * #taa2 * #taa2' ** #ex' #H'' #G''
     1058  %{st2_after_call} %{st2'}
     1059  %[@(ft_advance … ex' ?) [2: @hide_prf  normalize >cl' % ]
     1060    @(ft_extend_taa … (taa_append_taa … taa taa2))
     1061    assumption]
     1062  %{taa2'}
     1063  % [ %{H'' G''} ]
     1064  >ft_extend_taa_advance_obs @pair_elim' >(status_class_dep_match_rewrite … cl') normalize nodelta
     1065  whd in ⊢ (??%?); @pair_elim' >(status_class_dep_match_rewrite … cl) normalize nodelta
     1066  >S <EQcall >L' %
    9031067]
    9041068qed.
     1069
     1070theorem status_simulation_produce_ft_and_tlr :
     1071∀S1,S2.
     1072∀R.
     1073∀st1,st1',st1'',st2.
     1074∀ft1 : flat_trace S1 st1 st1'.
     1075∀tlr1 : trace_label_return S1 st1' st1''.
     1076status_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) ∧
     1082ft_observables … ft1 = ft_observables … ft2 ∧
     1083tlr_rel … tlr1 tlr2.
     1084#S1 #S2 #R #st1 #st1' #st1'' #st2 #ft1 #tlr1 * #S #L #simul
     1085cases (status_simulation_produce_ft … ft1 simul S L)
     1086#st2' * #st2_mid * #ft2 * #taa2 ** #S' #L' #EQ1
     1087cases (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
     1092]
     1093qed.
Note: See TracChangeset for help on using the changeset viewer.