root/src/common/StructuredTraces.ma @ 1926

include "basics/types.ma".
include "basics/bool.ma".
include "basics/jmeq.ma".
include "common/CostLabel.ma".
include "utilities/option.ma".
include "basics/lists/listb.ma".
include "ASM/Util.ma".

inductive status_class : Type[0] ≝
| cl_return : status_class
| cl_jump   : status_class
| cl_call   : status_class
| cl_other : status_class.

record abstract_status : Type[1] ≝
  { as_status :> Type[0]
  ; as_execute : as_status → as_status → Prop
  ; as_pc : DeqSet
  ; as_pc_of : as_status → as_pc
  ; as_classifier : as_status → status_class → Prop
  ; as_label : as_status → option costlabel
  ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
  ; as_final: as_status → Prop
}.

(* temporary alias for backward compatibility *)
definition final_abstract_status ≝ abstract_status.

definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝
  λa_s,st.as_label ? st ≠ None ?.

definition as_label_safe : ∀a_s : abstract_status.
  (Σs : a_s.as_costed ? s) → costlabel ≝
  λa_s,st_sig.opt_safe … (pi2 … st_sig).

inductive trace_ends_with_ret: Type[0] ≝
  | ends_with_ret: trace_ends_with_ret
  | doesnt_end_with_ret: trace_ends_with_ret.

inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
  | tlr_base:
      ∀status_before: S.
      ∀status_after: S.
        trace_label_label S ends_with_ret status_before status_after →
        trace_label_return S status_before status_after
  | tlr_step:
      ∀status_initial: S.
      ∀status_labelled: S.
      ∀status_final: S.
        trace_label_label S doesnt_end_with_ret status_initial status_labelled →
        trace_label_return S status_labelled status_final →
          trace_label_return S status_initial status_final
with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
  | tll_base:
      ∀ends_flag: trace_ends_with_ret.
      ∀start_status: S.
      ∀end_status: S.
        trace_any_label S ends_flag start_status end_status →
        as_costed S start_status →
          trace_label_label S ends_flag start_status end_status
with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
  (* Single steps within a function which reach a label.
     Note that this is the only case applicable for a jump. *)
  | tal_base_not_return:
      ∀start_status: S.
      ∀final_status: S.
        as_execute S start_status final_status →
        (as_classifier S start_status cl_jump ∨
         as_classifier S start_status cl_other) →
        as_costed S final_status →
          trace_any_label S doesnt_end_with_ret start_status final_status
  | tal_base_return:
      ∀start_status: S.
      ∀final_status: S.
        as_execute S start_status final_status →
        as_classifier S start_status cl_return →
          trace_any_label S ends_with_ret start_status final_status
  (* A call followed by a label on return. *)
  | tal_base_call:
      ∀status_pre_fun_call: S.
      ∀status_start_fun_call: S.
      ∀status_final: S.
        as_execute S status_pre_fun_call status_start_fun_call →
        ∀H:as_classifier S status_pre_fun_call cl_call.
          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final →
          trace_label_return S status_start_fun_call status_final →
          as_costed S status_final →
            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
  (* A call followed by a non-empty trace. *)
  | tal_step_call:
      ∀end_flag: trace_ends_with_ret.
      ∀status_pre_fun_call: S.
      ∀status_start_fun_call: S.
      ∀status_after_fun_call: S.
      ∀status_final: S.
        as_execute S status_pre_fun_call status_start_fun_call →
        ∀H:as_classifier S status_pre_fun_call cl_call.
          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
          trace_label_return S status_start_fun_call status_after_fun_call →
          ¬ as_costed S status_after_fun_call →
          trace_any_label S end_flag status_after_fun_call status_final →
            trace_any_label S end_flag status_pre_fun_call status_final
  | tal_step_default:
      ∀end_flag: trace_ends_with_ret.
      ∀status_pre: S.
      ∀status_init: S.
      ∀status_end: S.
        as_execute S status_pre status_init →
        trace_any_label S end_flag status_init status_end →
        as_classifier S status_pre cl_other →
        ¬ (as_costed S status_init) →
          trace_any_label S end_flag status_pre status_end.

let rec tal_pc_list (S : abstract_status) fl st1 st2 (tal : trace_any_label S fl st1 st2)
  on tal : list (as_pc S) ≝
 match tal with
 [ tal_step_call fl' pre _ st1' st2' _ _ _ _ _ tl ⇒ as_pc_of … pre :: tal_pc_list … tl
 | tal_step_default fl' pre st1' st2' _ tl _ _ ⇒  as_pc_of … pre :: tal_pc_list … tl
 | tal_base_not_return pre _ _ _ _ ⇒ [as_pc_of … pre]
 | tal_base_return pre _ _ _ ⇒ [as_pc_of … pre]
 | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
 ].

let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝
  match tlr with
  [ tlr_base st1 st2 tll ⇒ tll_unrepeating … tll
  | tlr_step st1 st2 st3 tll tl ⇒ tll_unrepeating … tll ∧ tlr_unrepeating … tl
  ]
and tll_unrepeating S fl st1 st2 (tll : trace_label_label S fl st1 st2) on tll : Prop ≝
  match tll with
  [ tll_base fl st1 st2 tal _ ⇒ tal_unrepeating … tal
  ]
and tal_unrepeating S fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : Prop ≝
  match tal with
  [ tal_step_call fl st1 st2 st3 st4 _ _ _ tlr _ tl ⇒
    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
    tal_unrepeating … tl ∧
    tlr_unrepeating … tlr
  | tal_step_default fl st1 st2 st3 _ tl _ _ ⇒
    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
    tal_unrepeating … tl
  | _ ⇒ True
  ].

definition tll_hd_label : ∀S : abstract_status.∀fl,st1,st2.
  trace_label_label S fl st1 st2 → costlabel ≝
  λS,fl,st1,st2,tr.match tr with
  [ tll_base _ st1' _ _ prf ⇒ as_label_safe … «st1', prf» ].

definition tlr_hd_label : ∀S : abstract_status.∀st1,st2.
  trace_label_return S st1 st2 → costlabel ≝
  λS,st1,st2,tr.match tr with
  [ tlr_base st1' st2' tll ⇒ tll_hd_label … tll
  | tlr_step st1' st2' _ tll _ ⇒ tll_hd_label … tll
  ].

let rec tal_unrepeating_uniqueb S fl st1 st2 tal on tal :
  tal_unrepeating S fl st1 st2 tal → bool_to_Prop (uniqueb … (tal_pc_list … tal)) ≝ ?.
cases tal //
#fl' #st1' [#st_fun] #st2' #st3' #H
[ #H0 #H1 #tlr #G #tal | #tal #H0 #G ] whd in ⊢ (% → ?%); [*]*
#A #B [#_] >A normalize nodelta @tal_unrepeating_uniqueb assumption
qed.

inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝
  | tac_base:
      ∀status: S.
        as_classifier S status cl_call →
          trace_any_call S status status
  | tac_step_call:
      ∀status_pre_fun_call: S.
      ∀status_after_fun_call: S.
      ∀status_final: S.
      ∀status_start_fun_call: S.
        as_execute S status_pre_fun_call status_start_fun_call →
        ∀H:as_classifier S status_pre_fun_call cl_call.
          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
          trace_label_return S status_start_fun_call status_after_fun_call →
          ¬ as_costed S status_after_fun_call →
          trace_any_call S status_after_fun_call status_final →
            trace_any_call S status_pre_fun_call status_final
  | tac_step_default:
      ∀status_pre: S.
      ∀status_end: S.
      ∀status_init: S.
        as_execute S status_pre status_init →
        trace_any_call S status_init status_end →
        as_classifier S status_pre cl_other →
        ¬ (as_costed S status_init) →
          trace_any_call S status_pre status_end.

              
inductive trace_label_call (S:abstract_status) : S → S → Type[0] ≝
  | tlc_base:
      ∀start_status: S.
      ∀end_status: S.
        trace_any_call S start_status end_status →
        as_costed S start_status →
        trace_label_call S start_status end_status
.

definition tlc_hd_label : ∀S : abstract_status.∀st1,st2.
  trace_label_call S st1 st2 → costlabel ≝
  λS,st1,st2,tr.match tr with
  [ tlc_base st1' _ _ prf ⇒ as_label_safe … «st1', prf»
  ].       

coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
  | tld_step:
      ∀status_initial: S.
      ∀status_labelled: S.
          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
          trace_label_diverges S status_labelled →
            trace_label_diverges S status_initial
  | tld_base:
      ∀status_initial: S.
      ∀status_pre_fun_call: S.
      ∀status_start_fun_call: S.
        trace_label_call S status_initial status_pre_fun_call →
        as_execute S status_pre_fun_call status_start_fun_call →
        ∀H:as_classifier S status_pre_fun_call cl_call.
          trace_label_diverges S status_start_fun_call →
            trace_label_diverges S status_initial.

definition tld_hd_label : ∀S : abstract_status.∀st.
  trace_label_diverges S st → costlabel ≝
  λS,st,tr.match tr with
  [ tld_step st' st'' tll _ ⇒ tll_hd_label … tll
  | tld_base st' st'' _ tlc _ _ _ ⇒ tlc_hd_label … tlc
  ].       

(* Version in Prop for showing existence. *)
coinductive trace_label_diverges_exists (S:abstract_status) : S → Prop ≝
  | tld_step:
      ∀status_initial: S.
      ∀status_labelled: S.
          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
          trace_label_diverges_exists S status_labelled →
            trace_label_diverges_exists S status_initial
  | tld_base:
      ∀status_initial: S.
      ∀status_pre_fun_call: S.
      ∀status_start_fun_call: S.
        trace_label_call S status_initial status_pre_fun_call →
        as_execute S status_pre_fun_call status_start_fun_call →
        ∀H:as_classifier S status_pre_fun_call cl_call.
          trace_label_diverges_exists S status_start_fun_call →
            trace_label_diverges_exists S status_initial.

inductive trace_whole_program (S: abstract_status) : S → Type[0] ≝
  | twp_terminating:
      ∀status_initial: S.
      ∀status_start_fun: S.
      ∀status_final: S.
        as_classifier S status_initial cl_call →
        as_execute S status_initial status_start_fun →
        trace_label_return S status_start_fun status_final →
        as_final S status_final →
        trace_whole_program S status_initial
  | twp_diverges:
      ∀status_initial: S.
      ∀status_start_fun: S.
        as_classifier S status_initial cl_call →
        as_execute S status_initial status_start_fun →
        trace_label_diverges S status_start_fun →
        trace_whole_program S status_initial.

(* Again, an identical version in Prop for existence proofs. *)
inductive trace_whole_program_exists (S: abstract_status) : S → Prop ≝
  | twp_terminating:
      ∀status_initial: S.
      ∀status_start_fun: S.
      ∀status_final: S.
        as_classifier S status_initial cl_call →
        as_execute S status_initial status_start_fun →
        trace_label_return S status_start_fun status_final →
        as_final S status_final →
        trace_whole_program_exists S status_initial
  | twp_diverges:
      ∀status_initial: S.
      ∀status_start_fun: S.
        as_classifier S status_initial cl_call →
        as_execute S status_initial status_start_fun →
        trace_label_diverges_exists S status_start_fun →
        trace_whole_program_exists S status_initial.


let rec trace_any_label_label S s s' f
  (tr:trace_any_label S f s s') on tr : match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] ≝
match tr return λf,s,s',tr. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] with 
[ tal_base_not_return start final _ _ C ⇒ C
| tal_base_return _ _  _ _ ⇒ I
| tal_base_call _ _ _ _ _ _ _ C ⇒ C
| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
].

definition tal_tl_label : ∀S : abstract_status.∀st1,st2.
  trace_any_label S doesnt_end_with_ret st1 st2 → costlabel ≝
  λS,st1,st2,tr.as_label_safe … «st2, trace_any_label_label … tr».

lemma trace_label_label_label : ∀S,s,s',f.
  ∀tr:trace_label_label S f s s'. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ].
#S #s #s' #f #tr
cases tr
#f #start #end #tr' #C @(trace_any_label_label … tr')
qed.

definition tll_tl_label : ∀S : abstract_status.∀st1,st2.
  trace_label_label S doesnt_end_with_ret st1 st2 → costlabel ≝
  λS,st1,st2,tr.as_label_safe … «st2, trace_label_label_label … tr».

lemma trace_any_call_call : ∀S,s,s'.
  trace_any_call S s s' → as_classifier S s' cl_call.
#S #s #s' #T elim T //
qed.

(* an uncalling, unreturning and *unjumping*,
  as well as unlabelled (but possibly for the first and last statuses) 
  possibly empty trace segment *)
inductive trace_any_any (S:abstract_status) : S → S → Type[0] ≝
  | taa_base :
      ∀start_status: S.
        trace_any_any S start_status start_status
  | taa_step :
      ∀status_pre: S.
      ∀status_init: S.
      ∀status_end: S.
        as_execute S status_pre status_init →
        trace_any_any S status_init status_end →
        as_classifier S status_pre cl_other →
        ¬as_costed … status_init →
          trace_any_any S status_pre status_end.

let rec taa_status_list S st1 st2 (taa : trace_any_any S st1 st2) on taa : list S ≝
  match taa with
  [ taa_base st1' ⇒ [st1']
  | taa_step st1' st2' st3' _ tl _ _ ⇒ st1' :: taa_status_list … tl
  ].

let rec taa_append_taa S st1 st2 st3 (taa1 : trace_any_any S st1 st2)
  on taa1 : trace_any_any S st2 st3 → trace_any_any S st1 st3 ≝
  match taa1
  return λst1,st2.λx : trace_any_any S st1 st2.
    trace_any_any S st2 st3 → trace_any_any S st1 st3
  with
  [ taa_base _ ⇒ λtaa2.taa2
  | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
      taa_step … H (taa_append_taa … tl taa2) G K
  ].

let rec taa_append_tal S st1 fl st2 st3 (taa : trace_any_any S st1 st2)
  on taa :
  trace_any_label S fl st2 st3 →
  trace_any_label S fl st1 st3 ≝
  match taa
  return λst1,st2.λx : trace_any_any S st1 st2.
    trace_any_label S fl st2 st3 → trace_any_label S fl st1 st3
  with
  [ taa_base _ ⇒ λtaa2.taa2
  | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
      tal_step_default … H (taa_append_tal … tl taa2) G K
  ].

let rec tlr_rel S1 st1 st1' S2 st2 st2'
  (tlr1 : trace_label_return S1 st1 st1')
  (tlr2 : trace_label_return S2 st2 st2') on tlr1 : Prop ≝
match tlr1 with
  [ tlr_base st1 st1' tll1 ⇒
    match tlr2 with
    [ tlr_base st2 st2' tll2 ⇒ tll_rel … tll1 tll2
    | _ ⇒ False
    ]
  | tlr_step st1 st1' st1'' tll1 tl1 ⇒
    match tlr2 with
    [ tlr_step st2 st2' st2'' tll2 tl2 ⇒
      tll_rel … tll1 tll2 ∧ tlr_rel … tl1 tl2
    | _ ⇒ False
    ]
  ]
and tll_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
 (tll1 : trace_label_label S1 fl1 st1 st1')
 (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝
  match tll1 with
  [ tll_base fl1 st1 st1' tal1 H ⇒
    match tll2 with
    [ tll_base fl2 st2 st2 tal2 G ⇒
      as_label_safe … («?, H») = as_label_safe … («?, G») ∧
      tal_rel … tal1 tal2
    ]
  ]
and tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
 (tal1 : trace_any_label S1 fl1 st1 st1')
 (tal2 : trace_any_label S2 fl2 st2 st2')
   on tal1 : Prop ≝
  match tal1 with
  [ tal_base_not_return st1 st1' _ _ _ ⇒
    ∃st2mid,taa,H,G,K.
    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
      (tal_base_not_return ? st2mid st2' H G K)
  | tal_base_return st1 st1' _ _ ⇒
    ∃st2mid,taa,H,G.
    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
      (tal_base_return ? st2mid st2' H G)
  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒
    ∃st2mid,taa,st2mid',H,G,K,tlr2,L.
    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
      (tal_base_call ? st2mid st2mid' st2' H G K tlr2 L) ∧
      tlr_rel … tlr1 tlr2
  | tal_step_call fl1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒
    ∃st2mid,taa,st2_fun,st2_after_fun,H,G,K,tlr2,L,tl2.
    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
      (tal_step_call ?? st2mid st2_fun st2_after_fun st2' H G K tlr2 L tl2) ∧
      tlr_rel … tlr1 tlr2 ∧ tal_rel … tl1 tl2
  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
    tal_rel … tl1 tal2 (* <- this makes it many to many *)
  ].