source: src/joint/stacksize.ma @ 2417

Last change on this file since 2417 was 2417, checked in by boender, 7 years ago
  • reverted changes to StructuredTraces? (shouldn't have been committed yet)
  • updated _jaap files to remove function identifier from cl_call and add an as_call predicate
File size: 13.9 KB
Line 
1include "basics/lists/list.ma".
2include "joint/semantics.ma".
3include "common/Executions.ma".
4
5inductive call_ud (p: params) (globals: list ident): Type [0] ≝
6  | up: joint_internal_function p globals → call_ud p globals    (* call *)
7  | down: joint_internal_function p globals → call_ud p globals. (* return *)
8 
9let rec max_stacksize (p: params) (g: list ident) (fn_list: list (call_ud p g))
10  (curr: nat) (max: nat) on fn_list: nat ≝
11  match fn_list with
12  [ nil      ⇒ max
13  | cons h t ⇒ match h with
14    [ up f   ⇒ let new_stack ≝ curr + joint_if_stacksize … f in
15      if leb max new_stack
16      then max_stacksize … t new_stack new_stack
17      else max_stacksize … t new_stack max
18    | down f ⇒ let new_stack ≝ curr - joint_if_stacksize … f in
19      max_stacksize … t new_stack max
20    ]
21  ].
22
23let rec extract_list_from_tlr (p: params) (g: list ident)
24  (lg: ident → joint_internal_function p g) (top_f: ident)
25  (S: abstract_status) (s,s':S) (tr: trace_label_return S s s')
26  (res: list (call_ud p g)) on tr: list (call_ud p g) ≝
27  match tr with
28  [ tlr_base s1 s2 tll        ⇒
29    extract_list_from_tll … lg top_f … tll res
30  | tlr_step s1 s2 s3 tll tlr ⇒
31    let res' ≝ extract_list_from_tll … lg top_f … tll res in
32    extract_list_from_tlr … lg top_f … tlr res'
33  ]
34and extract_list_from_tll (p: params) (g: list ident)
35  (lg: ident → joint_internal_function p g) (top_f: ident)
36  (S: abstract_status) ends (s,s':S) (tr: trace_label_label S ends s s')
37  (res: list (call_ud p g)) on tr: list (call_ud p g) ≝
38  match tr with
39  [ tll_base ends s1 s2 tal co ⇒
40    extract_list_from_tal … lg top_f … tal res
41  ]
42and extract_list_from_tal (p: params) (g: list ident)
43  (lg: ident → joint_internal_function p g) (top_f: ident)
44  (S: abstract_status) ends (s,s':S) (tr: trace_any_label S ends s s')
45  (res: list (call_ud p g)) on tr: list (call_ud p g) ≝
46  match tr with
47  [ tal_base_not_return s1 s2 ex cl co ⇒ res
48  | tal_base_return s1 s2 ex cl ⇒ down ?? (lg top_f)::res
49  | tal_base_call s1p s1s s2 ex cl f ca ar tlr co ⇒
50    extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res)
51  | tal_step_call end s1p s1s s1a s2 ex cl f ca ar tlr co tal ⇒
52    let res' ≝ extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res) in
53    extract_list_from_tal … lg top_f … tal res'
54  | tal_step_default end s1p s1i s1e ex tal cl co ⇒
55    extract_list_from_tal … lg top_f … tal res
56  ].
57
58let rec tlr_rel_extract_equal (p: params) (g: list ident)
59  (lg: ident → joint_internal_function p g) (top_f: ident)
60  S1 S2 s1 s1' s2 s2' t1 t2 on t1:
61  tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
62  ∀res.extract_list_from_tlr p g lg top_f S1 s1 s1' t1 res =
63  extract_list_from_tlr p g lg top_f S2 s2 s2' t2 res ≝
64  match t1 with
65  [ tlr_base st1 st1' tll1 ⇒ ?
66  | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
67  ]
68and tll_rel_extract_equal (p: params) (g: list ident)
69  (lg: ident → joint_internal_function p g) (top_f: ident)
70  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
71  t1 ≈ t2 →
72  ∀res.extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 res =
73  extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 res ≝
74  match t1 with
75  [ tll_base ends st1 st1' tal1 co ⇒ ?
76  ]
77and tal_rel_extract_equal (p: params) (g: list ident)
78  (lg: ident → joint_internal_function p g) (top_f: ident)
79  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
80  t1 ≈ t2 →
81  ∀res.extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 res =
82  extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 res ≝
83  match t1 with
84  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
85  | tal_base_return st1 st1' ex cl ⇒ ?
86  | tal_base_call st1p st1s st1' ex cl f ca ar tlr1 co ⇒ ?
87  | tal_step_call end st1p st1s st1 st1' ex cl f ca ar tlr1 co tal1 ⇒ ?
88  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
89  ].
90[ cases t2
91  [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim)
92  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs
93  ]
94| cases t2
95  [ #st2 #st2' #tll2 normalize #abs cases abs
96  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res
97    >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res)
98    @(tlr_rel_extract_equal … (proj2 ?? Hsim))
99  ]
100| cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2
101  @(tal_rel_extract_equal … H2)
102| cases t2
103  [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res %
104  | #st2 #st2' #ex' #cl' * #abs destruct (abs)
105  | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #H1 * #st2mid *
106    #taa * #H * #G * #K inversion taa in ⊢ ?;
107    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
108    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
109      normalize #abs destruct (abs)
110    ]
111  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2 normalize *
112    #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;
113    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
114    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
115      normalize #abs destruct (abs)
116    ]
117  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa
118    * #H * #G * #K inversion taa in ⊢ ?;
119    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
120    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
121      destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *)
122    ]
123  ]
124| cases t2
125  [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)
126  | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res %
127  | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #abs destruct (abs)
128  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2
129    normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;
130    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
131    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
132      normalize #abs destruct (abs)
133    ]
134  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid
135    * #taa * #H * #G inversion taa in ⊢ ?;
136    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
137    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
138      destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *) 
139    ]
140  ]
141| cases t2
142  [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #taa
143    * #st2mid' * #H * * [2: #st2mid'' *] #J * #f' * #G * #K * #tlr2 * #L * #H1
144    [ * * #H3 #H2 #H4 | #H2 ]
145    inversion taa in ⊢ ?;
146    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H3; destruct (H3)
147    | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
148      normalize in H3; destruct (H3)
149    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1)
150    | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
151      normalize in H1; destruct (H1)
152    ]
153  | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs)
154  | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #_ * #st2mid *
155    #taa * #st2mid' * #H * * [2: #st2mid'' *] #J * #f'' * #G * #K * #tlr2' * #L
156    inversion taa in ⊢ ?;
157    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #tal2 * * #H1 destruct (H1)
158    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
159      destruct normalize * #tal2 * * #H1 destruct (H1)
160    | #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res
161      >(tlr_rel_extract_equal p g lg f … H2) cases daemon (* use injectivity and H1? *)
162    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
163      destruct normalize * #abs destruct (abs)
164    ]
165  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2
166    normalize * #H1 * #st2mid * #taa * #st2mid' * #H * * [2: #st2mid'' *] #J * #f
167    * #G * #K * #tlr2' * #L
168    inversion taa in ⊢ ?;
169    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #tal2' * * #H1 #H2 #H3 #res
170      cases daemon
171    | #st2p' #st2p'' #st2mid'; #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
172      destruct normalize * #tal2' * * #H1 destruct (H1)
173    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)
174    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
175      destruct normalize * #abs destruct (abs)
176    ]
177  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid *
178    #taa * #st2mid' * #H * * [2: #stmid'' * ] #J * #f * #G * #K * #tlr2 * #L
179    inversion taa in ⊢ ?;
180    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #tal2' * * #H1 destruct (H1)
181    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
182      destruct normalize * #tal2' * * #H1 #H2 #H3 #res cases daemon
183    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)
184    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
185      destruct normalize * #H1 #H2 #res cases daemon (* do something with H1 and H2 *)
186    ]
187  ]
188| cases t2
189  [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #taa * #st2_fun *
190    #st2_after_fun * * [#H | #st2mid'] * #J * #f' * #G * #K * #tlr2 * #L [2: * #tl2]
191    inversion taa in ⊢ ?;
192    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #H1 destruct (H1)
193    | #st2p #st2p' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
194      normalize * * #H1 destruct (H1)
195    | #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
196    | #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
197      normalize * * #abs destruct (abs)
198    ]
199  | #st2 #st2' #ex' #cl' normalize * #st2mid * #taa * #st2mid' * #H *
200    [ * #abs destruct (abs) | * #st2mid'' * #J * #f' * #G * #K * #tlr2 * #L * #tl2
201      inversion taa in ⊢ ?;
202      [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
203      | #st2p #st2p' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
204        normalize * * #abs destruct (abs)
205      ]
206    ]
207  | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #st2mid * #taa
208    * #st2mid' * #H * * [ #_ | #st2mid'' ] * #J * #f'' * #G * #K * #tlr2' * #L [2: * #tl2]
209    inversion taa in ⊢ ?;
210    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
211    | #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
212      destruct normalize * * #abs destruct (abs)
213    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 cases daemon
214    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
215      destruct normalize * * #abs destruct (abs)
216    ]
217  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2
218    normalize * #st2mid * #taa * #st2mid' * #ex'' * * [ #_ | #st2mid''] * #J *
219    #f'' * #G * #K * #tlr2' * #L [2: * #tl2] inversion taa in ⊢ ?;
220    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
221      cases daemon (* injectivity needed again *)
222    | #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
223      destruct normalize * * #abs destruct (abs)
224    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) cases daemon
225      (* huh? *)
226    | #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
227      destruct normalize * * #abs destruct (abs) cases daemon (* huh2? *)
228    ]
229  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #taa *
230    #st2mid' * #H * * [ #He | #st2mid'' ] * #J * #f' * #G * #K * #tlr2' * #L
231    [2: * #tl2] inversion taa in ⊢ ?;
232    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
233    | #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
234      destruct normalize * * #H1 #H2 #H3 #res cases daemon (* look into this *)
235    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
236    | #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
237      destruct normalize * * #H1 #H2 #H3 #res cases daemon
238    ]
239  ]
240| cases t2
241  [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res
242    @(tal_rel_extract_equal p g lg top_f … Hsim)
243  | #ss #fs #ex' #cl' normalize #Hsim #res
244    @(tal_rel_extract_equal p g lg top_f … Hsim)
245  | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize #Hsim #res
246    @(tal_rel_extract_equal p g lg top_f … Hsim)
247  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2
248    normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim)
249  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize #Hsim #res
250    @(tal_rel_extract_equal p g lg top_f … Hsim)
251  ]
252]
253qed.
254
255(* let rec tlr_rel_max_equal (p: params) (g: list ident)
256  (lg: ident → joint_internal_function p g) (top_f: ident)
257  S1 S2 s1 s1' s2 s2' t1 t2 on t1:
258  tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
259  max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) =
260  max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝
261  match t1 with
262  [ tlr_base st1 st1' tll1 ⇒ ?
263  | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
264  ]
265and tll_rel_extract_equal (p: params) (g: list ident)
266  (lg: ident → joint_internal_function p g) (top_f: ident)
267  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
268  t1 ≈ t2 →
269  max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) =
270  max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝
271  match t1 with
272  [ tll_base ends st1 st1' tal1 co ⇒ ?
273  ]
274and tal_rel_extract_equal (p: params) (g: list ident)
275  (lg: ident → joint_internal_function p g) (top_f: ident)
276  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
277  t1 ≈ t2 →
278  max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) =
279  max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝
280  match t1 with
281  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
282  | tal_base_return st1 st1' ex cl ⇒ ?
283  | tal_base_call st1p st1s st1' ex f cl ar tlr1 co ⇒ ?
284  | tal_step_call end st1p st1s st1 st1' ex f cl ar tlr1 co tal1 ⇒ ?
285  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
286  ].
287 cases daemon (* next proof *)
288qed. *)
289     
290     
291     
292           
Note: See TracBrowser for help on using the repository browser.