source: src/joint/stacksize.ma @ 2702

Last change on this file since 2702 was 2661, checked in by sacerdot, 8 years ago

stacksize "repaired" by "considering" tailcalls
Some daemons added here and there since many are already in place.

File size: 14.4 KB
Line 
1include "basics/lists/list.ma".
2include "joint/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_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  ].
63
64let 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  ]
74and 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  ]
83and 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
273qed.
274
275let 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  ]
285and 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  ]
294and 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]
312qed.
Note: See TracBrowser for help on using the repository browser.