Ignore:
Timestamp:
Mar 1, 2013, 11:06:29 AM (7 years ago)
Author:
tranquil
Message:
  • changed primitives of abstract status (with stuf that is probably already there in all of its implementations): this temporarily breaks current as creations
  • generalised stacksize file and consequently moved it to common
File:
1 moved

Legend:

Unmodified
Added
Removed
  • src/common/stacksize.ma

    r2747 r2755  
    11include "basics/lists/list.ma".
    2 include "joint/joint_semantics.ma".
    3 include "common/Executions.ma".
    42include "common/StructuredTraces.ma".
    53
    6 inductive call_ud (p: params) (globals: list ident): Type [0] ≝
    7   | up: joint_internal_function p globals → call_ud p globals    (* call *)
    8   | down: joint_internal_function p globals → call_ud p globals. (* return *)
    9  
    10 let rec max_stacksize (p: params) (g: list ident) (fn_list: list (call_ud p g))
    11   (curr: nat) (max: nat) on fn_list: nat ≝
    12   match fn_list with
    13   [ nil      ⇒ max
    14   | cons h t ⇒ match h with
    15     [ up f   ⇒ let new_stack ≝ curr + joint_if_stacksize … f in
    16       if leb max new_stack
    17       then max_stacksize … t new_stack new_stack
    18       else max_stacksize … t new_stack max
    19     | down f ⇒ let new_stack ≝ curr - joint_if_stacksize … f in
    20       max_stacksize … t new_stack max
    21     ]
    22   ].
     4inductive call_ud : Type [0] ≝
     5  | up: ident → call_ud    (* call *)
     6  | down: ident → call_ud. (* return *)
    237
    24 let rec extract_list_from_tlr (p: params) (g: list ident)
    25   (lg: ident → joint_internal_function p g) (top_f: ident)
    26   (S: abstract_status) (s,s':S) (tr: trace_label_return S s s')
    27   (res: list (call_ud p g)) on tr: list (call_ud p g) ≝
    28   match tr with
    29   [ tlr_base s1 s2 tll        ⇒
    30     extract_list_from_tll … lg top_f … tll res
    31   | tlr_step s1 s2 s3 tll tlr ⇒
    32     let res' ≝ extract_list_from_tll … lg top_f … tll res in
    33     extract_list_from_tlr … lg top_f … tlr res'
    34   ]
    35 and extract_list_from_tll (p: params) (g: list ident)
    36   (lg: ident → joint_internal_function p g) (top_f: ident)
    37   (S: abstract_status) ends (s,s':S) (tr: trace_label_label S ends s s')
    38   (res: list (call_ud p g)) on tr: list (call_ud p g) ≝
    39   match tr with
    40   [ tll_base ends s1 s2 tal co ⇒
    41     extract_list_from_tal … lg top_f … tal res
    42   ]
    43 and extract_list_from_tal (p: params) (g: list ident)
    44   (lg: ident → joint_internal_function p g) (top_f: ident)
    45   (S: abstract_status) ends (s,s':S) (tr: trace_any_label S ends s s')
    46   (res: list (call_ud p g)) on tr: list (call_ud p g) ≝
    47   match tr with
    48   [ tal_base_not_return s1 s2 ex cl co ⇒ res
    49   | tal_base_return s1 s2 ex cl ⇒ down ?? (lg top_f)::res
    50   | tal_base_call s1p s1s s2 ex cl ar tlr co ⇒
    51     extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr
    52       (up ?? (lg (as_call_ident ? «s1p,cl»))::res)
    53   | tal_base_tailcall s1p s1s s2 ex cl tlr ⇒
    54      extract_list_from_tlr ?? lg (as_tailcall_ident ? «s1p,cl») … tlr
    55       (up ?? (lg (as_tailcall_ident ? «s1p,cl»))::down … (lg top_f)::res)
    56   | tal_step_call end s1p s1s s1a s2 ex cl ar tlr co tal ⇒
    57     let res' ≝ extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr
    58       (up ?? (lg (as_call_ident ? «s1p,cl»))::res) in
    59     extract_list_from_tal … lg top_f … tal res'
    60   | tal_step_default end s1p s1i s1e ex tal cl co ⇒
    61     extract_list_from_tal … lg top_f … tal res
    62   ].
     8record stacksize_info : Type[0] ≝
     9{ current : ℕ ; maximum : ℕ }.
    6310
    64 let rec tlr_rel_extract_equal (p: params) (g: list ident)
    65   (lg: ident → joint_internal_function p g) (top_f: ident)
    66   S1 S2 s1 s1' s2 s2' t1 t2 on t1:
    67   tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
    68   ∀res.extract_list_from_tlr p g lg top_f S1 s1 s1' t1 res =
    69   extract_list_from_tlr p g lg top_f S2 s2 s2' t2 res ≝
    70   match t1 with
    71   [ tlr_base st1 st1' tll1 ⇒ ?
    72   | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
    73   ]
    74 and tll_rel_extract_equal (p: params) (g: list ident)
    75   (lg: ident → joint_internal_function p g) (top_f: ident)
    76   S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
    77   t1 ≈ t2 →
    78   ∀res.extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 res =
    79   extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 res ≝
    80   match t1 with
    81   [ tll_base ends st1 st1' tal1 co ⇒ ?
    82   ]
    83 and tal_rel_extract_equal (p: params) (g: list ident)
    84   (lg: ident → joint_internal_function p g) (top_f: ident)
    85   S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
    86   t1 ≈ t2 →
    87   ∀res.extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 res =
    88   extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 res ≝
    89   match t1 with
    90   [ tal_base_not_return st1 st1' ex cl co ⇒ ?
    91   | tal_base_return st1 st1' ex cl ⇒ ?
    92   | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ?
    93   | tal_base_tailcall st1p st1s st1' ex cl tlr1 ⇒ ?
    94   | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ?
    95   | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
    96   ].
    97 [ cases t2
    98   [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim)
    99   | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs
    100   ]
    101 | cases t2
    102   [ #st2 #st2' #tll2 normalize #abs cases abs
    103   | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res
    104     >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res)
    105     @(tlr_rel_extract_equal … (proj2 ?? Hsim))
    106   ]
    107 | cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2
    108   @(tal_rel_extract_equal … H2)
    109 | cases t2
    110   [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res %
    111   | #st2 #st2' #ex' #cl' * #abs destruct (abs)
    112   | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid *
    113     #taa * #H * #G * #K inversion taa in ⊢ ?;
    114     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    115     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    116       normalize #abs destruct (abs)
    117     ]
    118   | #st2p #st2s #st2' #ex' #cl' #tlr2 normalize * #H1 * #st2mid *
    119     #taa * #H * #G * #K inversion taa in ⊢ ?;
    120     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    121     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    122       normalize #abs destruct (abs)
    123     ]
    124   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize *
    125     #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;
    126     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    127     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    128       normalize #abs destruct (abs)
    129     ]
    130   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa
    131     * #H * #G * #K inversion taa in ⊢ ?;
    132     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    133     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    134       destruct normalize #Hsim destruct (Hsim) (* getting somewhere. Use Hind? *)
    135       cases daemon
    136     ]
    137   ]
    138 | cases t2
    139   [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)
    140   | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res %
    141   | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs)
    142   | #st2p #st2s #st2' #ex' #cl' #tlr2 normalize * #abs destruct (abs)
    143   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
    144     normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;
    145     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    146     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    147       normalize #abs destruct (abs)
    148     ]
    149   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid
    150     * #taa * #H * #G inversion taa in ⊢ ?;
    151     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    152     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    153       destruct normalize #Hsim destruct (Hsim)
    154       cases daemon (* use Hind again? *) 
    155     ]
    156   ]
    157 | cases t2
    158   [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #G * #ident_eq * #taa
    159     * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2 * #L * #H1
    160     [ * * #H3 #H2 #H4 | #H2 ]
    161     inversion taa in ⊢ ?;
    162     [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H3; destruct (H3)
    163     | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    164       normalize in H3; destruct (H3)
    165     | #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1)
    166     | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    167       normalize in H1; destruct (H1)
    168     ]
    169   | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs)
    170   | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid * #G
    171     * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2' * #L
    172     [* #tl2]
    173     inversion taa in ⊢ ?;
    174     [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    175     | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    176       destruct normalize * * #abs destruct (abs)
    177     | #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res
    178       >(tlr_rel_extract_equal p g lg … H2) destruct (H1)
    179       >ident_eq %
    180     | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    181       destruct normalize * #abs destruct (abs)
    182     ]
    183   | (* tail call case *) cases daemon
    184   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize
    185     * #H1 * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *]
    186     #K * #tlr2' * #L [* #tl2]
    187     inversion taa in ⊢ ?;
    188     [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res
    189       destruct (H1) >(tlr_rel_extract_equal … H2) >ident_eq
    190       (* to do here: destruct tl2: 3 cases by contradiction, 1 by equality and 1 by
    191        * not sure yet *) cases daemon
    192     |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    193       destruct normalize * * [#abs destruct (abs)] #H2 #res <ident_eq
    194       >(tlr_rel_extract_equal … H2) cases daemon (* stumped here *)
    195     ]
    196   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid *
    197     #G * #ident_eq * #taa * #st2mid' * #H * * [2: #stmid'' * ] #K * #tlr2 * #L
    198     [* #tl2]
    199     inversion taa in ⊢ ?;
    200     [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res
    201       destruct (H1)
    202     |2,4: #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    203       destruct normalize * [*] #H1 #H2 [#H3] #res destruct (H1) <ident_eq
    204       >(tlr_rel_extract_equal … H2) cases daemon (* stumped again *)
    205     ]
    206   ]
    207 | (* tail call case *) cases daemon
    208 | cases t2
    209   [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #G * #ident_eq * #taa *
    210     #st2mid' * #H * * [#_ | #st2mid''] * #K * #tlr2 * #L [2: * #tl2]
    211     inversion taa in ⊢ ?;
    212     [1,3: #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #H1 destruct (H1)
    213     |2,4: #st2p #st2p' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    214       destruct normalize * * #H1 destruct (H1)
    215     ]
    216   | #st2 #st2' #ex' #cl' normalize * #st2mid * #G * #ident_eq * #taa * #st2mid'
    217     * #H * * [#abs destruct (abs)] #st2mid' * #K * #tlr2 * #L * #tl2
    218     inversion taa in ⊢ ?;
    219     [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    220     | #st2p #st2p' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    221       normalize * * #abs destruct (abs)
    222     ]
    223   | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #st2mid * #G *
    224     #ident_eq * #taa * #st2mid' * #H * * [ #_ | #st2mid'' ] * #K * #tlr2' * #L
    225     [2: * #tl2]
    226     inversion taa in ⊢ ?;
    227     [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
    228       destruct (H1) >ident_eq >(tlr_rel_extract_equal … H3)
    229       cases tal1 in H2;
    230       [ #ss #sf #ex'' #cl'' #co'' normalize #_ %
    231       | #ss #sf #ex'' #cl'' normalize #abs cases abs
    232       | #st1p' #st1s #sf #ex'' #cl'' #ar'' #tlr1' #co'' normalize #abs cases abs
    233       | #st1p' #st1s #sf #ex'' #cl'' #tlr1' normalize #abs cases abs
    234       | #end' #st1p' #st1s' #st1a' #sf #ex'' #cl'' #ar'' #tlr1' #co' #tal1'
    235         normalize #abs cases abs
    236       | #end' #st1p' #st1i #st1e #ex'' #tal1' #cl'' #co'' normalize
    237         cases daemon (* use induction here, but no *)
    238       ]
    239     |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    240       destruct normalize * * #abs destruct (abs)
    241     ]
    242   | (* tail call case *) cases daemon
    243   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
    244     normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * *
    245     [ #H1 | #st2mid''] * #K * #tlr2' * #L [2: * #tl2] inversion taa in ⊢ ?;
    246     [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
    247       destruct (H1) >ident_eq >(tal_rel_extract_equal … H2)
    248       >(tlr_rel_extract_equal … H3) %
    249     |2,4: #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    250       destruct normalize * * #abs destruct (abs)
    251     ]
    252   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #G *
    253     #ident_eq * #taa * #st2mid' * #H * * [ #He | #st2mid'' ] * #K * #tlr2' * #L
    254     [2: * #tl2] inversion taa in ⊢ ?;
    255     [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    256     |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    257       destruct normalize * * #H1 #H2 #H3 #res destruct (H1)
    258       >(tlr_rel_extract_equal … H3) <ident_eq normalize cases daemon
    259       (* look further here *)
    260     ]
    261   ]
    262 | cases t2
    263   [ #st2 #st2' #ex' #cl' #co'
    264   | #ss #fs #ex' #cl'
    265   | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co'
    266   | #st2p #st2s #st2' #ex' #cl' #tlr2
    267   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
    268   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co'
    269   ]
    270   normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim)
    271 ]
    272 (* Another tailcall case escaped *) cases daemon
     11definition update_stacksize_info :
     12  (ident → option ℕ) → stacksize_info → list call_ud → stacksize_info ≝
     13  λstacksizes.
     14  let get_stacksize ≝
     15    λf.match stacksizes f with
     16      [ Some n ⇒ n | None ⇒ 0 (* should never happen *) ] in
     17  let f ≝ λud,acc.
     18    match ud with
     19    [ up i ⇒
     20      let new_stack ≝ get_stacksize i + current acc in
     21      let new_max ≝ max (maximum acc) new_stack in
     22      mk_stacksize_info new_stack new_max
     23    | down i ⇒
     24      let new_stack ≝ current acc - get_stacksize i in
     25      mk_stacksize_info new_stack (maximum acc)
     26    ] in
     27  foldr ?? f.
     28
     29definition extract_call_ud_from_observables :
     30  list intensional_event → list call_ud ≝
     31let f ≝ λev.match ev with
     32[ IEVcall i ⇒ [up i] | IEVtailcall i j ⇒ [down i; up j] | IEVret i ⇒ [down i] | _ ⇒ [ ]] in
     33foldr ?? (λev.append ? (f ev)) [ ].
     34
     35definition extract_call_ud_from_tlr :
     36  ∀S,st1,st2.trace_label_return S st1 st2 → ident → list call_ud ≝
     37λS,st1,st2,tlr,curr.
     38  extract_call_ud_from_observables … (observables_trace_label_return … tlr curr).
     39
     40definition extract_call_ud_from_tll :
     41  ∀S,fl,st1,st2.trace_label_label fl S st1 st2 → ident → list call_ud ≝
     42λS,fl,st1,st2,tll,curr.
     43  extract_call_ud_from_observables … (observables_trace_label_label … tll curr).
     44
     45lemma tlr_rel_same_stacksize_info :
     46  ∀stacksizes.
     47  ∀S1,S2,s1,s1',s2,s2'.
     48  ∀tlr1 : trace_label_return S1 s1 s1'.
     49  ∀tlr2 : trace_label_return S2 s2 s2'.
     50  ∀curr.∀curr_stacksize.
     51  tlr_rel … tlr1 tlr2 →
     52  update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tlr … tlr1 curr) =
     53  update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tlr … tlr2 curr).
     54#stacksizes #S1 #S2 #s1 #s1' #s2 #s2' #tlr1 #tlr2 #curr #info
     55#equiv @eq_f whd in ⊢ (??%%); @eq_f
     56@tlr_rel_to_traces_same_observables assumption
    27357qed.
    27458
    275 let rec tlr_rel_max_equal (p: params) (g: list ident)
    276   (lg: ident → joint_internal_function p g) (top_f: ident)
    277   S1 S2 s1 s1' s2 s2' t1 t2 on t1:
    278   tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
    279   max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) =
    280   max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝
    281   match t1 with
    282   [ tlr_base st1 st1' tll1 ⇒ ?
    283   | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
    284   ]
    285 and tll_rel_max_equal (p: params) (g: list ident)
    286   (lg: ident → joint_internal_function p g) (top_f: ident)
    287   S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
    288   t1 ≈ t2 →
    289   max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) =
    290   max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝
    291   match t1 with
    292   [ tll_base ends st1 st1' tal1 co ⇒ ?
    293   ]
    294 and tal_rel_max_equal (p: params) (g: list ident)
    295   (lg: ident → joint_internal_function p g) (top_f: ident)
    296   S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
    297   t1 ≈ t2 →
    298   max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) =
    299   max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝
    300   match t1 with
    301   [ tal_base_not_return st1 st1' ex cl co ⇒ ?
    302   | tal_base_return st1 st1' ex cl ⇒ ?
    303   | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ?
    304   | tal_base_tailcall st1p st1s st1' ex cl tlr1 ⇒ ?
    305   | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ?
    306   | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
    307   ].
    308 [1,2: #Hsim >(tlr_rel_extract_equal … Hsim []) %
    309 |3: #Hsim >(tll_rel_extract_equal … Hsim []) %
    310 |*: #Hsim >(tal_rel_extract_equal … Hsim []) %
    311 ]
     59lemma tll_rel_same_stacksize_info :
     60  ∀stacksizes.
     61  ∀S1,S2,fl1,fl2,s1,s1',s2,s2'.
     62  ∀tll1 : trace_label_label S1 fl1 s1 s1'.
     63  ∀tll2 : trace_label_label S2 fl2 s2 s2'.
     64  ∀curr.∀curr_stacksize.
     65  tll_rel … tll1 tll2 →
     66  update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tll … tll1 curr) =
     67  update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tll … tll2 curr).
     68#stacksizes #S1 #S2 #fl1 #fl2 #s1 #s1' #s2 #s2' #tlr1 #tlr2 #curr #info
     69#equiv @eq_f whd in ⊢ (??%%); @eq_f
     70@tll_rel_to_traces_same_observables assumption
    31271qed.
Note: See TracChangeset for help on using the changeset viewer.