1 | include "basics/lists/list.ma". |
---|
2 | include "joint/semantics.ma". |
---|
3 | include "common/Executions.ma". |
---|
4 | include "common/StructuredTraces.ma". |
---|
5 | |
---|
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 | ]. |
---|
23 | |
---|
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_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 | |
---|
61 | let 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 | ] |
---|
71 | and 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 | ] |
---|
80 | and 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 | ] |
---|
256 | qed. |
---|
257 | |
---|
258 | (* let 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 | ] |
---|
268 | and 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 | ] |
---|
277 | and 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 f cl ar tlr1 co ⇒ ? |
---|
287 | | tal_step_call end st1p st1s st1 st1' ex f cl ar tlr1 co tal1 ⇒ ? |
---|
288 | | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ? |
---|
289 | ]. |
---|
290 | cases daemon (* next proof *) |
---|
291 | qed. *) |
---|
292 | |
---|
293 | |
---|
294 | |
---|
295 | |
---|