1 | include "basics/lists/list.ma". |
---|
2 | include "joint/semantics.ma". |
---|
3 | include "common/Executions.ma". |
---|
4 | |
---|
5 | inductive 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 | |
---|
9 | let 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 | |
---|
23 | let 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 | ] |
---|
34 | and 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 | ] |
---|
42 | and 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 f cl 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 f cl 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 | |
---|
58 | let 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 | ] |
---|
68 | and 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 | ] |
---|
77 | and 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 f cl ar tlr1 co ⇒ ? |
---|
87 | | tal_step_call end st1p st1s st1 st1' ex f cl 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' #f' #cl' #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' #f' #cl' #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' #f' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs) |
---|
128 | | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #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 * #f' * #G * #K * #tlr2 * #L * #H1 #H2 inversion taa in ⊢ ?; |
---|
144 | [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1) |
---|
145 | | #st2'' #st2''' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct |
---|
146 | normalize in H1; destruct (H1) |
---|
147 | ] |
---|
148 | | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs) |
---|
149 | | #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid * |
---|
150 | #taa * #st2mid' * #H * #f'' * #G * #K * #tlr2' * #L inversion taa in ⊢ ?; |
---|
151 | [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res |
---|
152 | >(tlr_rel_extract_equal p g lg f … H2) cases daemon (* use injectivity and H1? *) |
---|
153 | | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
---|
154 | destruct normalize * #abs destruct (abs) |
---|
155 | ] |
---|
156 | | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2 |
---|
157 | normalize * #H1 * #st2mid * #taa * #st2mid' * #H * #f * #G * #K * #tlr2' * #L |
---|
158 | inversion taa in ⊢ ?; |
---|
159 | [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs) |
---|
160 | | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
---|
161 | destruct normalize * #abs destruct (abs) |
---|
162 | ] |
---|
163 | | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * |
---|
164 | #taa * #st2mid' * #H * #f * #G * #K * #tlr2 * #L inversion taa in ⊢ ?; |
---|
165 | [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs) |
---|
166 | | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
---|
167 | destruct normalize * #H1 #H2 #res cases daemon (* do something with H1 and H2 *) |
---|
168 | ] |
---|
169 | ] |
---|
170 | | cases t2 |
---|
171 | [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #taa * #st2_fun * #st2_after_fun |
---|
172 | * #H * #f' * #G * #K * #tlr2 * #L * #tl2 inversion taa in ⊢ ?; |
---|
173 | [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) |
---|
174 | | #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct |
---|
175 | normalize * * #abs destruct (abs) |
---|
176 | ] |
---|
177 | | #st2 #st2' #ex' #cl' normalize * #st2mid * #taa * #st2_fun * #st2_after_fun |
---|
178 | * #H * #f' * #G * #K * #tlr2 * #L * #tl2 inversion taa in ⊢ ?; |
---|
179 | [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) |
---|
180 | | #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct |
---|
181 | normalize * * #abs destruct (abs) |
---|
182 | ] |
---|
183 | | #st2p #st2s #st2' #ex' #f' #H #ar' #tlr2 #co' normalize * #st2mid * #taa |
---|
184 | * #st2_fun * #st2_after_fun * #H' * #f'' * #G * #K * #tlr2' * #L * #tl2 |
---|
185 | inversion taa in ⊢ ?; |
---|
186 | [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) |
---|
187 | | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
---|
188 | destruct normalize * * #abs destruct (abs) |
---|
189 | ] |
---|
190 | | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2 |
---|
191 | normalize * #st2mid * #taa * #st2_fun * #st2_after_fun * #H * #f'' * |
---|
192 | #G * #K * #tlr2' * #L * #tl2 inversion taa in ⊢ ?; |
---|
193 | [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res |
---|
194 | >(tlr_rel_extract_equal … H2) cases daemon (* injectivity needed again *) |
---|
195 | | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
---|
196 | destruct normalize * * #abs destruct (abs) |
---|
197 | ] |
---|
198 | | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #taa * |
---|
199 | #st2_fun * #st2_after_fun * #H * #f' * #G * #K * #tlr2' * #L * #tl2 |
---|
200 | inversion taa in ⊢ ?; |
---|
201 | [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) |
---|
202 | | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
---|
203 | destruct normalize * * #H1 #H2 #H3 #res cases daemon (* look into this *) |
---|
204 | ] |
---|
205 | ] |
---|
206 | | cases t2 |
---|
207 | [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res |
---|
208 | @(tal_rel_extract_equal p g lg top_f … Hsim) |
---|
209 | | #ss #fs #ex' #cl' normalize #Hsim #res |
---|
210 | @(tal_rel_extract_equal p g lg top_f … Hsim) |
---|
211 | | #st2p #st2s #st2' #ex' #f' #H #ar' #tlr2 #co' normalize #Hsim #res |
---|
212 | @(tal_rel_extract_equal p g lg top_f … Hsim) |
---|
213 | | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2 |
---|
214 | normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim) |
---|
215 | | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize #Hsim #res |
---|
216 | @(tal_rel_extract_equal p g lg top_f … Hsim) |
---|
217 | ] |
---|
218 | ] |
---|
219 | qed. |
---|
220 | |
---|
221 | let rec tlr_rel_max_equal (p: params) (g: list ident) |
---|
222 | (lg: ident → joint_internal_function p g) (top_f: ident) |
---|
223 | S1 S2 s1 s1' s2 s2' t1 t2 on t1: |
---|
224 | tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 → |
---|
225 | max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) = |
---|
226 | max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝ |
---|
227 | match t1 with |
---|
228 | [ tlr_base st1 st1' tll1 ⇒ ? |
---|
229 | | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ? |
---|
230 | ] |
---|
231 | and tll_rel_extract_equal (p: params) (g: list ident) |
---|
232 | (lg: ident → joint_internal_function p g) (top_f: ident) |
---|
233 | S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: |
---|
234 | t1 ≈ t2 → |
---|
235 | max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) = |
---|
236 | max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝ |
---|
237 | match t1 with |
---|
238 | [ tll_base ends st1 st1' tal1 co ⇒ ? |
---|
239 | ] |
---|
240 | and tal_rel_extract_equal (p: params) (g: list ident) |
---|
241 | (lg: ident → joint_internal_function p g) (top_f: ident) |
---|
242 | S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: |
---|
243 | t1 ≈ t2 → |
---|
244 | max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) = |
---|
245 | max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝ |
---|
246 | match t1 with |
---|
247 | [ tal_base_not_return st1 st1' ex cl co ⇒ ? |
---|
248 | | tal_base_return st1 st1' ex cl ⇒ ? |
---|
249 | | tal_base_call st1p st1s st1' ex f cl ar tlr1 co ⇒ ? |
---|
250 | | tal_step_call end st1p st1s st1 st1' ex f cl ar tlr1 co tal1 ⇒ ? |
---|
251 | | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ? |
---|
252 | ]. |
---|
253 | cases daemon (* next proof *) |
---|
254 | qed. |
---|
255 | |
---|
256 | |
---|
257 | |
---|
258 | |
---|