source: src/joint/stacksize.ma @ 2562

Last change on this file since 2562 was 2456, checked in by boender, 8 years ago
  • added simple proof
File size: 13.5 KB
Line 
1include "basics/lists/list.ma".
2include "joint/semantics.ma".
3include "common/Executions.ma".
4include "common/StructuredTraces.ma".
5
6inductive 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 
10let 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  ].
23
24let 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  ]
35and 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  ]
43and 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_step_call end s1p s1s s1a s2 ex cl ar tlr co tal ⇒
54    let res' ≝ extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr
55      (up ?? (lg (as_call_ident ? «s1p,cl»))::res) in
56    extract_list_from_tal … lg top_f … tal res'
57  | tal_step_default end s1p s1i s1e ex tal cl co ⇒
58    extract_list_from_tal … lg top_f … tal res
59  ].
60
61let rec tlr_rel_extract_equal (p: params) (g: list ident)
62  (lg: ident → joint_internal_function p g) (top_f: ident)
63  S1 S2 s1 s1' s2 s2' t1 t2 on t1:
64  tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
65  ∀res.extract_list_from_tlr p g lg top_f S1 s1 s1' t1 res =
66  extract_list_from_tlr p g lg top_f S2 s2 s2' t2 res ≝
67  match t1 with
68  [ tlr_base st1 st1' tll1 ⇒ ?
69  | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
70  ]
71and tll_rel_extract_equal (p: params) (g: list ident)
72  (lg: ident → joint_internal_function p g) (top_f: ident)
73  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
74  t1 ≈ t2 →
75  ∀res.extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 res =
76  extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 res ≝
77  match t1 with
78  [ tll_base ends st1 st1' tal1 co ⇒ ?
79  ]
80and tal_rel_extract_equal (p: params) (g: list ident)
81  (lg: ident → joint_internal_function p g) (top_f: ident)
82  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
83  t1 ≈ t2 →
84  ∀res.extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 res =
85  extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 res ≝
86  match t1 with
87  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
88  | tal_base_return st1 st1' ex cl ⇒ ?
89  | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ?
90  | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ?
91  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
92  ].
93[ cases t2
94  [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim)
95  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs
96  ]
97| cases t2
98  [ #st2 #st2' #tll2 normalize #abs cases abs
99  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res
100    >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res)
101    @(tlr_rel_extract_equal … (proj2 ?? Hsim))
102  ]
103| cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2
104  @(tal_rel_extract_equal … H2)
105| cases t2
106  [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res %
107  | #st2 #st2' #ex' #cl' * #abs destruct (abs)
108  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid *
109    #taa * #H * #G * #K inversion taa in ⊢ ?;
110    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
111    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
112      normalize #abs destruct (abs)
113    ]
114  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize *
115    #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;
116    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
117    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
118      normalize #abs destruct (abs)
119    ]
120  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa
121    * #H * #G * #K inversion taa in ⊢ ?;
122    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
123    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
124      destruct normalize #Hsim destruct (Hsim) (* getting somewhere. Use Hind? *)
125      cases daemon
126    ]
127  ]
128| cases t2
129  [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)
130  | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res %
131  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs)
132  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
133    normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;
134    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
135    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
136      normalize #abs destruct (abs)
137    ]
138  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid
139    * #taa * #H * #G inversion taa in ⊢ ?;
140    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
141    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
142      destruct normalize #Hsim destruct (Hsim)
143      cases daemon (* use Hind again? *) 
144    ]
145  ]
146| cases t2
147  [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #G * #ident_eq * #taa
148    * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2 * #L * #H1
149    [ * * #H3 #H2 #H4 | #H2 ]
150    inversion taa in ⊢ ?;
151    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H3; destruct (H3)
152    | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
153      normalize in H3; destruct (H3)
154    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1)
155    | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
156      normalize in H1; destruct (H1)
157    ]
158  | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs)
159  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid * #G
160    * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2' * #L
161    [* #tl2]
162    inversion taa in ⊢ ?;
163    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
164    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
165      destruct normalize * * #abs destruct (abs)
166    | #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res
167      >(tlr_rel_extract_equal p g lg … H2) destruct (H1)
168      >ident_eq %
169    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
170      destruct normalize * #abs destruct (abs)
171    ]
172  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize
173    * #H1 * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *]
174    #K * #tlr2' * #L [* #tl2]
175    inversion taa in ⊢ ?;
176    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res
177      destruct (H1) >(tlr_rel_extract_equal … H2) >ident_eq
178      (* to do here: destruct tl2: 3 cases by contradiction, 1 by equality and 1 by
179       * not sure yet *) cases daemon
180    |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
181      destruct normalize * * [#abs destruct (abs)] #H2 #res <ident_eq
182      >(tlr_rel_extract_equal … H2) cases daemon (* stumped here *)
183    ]
184  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid *
185    #G * #ident_eq * #taa * #st2mid' * #H * * [2: #stmid'' * ] #K * #tlr2 * #L
186    [* #tl2]
187    inversion taa in ⊢ ?;
188    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res
189      destruct (H1)
190    |2,4: #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
191      destruct normalize * [*] #H1 #H2 [#H3] #res destruct (H1) <ident_eq
192      >(tlr_rel_extract_equal … H2) cases daemon (* stumped again *)
193    ]
194  ]
195| cases t2
196  [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #G * #ident_eq * #taa *
197    #st2mid' * #H * * [#_ | #st2mid''] * #K * #tlr2 * #L [2: * #tl2]
198    inversion taa in ⊢ ?;
199    [1,3: #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #H1 destruct (H1)
200    |2,4: #st2p #st2p' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
201      destruct normalize * * #H1 destruct (H1)
202    ]
203  | #st2 #st2' #ex' #cl' normalize * #st2mid * #G * #ident_eq * #taa * #st2mid'
204    * #H * * [#abs destruct (abs)] #st2mid' * #K * #tlr2 * #L * #tl2
205    inversion taa in ⊢ ?;
206    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
207    | #st2p #st2p' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
208      normalize * * #abs destruct (abs)
209    ]
210  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #st2mid * #G *
211    #ident_eq * #taa * #st2mid' * #H * * [ #_ | #st2mid'' ] * #K * #tlr2' * #L
212    [2: * #tl2]
213    inversion taa in ⊢ ?;
214    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
215      destruct (H1) >ident_eq >(tlr_rel_extract_equal … H3)
216      cases tal1 in H2;
217      [ #ss #sf #ex'' #cl'' #co'' normalize #_ %
218      | #ss #sf #ex'' #cl'' normalize #abs cases abs
219      | #st1p' #st1s #sf #ex'' #cl'' #ar'' #tlr1' #co'' normalize #abs cases abs
220      | #end' #st1p' #st1s' #st1a' #sf #ex'' #cl'' #ar'' #tlr1' #co' #tal1'
221        normalize #abs cases abs
222      | #end' #st1p' #st1i #st1e #ex'' #tal1' #cl'' #co'' normalize
223        cases daemon (* use induction here, but no *)
224      ]
225    |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
226      destruct normalize * * #abs destruct (abs)
227    ]
228  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
229    normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * *
230    [ #H1 | #st2mid''] * #K * #tlr2' * #L [2: * #tl2] inversion taa in ⊢ ?;
231    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
232      destruct (H1) >ident_eq >(tal_rel_extract_equal … H2)
233      >(tlr_rel_extract_equal … H3) %
234    |2,4: #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
235      destruct normalize * * #abs destruct (abs)
236    ]
237  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #G *
238    #ident_eq * #taa * #st2mid' * #H * * [ #He | #st2mid'' ] * #K * #tlr2' * #L
239    [2: * #tl2] inversion taa in ⊢ ?;
240    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
241    |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
242      destruct normalize * * #H1 #H2 #H3 #res destruct (H1)
243      >(tlr_rel_extract_equal … H3) <ident_eq normalize cases daemon
244      (* look further here *)
245    ]
246  ]
247| cases t2
248  [ #st2 #st2' #ex' #cl' #co'
249  | #ss #fs #ex' #cl'
250  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co'
251  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
252  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co'
253  ]
254  normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim)
255]
256qed.
257
258let rec tlr_rel_max_equal (p: params) (g: list ident)
259  (lg: ident → joint_internal_function p g) (top_f: ident)
260  S1 S2 s1 s1' s2 s2' t1 t2 on t1:
261  tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
262  max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) =
263  max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝
264  match t1 with
265  [ tlr_base st1 st1' tll1 ⇒ ?
266  | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
267  ]
268and tll_rel_max_equal (p: params) (g: list ident)
269  (lg: ident → joint_internal_function p g) (top_f: ident)
270  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
271  t1 ≈ t2 →
272  max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) =
273  max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝
274  match t1 with
275  [ tll_base ends st1 st1' tal1 co ⇒ ?
276  ]
277and tal_rel_max_equal (p: params) (g: list ident)
278  (lg: ident → joint_internal_function p g) (top_f: ident)
279  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
280  t1 ≈ t2 →
281  max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) =
282  max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝
283  match t1 with
284  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
285  | tal_base_return st1 st1' ex cl ⇒ ?
286  | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ?
287  | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ?
288  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
289  ].
290[1,2: #Hsim >(tlr_rel_extract_equal … Hsim []) %
291|3: #Hsim >(tll_rel_extract_equal … Hsim []) %
292|*: #Hsim >(tal_rel_extract_equal … Hsim []) %
293]
294qed.
295     
296     
297     
298           
Note: See TracBrowser for help on using the repository browser.