source: src/joint/stacksize.ma @ 2645

Last change on this file since 2645 was 2601, checked in by sacerdot, 7 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 13.5 KB
RevLine 
[2398]1include "basics/lists/list.ma".
[2601]2include "joint/joint_semantics.ma".
[2398]3include "common/Executions.ma".
[2426]4include "common/StructuredTraces.ma".
[2398]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
[2426]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
[2398]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 ⇒ ?
[2426]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 ⇒ ?
[2398]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)
[2426]108  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid *
[2398]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    ]
[2426]114  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize *
[2398]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
[2426]124      destruct normalize #Hsim destruct (Hsim) (* getting somewhere. Use Hind? *)
125      cases daemon
[2398]126    ]
127  ]
128| cases t2
129  [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)
130  | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res %
[2426]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
[2398]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
[2426]142      destruct normalize #Hsim destruct (Hsim)
143      cases daemon (* use Hind again? *) 
[2398]144    ]
145  ]
146| cases t2
[2426]147  [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #G * #ident_eq * #taa
148    * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2 * #L * #H1
[2417]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
[2398]156      normalize in H1; destruct (H1)
157    ]
158  | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs)
[2426]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]
[2417]162    inversion taa in ⊢ ?;
[2426]163    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
[2417]164    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
[2426]165      destruct normalize * * #abs destruct (abs)
[2417]166    | #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res
[2426]167      >(tlr_rel_extract_equal p g lg … H2) destruct (H1)
168      >ident_eq %
[2398]169    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
170      destruct normalize * #abs destruct (abs)
171    ]
[2426]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]
[2398]175    inversion taa in ⊢ ?;
[2426]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 *)
[2398]183    ]
184  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid *
[2426]185    #G * #ident_eq * #taa * #st2mid' * #H * * [2: #stmid'' * ] #K * #tlr2 * #L
186    [* #tl2]
[2417]187    inversion taa in ⊢ ?;
[2426]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 *)
[2398]193    ]
[2426]194  ]
[2398]195| cases t2
[2426]196  [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #G * #ident_eq * #taa *
197    #st2mid' * #H * * [#_ | #st2mid''] * #K * #tlr2 * #L [2: * #tl2]
[2417]198    inversion taa in ⊢ ?;
[2426]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
[2398]208      normalize * * #abs destruct (abs)
209    ]
[2426]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 *)
[2417]224      ]
[2426]225    |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
[2417]226      destruct normalize * * #abs destruct (abs)
[2398]227    ]
[2426]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
[2398]235      destruct normalize * * #abs destruct (abs)
236    ]
[2426]237  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #G *
238    #ident_eq * #taa * #st2mid' * #H * * [ #He | #st2mid'' ] * #K * #tlr2' * #L
[2417]239    [2: * #tl2] inversion taa in ⊢ ?;
[2426]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 *)
[2398]245    ]
246  ]
247| cases t2
[2426]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'
[2398]253  ]
[2426]254  normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim)
[2398]255]
256qed.
257
[2456]258let rec tlr_rel_max_equal (p: params) (g: list ident)
[2398]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  ]
[2426]268and tll_rel_max_equal (p: params) (g: list ident)
[2398]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  ]
[2426]277and tal_rel_max_equal (p: params) (g: list ident)
[2398]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 ⇒ ?
[2456]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 ⇒ ?
[2398]288  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
289  ].
[2456]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.
[2398]295     
296     
297     
[2601]298           
Note: See TracBrowser for help on using the repository browser.