source: src/joint/stacksize.ma @ 2407

include "basics/lists/list.ma".
include "joint/semantics.ma".
include "common/Executions.ma".

inductive call_ud (p: params) (globals: list ident): Type [0] ≝ 
  | up: joint_internal_function p globals → call_ud p globals    (* call *)
  | down: joint_internal_function p globals → call_ud p globals. (* return *)
  
let rec max_stacksize (p: params) (g: list ident) (fn_list: list (call_ud p g))
  (curr: nat) (max: nat) on fn_list: nat ≝ 
  match fn_list with
  [ nil      ⇒ max
  | cons h t ⇒ match h with
    [ up f   ⇒ let new_stack ≝ curr + joint_if_stacksize … f in
      if leb max new_stack
      then max_stacksize … t new_stack new_stack
      else max_stacksize … t new_stack max
    | down f ⇒ let new_stack ≝ curr - joint_if_stacksize … f in
      max_stacksize … t new_stack max
    ] 
  ].

let rec extract_list_from_tlr (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  (S: abstract_status) (s,s':S) (tr: trace_label_return S s s')
  (res: list (call_ud p g)) on tr: list (call_ud p g) ≝
  match tr with
  [ tlr_base s1 s2 tll        ⇒ 
    extract_list_from_tll … lg top_f … tll res
  | tlr_step s1 s2 s3 tll tlr ⇒ 
    let res' ≝ extract_list_from_tll … lg top_f … tll res in
    extract_list_from_tlr … lg top_f … tlr res'
  ]
and extract_list_from_tll (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  (S: abstract_status) ends (s,s':S) (tr: trace_label_label S ends s s')
  (res: list (call_ud p g)) on tr: list (call_ud p g) ≝
  match tr with
  [ tll_base ends s1 s2 tal co ⇒ 
    extract_list_from_tal … lg top_f … tal res
  ]
and extract_list_from_tal (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  (S: abstract_status) ends (s,s':S) (tr: trace_any_label S ends s s')
  (res: list (call_ud p g)) on tr: list (call_ud p g) ≝ 
  match tr with
  [ tal_base_not_return s1 s2 ex cl co ⇒ res
  | tal_base_return s1 s2 ex cl ⇒ down ?? (lg top_f)::res
  | tal_base_call s1p s1s s2 ex f cl ar tlr co ⇒
    extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res)
  | tal_step_call end s1p s1s s1a s2 ex f cl ar tlr co tal ⇒ 
    let res' ≝ extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res) in
    extract_list_from_tal … lg top_f … tal res'
  | tal_step_default end s1p s1i s1e ex tal cl co ⇒
    extract_list_from_tal … lg top_f … tal res
  ].

let rec tlr_rel_extract_equal (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  S1 S2 s1 s1' s2 s2' t1 t2 on t1:
  tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
  ∀res.extract_list_from_tlr p g lg top_f S1 s1 s1' t1 res =
  extract_list_from_tlr p g lg top_f S2 s2 s2' t2 res ≝ 
  match t1 with
  [ tlr_base st1 st1' tll1 ⇒ ?
  | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
  ]
and tll_rel_extract_equal (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
  t1 ≈ t2 →
  ∀res.extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 res =
  extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 res ≝
  match t1 with
  [ tll_base ends st1 st1' tal1 co ⇒ ?
  ]
and tal_rel_extract_equal (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
  t1 ≈ t2 →
  ∀res.extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 res =
  extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 res ≝
  match t1 with
  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
  | tal_base_return st1 st1' ex cl ⇒ ?
  | tal_base_call st1p st1s st1' ex f cl ar tlr1 co ⇒ ?
  | tal_step_call end st1p st1s st1 st1' ex f cl ar tlr1 co tal1 ⇒ ?
  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
  ].
[ cases t2
  [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim)
  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs
  ]
| cases t2
  [ #st2 #st2' #tll2 normalize #abs cases abs
  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res
    >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res)
    @(tlr_rel_extract_equal … (proj2 ?? Hsim))
  ]
| cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2
  @(tal_rel_extract_equal … H2)
| cases t2 
  [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res %
  | #st2 #st2' #ex' #cl' * #abs destruct (abs)
  | #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid *
    #taa * #H * #G * #K inversion taa in ⊢ ?;
    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 
    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
      normalize #abs destruct (abs)
    ]
  | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2 normalize *
    #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;
    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
      normalize #abs destruct (abs)
    ]
  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa
    * #H * #G * #K inversion taa in ⊢ ?;
    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 
      destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *)
    ]
  ]
| cases t2
  [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)
  | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res % 
  | #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs) 
  | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2
    normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;
    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
      normalize #abs destruct (abs)
    ]
  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid
    * #taa * #H * #G inversion taa in ⊢ ?;
    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
      destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *)  
    ]
  ]
| cases t2
  [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #taa
    * #st2mid' * #H * #f' * #G * #K * #tlr2 * #L * #H1 #H2 inversion taa in ⊢ ?;
    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1)
    | #st2'' #st2''' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
      normalize in H1; destruct (H1)
    ]
  | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs)
  | #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid *
    #taa * #st2mid' * #H * #f'' * #G * #K * #tlr2' * #L inversion taa in ⊢ ?;
    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res
      >(tlr_rel_extract_equal p g lg f … H2) cases daemon (* use injectivity and H1? *)
    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
      destruct normalize * #abs destruct (abs)
    ]
  | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2
    normalize * #H1 * #st2mid * #taa * #st2mid' * #H * #f * #G * #K * #tlr2' * #L
    inversion taa in ⊢ ?;
    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)
    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
      destruct normalize * #abs destruct (abs)
    ]
  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid *
    #taa * #st2mid' * #H * #f * #G * #K * #tlr2 * #L inversion taa in ⊢ ?;
    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)
    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
      destruct normalize * #H1 #H2 #res cases daemon (* do something with H1 and H2 *) 
    ]
  ]
| cases t2
  [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #taa * #st2_fun * #st2_after_fun
    * #H * #f' * #G * #K * #tlr2 * #L * #tl2 inversion taa in ⊢ ?;
    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    | #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
      normalize * * #abs destruct (abs)
    ]
  | #st2 #st2' #ex' #cl' normalize * #st2mid * #taa * #st2_fun * #st2_after_fun
    * #H * #f' * #G * #K * #tlr2 * #L * #tl2 inversion taa in ⊢ ?;
    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    | #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
      normalize * * #abs destruct (abs)
    ]
  | #st2p #st2s #st2' #ex' #f' #H #ar' #tlr2 #co' normalize * #st2mid * #taa
    * #st2_fun * #st2_after_fun * #H' * #f'' * #G * #K * #tlr2' * #L * #tl2
    inversion taa in ⊢ ?;
    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
      destruct normalize * * #abs destruct (abs)
    ]
  | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2
    normalize * #st2mid * #taa * #st2_fun * #st2_after_fun * #H * #f'' *
    #G * #K * #tlr2' * #L * #tl2 inversion taa in ⊢ ?;
    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
      >(tlr_rel_extract_equal … H2) cases daemon (* injectivity needed again *)
    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
      destruct normalize * * #abs destruct (abs)
    ]
  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #taa *
    #st2_fun * #st2_after_fun * #H * #f' * #G * #K * #tlr2' * #L * #tl2 
    inversion taa in ⊢ ?;
    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
      destruct normalize * * #H1 #H2 #H3 #res cases daemon (* look into this *) 
    ]
  ]
| cases t2
  [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res
    @(tal_rel_extract_equal p g lg top_f … Hsim) 
  | #ss #fs #ex' #cl' normalize #Hsim #res 
    @(tal_rel_extract_equal p g lg top_f … Hsim) 
  | #st2p #st2s #st2' #ex' #f' #H #ar' #tlr2 #co' normalize #Hsim #res
    @(tal_rel_extract_equal p g lg top_f … Hsim)
  | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2
    normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim)
  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize #Hsim #res
    @(tal_rel_extract_equal p g lg top_f … Hsim)
  ]
]
qed.

let rec tlr_rel_max_equal (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  S1 S2 s1 s1' s2 s2' t1 t2 on t1:
  tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
  max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) =
  max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝
  match t1 with
  [ tlr_base st1 st1' tll1 ⇒ ?
  | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
  ]
and tll_rel_extract_equal (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
  t1 ≈ t2 →
  max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) =
  max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝
  match t1 with
  [ tll_base ends st1 st1' tal1 co ⇒ ?
  ]
and tal_rel_extract_equal (p: params) (g: list ident)
  (lg: ident → joint_internal_function p g) (top_f: ident)
  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
  t1 ≈ t2 →
  max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) =
  max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝
  match t1 with
  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
  | tal_base_return st1 st1' ex cl ⇒ ?
  | tal_base_call st1p st1s st1' ex f cl ar tlr1 co ⇒ ?
  | tal_step_call end st1p st1s st1 st1' ex f cl ar tlr1 co tal1 ⇒ ?
  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
  ].
 cases daemon (* next proof *)
qed.