source: LTS/Language.ma @ 3398

Last change on this file since 3398 was 3398, checked in by piccolo, 6 years ago

state relation with stack relation uptaded

File size: 39.8 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "basics/types.ma".
16include "Traces.ma".
17include "basics/lists/list.ma".
18include "../src/utilities/option.ma".
19include "basics/jmeq.ma".
20
21discriminator option.
22
23record instr_params : Type[1] ≝
24{ seq_instr : DeqSet
25; io_instr : DeqSet
26; cond_instr : DeqSet
27; loop_instr : DeqSet
28; act_params_type : DeqSet
29; return_type : DeqSet
30}.
31
32
33inductive Instructions (p : instr_params) : Type[0] ≝
34 | EMPTY : Instructions p
35 | RETURN : return_type p → Instructions p
36 | SEQ : (seq_instr p) → option NonFunctionalLabel → Instructions p → Instructions p
37 | COND : (cond_instr p) → NonFunctionalLabel → Instructions p →
38                 NonFunctionalLabel → Instructions p → Instructions p →
39                       Instructions p
40 | LOOP : (loop_instr p) → NonFunctionalLabel → Instructions p →
41                  NonFunctionalLabel → Instructions p → Instructions p
42 | CALL : FunctionName → (act_params_type p) → option ReturnPostCostLabel →
43            Instructions p → Instructions p
44 | IO : NonFunctionalLabel → (io_instr p) → NonFunctionalLabel → Instructions p →
45             Instructions p.
46
47let rec eq_instructions (p : instr_params) (i : Instructions p)
48 on i : (Instructions p) → bool ≝
49match i with
50[ EMPTY ⇒ λi'.match i' with [ EMPTY ⇒ true | _ ⇒ false ]
51| RETURN x ⇒ λi'.match i' with [ RETURN y ⇒ x == y | _ ⇒ false ]
52| SEQ x lab instr ⇒ λi'.match i' with
53                      [ SEQ y lab' instr' ⇒ x == y ∧ eq_instructions … instr instr' ∧
54                              match lab with [ None ⇒ match lab' with [ None ⇒ true | _ ⇒ false ]
55                                             | Some l1 ⇒ match lab' with [Some l2 ⇒ eq_nf_label l1 l2 | _ ⇒ false]
56                                             ]
57                      | _ ⇒ false
58                      ]
59| COND x ltrue i1 lfalse i2 i3 ⇒ λi'.match i' with
60                          [ COND y ltrue' i1' lfalse' i2' i3' ⇒
61                             x == y ∧ eq_nf_label ltrue ltrue' ∧
62                             eq_instructions … i1 i1' ∧ eq_nf_label lfalse lfalse' ∧
63                             eq_instructions … i2 i2' ∧ eq_instructions … i3 i3'
64                         | _ ⇒ false
65                         ]
66| LOOP x ltrue i1 lfalse i2 ⇒ λi'.match i' with
67              [ LOOP y ltrue' i1' lfalse' i2' ⇒ x == y ∧
68                      eq_instructions … i1 i1' ∧ eq_nf_label ltrue ltrue' ∧
69                      eq_instructions … i2 i2'
70              | _ ⇒ false
71              ]
72| CALL f act_p r_lb i1 ⇒ λi'.match i' with
73             [ CALL f' act_p' r_lb' i1' ⇒ eq_function_name f f' ∧
74                       act_p == act_p' ∧ eq_instructions … i1 i1' ∧
75                       match r_lb with [ None ⇒ match r_lb' with [None ⇒ true | _ ⇒ false]
76                                       | Some z ⇒ match r_lb' with [Some w ⇒  eq_return_cost_lab z w | _ ⇒ false ]
77                                       ]
78            | _ ⇒ false
79            ]
80| IO lin io lout i1 ⇒ λi'.match i' with
81             [ IO lin' io' lout' i1' ⇒ eq_nf_label lin lin' ∧ io == io' ∧
82                                       eq_nf_label lout lout' ∧ eq_instructions … i1 i1'
83             | _ ⇒ false                                       
84             ]
85].
86
87lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) →
88(i1 ≠ i2 → P false) → P (eq_instructions p i1 i2).
89#P #p #i1 elim i1
90[ * normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
91  (* destruct(EQ) gives no choice for ID(instructions_discr) *) cases daemon ]
92cases daemon (*TODO*)
93qed.
94
95record env_params : Type[1] ≝
96{ form_params_type : Type[0]
97}.
98
99record signature (p : env_params) (p' : instr_params) : Type[0] ≝
100{ f_name : FunctionName
101; f_pars : form_params_type p
102; f_ret : return_type p'
103}.
104
105record env_item (p : env_params) (p' : instr_params) : Type[0] ≝
106{ f_sig :> signature p p'
107; f_lab : CallCostLabel
108; f_body : Instructions p'
109}.
110
111record state_params : Type[1] ≝
112{ i_pars : instr_params
113; e_pars : env_params
114; store_type : DeqSet
115}.
116
117coercion i_pars.
118coercion e_pars.
119
120record state (p : state_params) : Type[0] ≝
121{ code : Instructions p
122; cont : list (ActionLabel × (Instructions p))
123; store : store_type p
124; io_info : bool
125}.
126
127definition is_io : ∀p.state p → Prop ≝ λp,st.io_info … st = true.
128
129record sem_state_params (p : state_params) : Type[0] ≝
130{ eval_seq : seq_instr p → state p → option (store_type p)
131; eval_io : io_instr p → state p → option (store_type p)
132; eval_cond_cond : cond_instr p → state p → option (bool × (store_type p))
133; eval_loop_cond : loop_instr p → state p → option (bool × (store_type p))
134; eval_call : signature p p → act_params_type p → state p → option (store_type p)
135; eval_after_return : return_type p → store_type p → option (store_type p)
136; init_store : store_type p
137}.
138
139
140let rec lookup (p : env_params) (p' : instr_params) (l : list (env_item p p'))
141 on l : FunctionName → option (env_item p p') ≝
142match l with
143[ nil ⇒ λ_.None ?
144| cons x xs ⇒  λf.if (eq_function_name f (f_name … x))
145                  then Some ? x
146                  else lookup … xs f
147].
148
149definition is_ret_act : ActionLabel → Prop ≝
150λa.match a with [ret_act _ ⇒ True | _ ⇒ False ].
151
152inductive execute_l (p : state_params) (p' : sem_state_params p) (env : list (env_item p p)) :
153                                         ActionLabel → relation (state p) ≝
154| empty : ∀st,st',hd,tl.(code ? st) = (EMPTY p)→ (cont ? st) = hd :: tl →
155           (code ? st') = \snd hd → (cont … st') = tl → (store … st) = (store … st') →
156           (io_info … st = true → is_non_silent_cost_act (\fst hd)) →  (io_info … st') = false → ¬ is_ret_act (\fst hd) →  execute_l … (\fst hd) st st'
157| seq_sil : ∀st,st',i,cd,s,opt_l.(code ? st) = SEQ … i opt_l cd →
158             eval_seq … p' i st = return s → (code ? st') = cd →
159             (cont … st) = (cont … st') → (store … st') = s →
160             io_info … st = false →  io_info ? st' = false → execute_l … (cost_act opt_l) st st'
161| cond_true : ∀st,st',exp,ltrue,i_true,lfalse,i_false,cd,new_m.
162   (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp st = return 〈true,new_m〉 →
163   cont ? st' = 〈cost_act (None ?),cd〉 ::(cont … st) → code … st' = i_true → store … st' = new_m →
164   io_info … st = false →  io_info … st' = false → execute_l … (cost_act (Some ? ltrue)) st st'
165| cond_false : ∀st,st',exp,ltrue,i_true,lfalse,i_false,cd,new_m.
166   (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp st = return 〈false,new_m〉 →
167   cont ? st' = 〈cost_act (None ?),cd〉 ::(cont … st) → code … st' = i_false → store … st' = new_m →
168   io_info … st = false →  io_info … st' = false → execute_l … (cost_act (Some ? lfalse)) st st'
169| loop_true : ∀st,st',exp,ltrue,i_true,lfalse,i_false,new_m.
170   code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp st = return 〈true,new_m〉 →
171   cont ? st' = 〈cost_act (None ?),LOOP … exp ltrue i_true lfalse i_false〉 :: (cont … st) →
172   code … st' = i_true → store … st' = new_m → io_info … st = false →  io_info … st' = false →
173   execute_l … (cost_act (Some ? ltrue)) st st'
174| loop_false : ∀st,st',exp,ltrue,i_true,lfalse,i_false,new_m.
175   code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp st = return 〈false,new_m〉 →
176   cont ? st' = cont … st → code … st' = i_false → store … st = store … st' →
177   io_info … st = false →  io_info … st' = false → execute_l … (cost_act (Some ? lfalse)) st st'
178| io_in : ∀st,st',lin,io,lout,cd,mem.(code ? st) = IO … lin io lout cd →
179    eval_io … p' io st = return mem → code ? st' = EMPTY p →
180    cont … st' = 〈cost_act (Some ? lout),cd〉 :: (cont … st) → store … st' = mem →
181    io_info … st' = true → execute_l … (cost_act (Some ? lin)) st st'
182| call : ∀st,st',f,act_p,r_lb,cd,mem,env_it.(code ? st) = CALL … f act_p r_lb cd →
183    lookup … env f = return env_it →
184    eval_call ? p' env_it act_p st = return mem →
185    store ? st' = mem → code … st' = f_body … env_it →
186     cont … st' =
187       〈(ret_act r_lb),cd〉 :: (cont … st) → 
188    io_info … st = false →  (io_info … st') = false →
189    execute_l … (call_act f (f_lab ?? env_it)) st st'
190| ret_instr : ∀st,st',r_t,mem,tl',rb,cd.code ? st = RETURN … r_t →
191   cont … st = 〈ret_act rb,cd〉 :: tl' → cont ? st' = tl' →
192   io_info … st = false →  io_info ? st' = false →
193   eval_after_return … p' r_t (store … st) = return mem → code … st' = cd →
194   store … st' = mem → execute_l … (ret_act rb) st st'.
195
196record Program (p : env_params) (p' : instr_params) : Type[0] ≝
197{ env : list (env_item p p')
198; main : Instructions p'
199}.
200
201definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2.True.
202(* bisognerebbe confrontare la coda dell'istruzione corrente e la parte di stack fino alla prima label.
203 match (code … s1) with
204 [ CALL f act_p r_lb i1 ⇒ code … s2 = i1
205 | _ ⇒ False
206 ].
207*)
208
209include "basics/lists/listb.ma".
210include "../src/utilities/hide.ma".
211
212definition operational_semantics : ∀p : state_params.∀p'.Program p p → abstract_status ≝
213λp,p',prog.mk_abstract_status
214                (state p)
215                (execute_l ? p' (env … prog))
216                (is_synt_succ …)
217                (λs.match (code … s) with
218                    [ COND _ _ _ _ _ _ ⇒ cl_jump
219                    | LOOP _ _ _ _ _ ⇒ cl_jump
220                    | EMPTY ⇒ if io_info … s then cl_io else cl_other
221                    | _ ⇒ cl_other
222                    ])
223                (λs.match (code … s) with
224                    [CALL _ _ m _ ⇒ match m with [ Some _ ⇒ true | None ⇒ false ]
225                    | _ ⇒ false
226                    ])
227                (λs.eq_instructions … (code … s) (main … prog) ∧ isnilb … (cont … s) ∧ store … s == init_store … p' ∧ io_info … s)
228                (λs.match (cont … s) with
229                    [ nil ⇒ match (code … s) with
230                            [ EMPTY ⇒ true
231                            | RETURN _ ⇒ true
232                            | _ ⇒ false
233                            ]
234                    | _ ⇒ false
235                    ])
236                ???.
237@hide_prf
238[ #s1 #s2 #l #H #H1 inversion H1 #st #st'
239 [ #hd #tl
240 | #i #cd #s #opt_l
241 |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m
242 |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m
243 | #lin #io #lout #cd #mem
244 | #f #act_p #r_lb #cd #mem #env_it
245 | #r_t #mem #tl #rb #cd
246 ]
247 #EQcode
248 [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQ5 #H2 #EQ' #EQ6 #EQ7
249 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9
250 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9
251 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9
252 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9
253 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9
254 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8
255 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
256 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
257 ]
258 #_ destruct >EQcode in H; normalize nodelta /2 by ex_intro/
259 [ cases(io_info ??) normalize nodelta] #EQ destruct
260| #s1 #s2 #l #H #H1 inversion H1 #st #st'
261 [ #hd #tl
262 | #i #cd #s #opt_l
263 |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m
264 |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m
265 | #lin #io #lout #cd #mem
266 | #f #act_p #r_lb #cd #mem #env_it
267 | #r_t #mem #tl #rb #cd
268 ]
269 #EQcode
270 [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQiost' #H2 #EQ' #EQ6 #EQ7
271 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9
272 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9
273 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9
274 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9
275 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9
276 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost' #EQ6 #EQ7 #EQ8
277 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQiost' #EQ8 #EQ9 #EQ10
278 | #EQ1 #EQ2 #EQ3 #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
279 ]
280 #_ destruct
281 cases(code ? st') in H; normalize nodelta >EQiost' normalize nodelta
282 #eq destruct try (#eq1 destruct) try (#eq2 destruct) try (#eq3 destruct)
283 try (#eq4 destruct) try (#eq5 destruct) try (#eq6 destruct) %{lin} %
284| #s1 #s2 #l #H #H1 inversion H1 #st #st'
285 [ #hd #tl
286 | #i #cd #s #opt_l
287 |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m
288 |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m
289 | #lin #io #lout #cd #mem
290 | #f #act_p #r_lb #cd #mem #env_it
291 | #r_t #mem #tl #rb #cd
292 ]
293 #EQcode
294 [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQiost' #H2 #EQ' #EQ6 #EQ7
295 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9
296 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9
297 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9
298 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9
299 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9
300 | #EQ1 #EQ2 #EQ3 #EQiost #EQiost' #EQ6 #EQ7 #EQ8
301 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost #EQiost' #EQ8 #EQ9 #EQ10
302 | #EQ1 #EQ2 #EQiost #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
303 ]
304 #_ destruct >EQcode in H; normalize nodelta [|*: #EQ destruct]
305 cases(io_info … st) in x; normalize nodelta [2: #_ #EQ destruct]
306 #H3 #_ @H3 %
307]
308qed.
309
310let rec eqb_list (D : DeqSet) (l1 : list D) on l1 : list D → bool ≝
311match l1 with
312[ nil ⇒ λl2.match l2 with [nil ⇒ true | _ ⇒ false ]
313| cons x xs ⇒ λl2.match l2 with [ cons y ys ⇒ x == y ∧ eqb_list … xs ys | _ ⇒ false ]
314].
315
316definition DeqSet_List : DeqSet → DeqSet ≝
317λX.mk_DeqSet (list X) (eqb_list …) ?.
318#x elim x [ * /2 by refl, conj/ #y #ys normalize % #EQ destruct] -x
319#x #xs #IH * [ normalize % #EQ destruct] #y #ys normalize % inversion(x == y)
320#EQ normalize nodelta
321[ #H >(proj1 … (IH ys) H) @eq_f2 [2: %] @(proj1 … (eqb_true …)) assumption
322| #EQ destruct
323| #EQ1 destruct @(proj2 … (IH …)) %
324| #EQ1 destruct <EQ @(proj2 … (eqb_true …)) %
325]
326qed.
327
328unification hint  0 ≔ C;
329    X ≟ DeqSet_List C
330(* ---------------------------------------- *) ⊢
331    list C ≡ carr X.
332
333
334unification hint  0 ≔ D,p1,p2;
335    X ≟ DeqSet_List D
336(* ---------------------------------------- *) ⊢
337    eqb_list D p1 p2 ≡ eqb X p1 p2.
338    check NonFunctionalLabel
339
340definition associative_list : DeqSet → Type[0] → Type[0] ≝
341λA,B.list (A × (list B)).
342
343let rec update_list (A : DeqSet) (B : Type[0]) (l : associative_list A B)
344   on l : A → list B → associative_list A B ≝
345λa,b.match l with
346    [ nil ⇒ [〈a,b〉]
347    | cons x xs ⇒ if (a == (\fst x)) then 〈a,b〉 :: xs
348                  else x :: (update_list … xs a b) 
349    ].
350
351let rec get_element (A :DeqSet) (B : Type[0]) (l: associative_list A B) on l : A → list B ≝
352λa.match l with [ nil ⇒ nil ?
353                | cons x xs ⇒ if (a == \fst x) then \snd x else get_element … xs a
354                ].
355 
356definition fresh_nf_label : ℕ → NonFunctionalLabel × ℕ ≝
357λx.〈a_non_functional_label x,S x〉.
358
359definition fresh_cc_labe : ℕ → CallCostLabel × ℕ ≝
360λx.〈a_call_label x,S x〉.
361
362definition fresh_rc_label : ℕ → ReturnPostCostLabel × ℕ ≝
363λx.〈a_return_cost_label x,S x〉.
364
365record call_post_info (p : instr_params) : Type[0] ≝
366{ gen_labels : list CostLabel
367; t_code : Instructions p
368; fresh : ℕ
369; lab_map : associative_list DEQCostLabel CostLabel
370; lab_to_keep : list CostLabel
371}.
372
373let rec call_post_trans (p : instr_params) (i : Instructions p) (n : ℕ) on i :
374list CostLabel → call_post_info p ≝
375λabs.
376match i with
377[ EMPTY ⇒ mk_call_post_info ? abs (EMPTY …) n (nil ?) (nil ?)
378| RETURN x ⇒ mk_call_post_info ? abs (RETURN … x) n (nil ?) (nil ?)
379| SEQ x lab instr ⇒
380   let ih ≝ call_post_trans … instr n abs in
381   match lab with
382   [ None ⇒ mk_call_post_info ? (gen_labels … ih) (SEQ … x (None ?) (t_code … ih))
383             (fresh … ih) (lab_map … ih) (lab_to_keep … ih)
384   | Some lbl ⇒
385      mk_call_post_info ? (nil ?) (SEQ … x (Some ? lbl) (t_code …  ih)) (fresh … ih)
386      (〈a_non_functional_label lbl,(a_non_functional_label lbl :: (gen_labels … ih))〉 :: (lab_map … ih))
387      (lab_to_keep … ih)
388   ]
389| COND x ltrue i1 lfalse i2 i3 ⇒
390   let ih3 ≝ call_post_trans … i3 n abs in
391   let ih2 ≝ call_post_trans … i2 (fresh … ih3) (gen_labels … ih3) in
392   let ih1 ≝ call_post_trans … i1 (fresh … ih2) (gen_labels … ih3) in
393   mk_call_post_info ? (nil ?) (COND … x ltrue (t_code … ih1) lfalse (t_code … ih2) (t_code … ih3))
394    (fresh … ih1) 
395    (〈a_non_functional_label ltrue,(a_non_functional_label ltrue :: (gen_labels … ih1))〉::
396      〈a_non_functional_label lfalse,(a_non_functional_label lfalse :: (gen_labels … ih2))〉::
397       ((lab_map … ih1) @ (lab_map …  ih2) @ (lab_map … ih3)))
398    ((lab_to_keep … ih1) @ (lab_to_keep … ih2) @ (lab_to_keep … ih3))
399| LOOP x ltrue i1 lfalse i2 ⇒
400   let ih2 ≝ call_post_trans … i2 n abs in
401   let ih1 ≝ call_post_trans … i1 (fresh … ih2) (nil ?) in
402   mk_call_post_info ? (nil ?) (LOOP … x ltrue (t_code … ih1) lfalse (t_code … ih2)) (fresh … ih1)
403    (〈a_non_functional_label lfalse,(a_non_functional_label lfalse :: (gen_labels … ih2))〉 ::
404     〈a_non_functional_label ltrue,(a_non_functional_label ltrue :: (gen_labels … ih1))〉 ::
405      ((lab_map … ih1) @ (lab_map … ih2)))
406    ((lab_to_keep … ih1) @ (lab_to_keep … ih2))
407| CALL f act_p r_lb i1 ⇒
408   let ih ≝ call_post_trans … i1 n abs in
409   match r_lb with
410   [ None ⇒ let 〈l',f''〉 ≝ fresh_rc_label (fresh … ih) in
411       mk_call_post_info ? ((a_return_post l')::(gen_labels … ih))
412         (CALL … f act_p (Some ? l') (t_code … ih))  f'' (lab_map … ih) (lab_to_keep … ih)
413   | Some lbl ⇒
414      mk_call_post_info ? (nil ?) (CALL ? f act_p (Some ? lbl) (t_code … ih)) (fresh … ih)
415       (〈a_return_post lbl,(a_return_post lbl :: (gen_labels … ih))〉 :: (lab_map … ih))
416       (a_return_post lbl :: lab_to_keep … ih)
417   ]
418| IO lin io lout i1 ⇒
419    let ih ≝ call_post_trans … i1 n abs in
420    mk_call_post_info ? (nil ?) (IO ? lin io lout (t_code … ih)) (fresh … ih)
421     (〈a_non_functional_label lout,(a_non_functional_label lout :: (gen_labels … ih))〉 ::
422      〈a_non_functional_label lin,[a_non_functional_label lin]〉 :: (lab_map … ih)) (lab_to_keep … ih)
423].
424
425
426let rec call_post_clean (p : instr_params) (i : Instructions p) on i :
427associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel →
428option ((list CostLabel) × (Instructions p)) ≝
429λm,keep,abs.
430 match i with
431[ EMPTY ⇒ Some ? 〈abs,EMPTY …〉
432| RETURN x ⇒ Some ? 〈abs,RETURN … x〉
433| SEQ x lab instr ⇒
434   ! 〈l,i1〉 ← call_post_clean … instr m keep abs;
435   match lab with
436   [ None ⇒ return 〈l,SEQ … x (None ?) i1〉
437   | Some lbl ⇒ if ((get_element … m lbl) == lbl :: l)
438                then return 〈nil ?,SEQ … x (Some ? lbl) i1〉
439                else None ?
440   ]
441| COND x ltrue i1 lfalse i2 i3 ⇒
442    ! 〈l3,instr3〉 ← call_post_clean … i3 m keep abs;
443    ! 〈l2,instr2〉 ← call_post_clean … i2 m keep l3;
444    ! 〈l1,instr1〉 ← call_post_clean … i1 m keep l3;
445    if ((get_element … m ltrue) == ltrue :: l1) ∧
446       ((get_element … m lfalse) == lfalse :: l2)
447    then return 〈nil ?,COND … x ltrue instr1 lfalse instr2 instr3〉
448    else None ?
449| LOOP x ltrue i1 lfalse i2 ⇒
450   ! 〈l2,instr2〉 ← call_post_clean … i2 m keep abs;
451   ! 〈l1,instr1〉 ← call_post_clean … i1 m keep (nil ?);
452   if ((get_element … m ltrue) == ltrue :: l1) ∧
453      ((get_element … m lfalse) == lfalse :: l2)
454   then return 〈nil ?,LOOP … x ltrue instr1 lfalse instr2〉
455   else None ?
456| CALL f act_p r_lb i1 ⇒
457  ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs;
458  match r_lb with
459  [ None ⇒ return 〈l1,CALL … f act_p (None ?) instr1〉
460  | Some lbl ⇒ if ((a_return_post lbl ∈ keep))
461               then if ((get_element … m lbl) == lbl :: l1)
462                    then return 〈nil ?,CALL … f act_p (Some ? lbl) instr1〉
463                    else None ?
464               else return 〈(a_return_post lbl) :: l1,CALL … f act_p (None ?) instr1〉
465  ]
466| IO lin io lout i1 ⇒
467   ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs;
468   if ((get_element … m lout) == lout :: l1) ∧ ((get_element … m lin) == [lin])
469   then return 〈nil ?,IO … lin io lout instr1〉
470   else None ?   
471].
472
473let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (a : A) (l1 : list B)
474(l2 : list C) (f : A → B → C → A) on l1 : option A≝
475match l1 with
476[ nil ⇒ match l2 with [ nil ⇒ return a | cons y ys ⇒ None ? ]
477| cons x xs ⇒
478        match l2 with
479        [ nil ⇒ None ?
480        | cons y ys ⇒ ! ih ← (foldr2 … a xs ys f);
481                      return f ih x y
482        ]
483].
484
485definition is_silent_cost_act_b : ActionLabel → bool ≝
486λact. match act with
487 [ cost_act x ⇒ match x with [None ⇒ true | _ ⇒ false ] | _ ⇒ false].
488
489definition eq_ActionLabel : ActionLabel → ActionLabel → bool ≝
490λc1,c2.
491match c1 with
492[ call_act f l ⇒ match c2 with [ call_act f' l' ⇒ f == f' ∧ l == l' | _ ⇒ false]
493| ret_act x ⇒ match c2 with [ret_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true | _ ⇒ false]
494                                                      | Some l ⇒ match y with [ Some l' ⇒ l == l' | _ ⇒ false]
495                                                      ]
496                            | _ ⇒ false
497                            ]
498| cost_act x ⇒ match c2 with [cost_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true | _ ⇒ false]
499                                                        | Some l ⇒ match y with [ Some l' ⇒ l == l' | _ ⇒ false]
500                                                        ]
501                             | _ ⇒ false
502                             ]
503| init_act ⇒ match c2 with [init_act ⇒ true | _ ⇒ false]
504].
505
506definition ret_costed_abs : list CostLabel → option ReturnPostCostLabel → option CostLabel ≝
507λkeep,x.
508 match x with
509              [ Some lbl ⇒ if (a_return_post lbl) ∈ keep then return (a_return_post lbl)
510                           else None ?
511              | None ⇒ None ?
512              ].
513
514definition check_continuations : ∀p : instr_params.
515∀l1,l2 : list (ActionLabel × (Instructions p)).
516associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel →
517list (list CostLabel) →  option (Prop × (list CostLabel) × (list (list CostLabel))) ≝
518λp,cont1,cont2,m,keep,abs_top,abs_tail.
519foldr2 ??? 〈True,abs_top,abs_tail〉 cont1 cont2
520 (λx,y,z.
521   let 〈cond,abs_top',abs_tail'〉 ≝ x in
522   match call_post_clean p (\snd z) m keep abs_top' with
523   [ None ⇒ 〈False,nil ?,nil ?〉
524   | Some w ⇒
525      match \fst z with
526       [ ret_act opt_x ⇒
527           match ret_costed_abs keep opt_x with
528           [ Some lbl ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧
529                               get_element … m lbl = lbl :: (\fst w),(nil ?),(nil ?) :: abs_tail'〉
530           | None ⇒
531              〈\fst y = ret_act (None ?) ∧ cond ∧ \snd w = \snd y,(nil ?),(\fst w) :: abs_tail'〉
532           ]
533       | cost_act opt_x ⇒
534           match opt_x with
535           [ None ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y,\fst w,abs_tail'〉
536           | Some xx ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧
537                               get_element … m xx = xx :: (\fst w),(nil ?),abs_tail'〉]
538       | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]).
539(* in input :
540     abs_top is the list of labels to be propageted to the deepest level of the call stack
541     abs_tail are the lists of labels to be propagated to the levels "below" the deepest level
542   in output :
543     abs_top is the list of labels to be propageted from the current level of the call stack
544     abs_tail are the lists of labels to be propagated from the levels "below" the current level
545  *)       
546       
547
548definition state_rel : ∀p.
549associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → list (list CostLabel) →
550relation (state p) ≝ λp,m,keep,abs_top,abs_tail,st1,st2.
551match check_continuations ? (cont ? st1) (cont … st2) m keep (nil ?) (nil ?) with
552[ Some x ⇒ let 〈prf1,abs_top',abs_tail'〉 ≝ x in
553           prf1 ∧ call_post_clean … (code … st2) m keep abs_top' = return 〈abs_top,(code … st1)〉
554           ∧ store … st1 = store … st2 ∧ io_info … st1 = io_info … st2 ∧ abs_tail = abs_tail'
555| None ⇒ False
556].
557
558include "Simulation.ma".
559
560let rec len (S : abstract_status) (st1 : S) (st2 : S) (t : raw_trace S st1 st2)
561on t : ℕ ≝
562match t with
563[ t_base s ⇒ O
564| t_ind s1 s2 s3 l prf lt ⇒ (len … lt) + 1
565].
566(*
567lemma associative_max : ∀n1,n2,n3.max (max n1 n2) n3 = max n1 (max n2 n3).
568#n1 #n2 #n3 normalize @leb_elim normalize
569[ @leb_elim normalize
570  [ #H1 #H2 @leb_elim normalize
571    [ @leb_elim normalize // * #H @⊥ @H assumption 
572    | @leb_elim normalize
573      [ #H3 * #H @⊥ @H @(transitive_le … H1) assumption
574      | * #H @⊥ @H assumption
575      ]
576    ]
577  | #H1 #H2 @leb_elim normalize
578    [ @leb_elim normalize // #_ #H cases H1 #H1 @⊥ @H1 assumption
579    | @leb_elim normalize
580      [ #_ * #H @⊥ @H assumption
581      | * #H @⊥ @H @(transitive_le … H2)
582*)
583let rec compute_max_n (p : instr_params) (i : Instructions p) on i : ℕ ≝
584match i with
585[ EMPTY ⇒ O
586| RETURN x ⇒ O
587| SEQ x lab instr ⇒ let n ≝ compute_max_n … instr in
588                    match lab with
589                    [ None ⇒ n
590                    | Some l ⇒
591                        match l with
592                        [ a_non_functional_label n' ⇒ S (max n n') ]
593                    ]
594| COND x ltrue i1 lfalse i2 i3 ⇒
595  let n1 ≝ compute_max_n … i1 in
596  let n2 ≝ compute_max_n … i2 in
597  let n3 ≝ compute_max_n … i3 in
598  let mx ≝ max (max n1 n2) n3 in
599  match ltrue with
600  [ a_non_functional_label lt ⇒
601    match lfalse with
602    [a_non_functional_label lf ⇒ S (max (max mx lt) lf) ] ]
603| LOOP x ltrue i1 lfalse i2 ⇒
604   let n1 ≝ compute_max_n … i1 in
605   let n2 ≝ compute_max_n … i2 in
606   let mx ≝ max n1 n2 in
607   match ltrue with
608  [ a_non_functional_label lt ⇒
609    match lfalse with
610    [a_non_functional_label lf ⇒ S (max (max mx lt) lf) ] ]
611| CALL f act_p r_lb i1 ⇒
612   let n ≝ compute_max_n … i1 in
613   match r_lb with
614   [ None ⇒ n
615   | Some lbl ⇒ match lbl with [a_return_cost_label l ⇒ S(max l n) ]
616   ]
617| IO lin io lout i1 ⇒
618  let n ≝ compute_max_n … i1 in
619  match lin with
620  [a_non_functional_label l1 ⇒
621    match lout with
622    [a_non_functional_label l2 ⇒ S(max (max n l1) l2) ] ]
623].
624
625
626lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.
627n ≥ compute_max_n … i1 →
628∀info,l.call_post_trans p i1 n l = info →
629call_post_clean … (t_code … info) (lab_map … info) (lab_to_keep … info) l
630 = return 〈gen_labels … info,i1〉.
631cases daemon (*TODO*)
632qed.
633
634definition trans_prog : ∀p,p'.Program p p' →
635(Program p p') × (associative_list DEQCostLabel CostLabel) × (list CostLabel)≝
636λp,p',prog.
637let max_all ≝ foldl … (λn,i.max n (compute_max_n … (f_body … i))) O (env … prog) in
638let 〈t_env,n,m,keep〉 ≝ (foldr ??
639           (λi,x.let 〈t_env,n,m,keep〉 ≝ x in
640           let info ≝ call_post_trans … (f_body … i) n (nil ?) in
641                   〈(mk_env_item ??
642                       (mk_signature ??(f_name ?? i) (f_pars … i) (f_ret … i))
643                       (f_lab … i) (f_body … i)) :: t_env,
644                     fresh … info, 〈a_call (f_lab … i),(a_call (f_lab … i)) :: (gen_labels ? info)〉 ::
645                                     ((lab_map … info) @ m),(lab_to_keep … info) @ keep〉)
646          (〈nil ?,max_all,nil ?,nil ?〉) (env … prog)) in
647〈mk_Program ?? t_env (t_code … (call_post_trans … (main … prog) n (nil ?))),m,keep〉 .
648
649definition map_labels_on_trace :
650(associative_list DEQCostLabel CostLabel) → list CostLabel → list CostLabel ≝
651λm,l.foldr … (λlab,t.(get_element … m lab) @ t) (nil ?) l.
652
653lemma map_labels_on_trace_append:
654 ∀m,l1,l2. map_labels_on_trace m (l1@l2) =
655  map_labels_on_trace m l1 @ map_labels_on_trace m l2.
656 #m #l1 elim l1 // #hd #tl #IH #l2 >associative_append <IH //
657qed.
658
659include "../src/common/Errors.ma".
660
661lemma correctness : ∀p,p',prog.
662let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
663∀s1,s2,s1' : state p.∀abs_top,abs_tail.
664∀t : raw_trace (operational_semantics … p' prog) s1 s2.
665state_rel … m keep abs_top abs_tail s1 s1' →
666∃abs_top',abs_tail'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'.
667state_rel  … m keep abs_top' abs_tail' s2 s2' ∧
668(foldr … (append …) (nil ?) (rev … abs_tail')) @ abs_top' @
669  (map_labels_on_trace m (get_costlabels_of_trace … t)) =
670  (get_costlabels_of_trace … t') @ abs_top @ (foldr … (append …) (nil ?) abs_tail) ∧
671 len … t = len … t'.
672xxxxxx
673#p #p' #prog @pair_elim * #trans_prog #m #keep #EQtrans
674#s1 #s2 #s1' #l #t lapply l -l lapply s1' -s1' elim t
675[ #st #s1' #l #H %{l} %{s1'} %{(t_base …)} % [2: %] %{H} normalize // ]
676#st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
677[ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore
678  #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #_ destruct #tl #IH #s1' #l1
679  whd in match state_rel in ⊢ (% → ?); normalize nodelta >EQcont11
680  whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????);
681  inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1'
682  normalize nodelta change with (check_continuations ??????) in match (foldr2 ???????);
683  inversion(check_continuations ??????) [ #_ *] * #H1 #l2 #EQHl2
684  >m_return_bind normalize nodelta inversion (call_post_clean ?????) [ #_ **** ]
685  * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta
686  cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta
687  [1,4: [ #x #y ] #_ (*#_ #_ #_ #H*) ****
688  | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] *****[|*] #EQ @⊥ >EQ in Hl1;
689    normalize * /2/ ] *
690  [ #EQconts1' normalize nodelta ***** #EQ destruct(EQ)
691    #HH1 #EQ destruct(EQ) >EQcode11 inversion(code … s1')
692    [
693    | #x
694    | #seq #lbl #i #_
695    | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
696    | #cond #ltrue #i1 #lfalse #i2 #_ #_
697    | #f #act_p #ret_post #i #_
698    | #l_in #io #l_out #i #_
699    ]
700    [|*: #_ whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)]
701         cases(call_post_clean ?????) normalize nodelta
702         [1,3,5,7,9: #EQ destruct(EQ)] cases daemon (* da fare assurdi!!!*) ]
703    #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11
704    cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l1 …)
705    [2: whd whd in match check_continuations; normalize nodelta
706    change with (check_continuations ??????) in match (foldr2 ???????);  >EQHl2
707        normalize nodelta % // % // % // @EQcode_c_st12 ]
708    #l3 * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen %{l3} %{st3'}
709    %{(t_ind … (cost_act (None ?)) …  t')}
710    [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉)
711      [3: assumption |4: assumption |*:] /3 by nmk/ ]
712    % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'}
713    whd in match (get_costlabels_of_trace ????);
714    whd in match (get_costlabels_of_trace ????); >EQcosts %
715  | #lbl #EQconts1' normalize nodelta ****** #EQ destruct(EQ)
716    #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 inversion(code … s1')
717    [
718    | #x
719    | #seq #lbl #i #_
720    | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
721    | #cond #ltrue #i1 #lfalse #i2 #_ #_
722    | #f #act_p #ret_post #i #_
723    | #l_in #io #l_out #i #_
724    ]
725    [|*: #_ whd in ⊢ (??%% → ?); #EQ cases daemon (* da fare assurdi !!!*) ]
726    #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio
727    cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l3 …)
728    [2: whd whd in match check_continuations; normalize nodelta
729       change with (check_continuations ??????) in match (foldr2 ???????);  >EQHl2
730        normalize nodelta % // % // % // @EQcode_c_st12 ]
731    #l3' * #st3' * #t' ** #Hst3st3' #EQcost #EQlen %{l3'} %{st3'}
732    %{(t_ind … (cost_act (Some ? lbl)) … t')}
733    [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉)
734      [3: assumption |4: assumption |*:] /3 by nmk/ ]
735    % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'}
736    whd in match (get_costlabels_of_trace ????);
737    whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
738    whd in match map_labels_on_trace; normalize nodelta
739    whd in match (foldr ?????);
740    change with (map_labels_on_trace ??) in match (foldr ?????); >EQget_el
741    whd in match (append ???); whd in match (append ???) in ⊢ (???%); @eq_f
742    whd in match (append ???) in ⊢ (??(???%)(??%?)); @EQcost
743  ]   
744| #seq #i #store * [| #lbl] #EQcode11 #EQstore #EQ destruct(EQ) #EQcont
745  #EQ destruct(EQ) #Hio_st11 #Hio_st12 #EQ destruct(EQ) #EQ1 #EQ2 destruct(EQ1 EQ2)
746  #EQ destruct(EQ) #tl #IH #st3 #l1 whd in ⊢ (% → ?);
747  inversion(check_continuations ?????) [1,3: #_ *] * #H1 #l2
748  [ >EQcont in ⊢ (% → ?); | >EQcont in ⊢ (% → ?); ] #EQcheck normalize nodelta
749  *** #HH1 [ >EQcode11 in ⊢ (% → ?); | >EQcode11 in ⊢ (% → ?); ]
750  inversion(code … st3)
751  [1,2,4,5,6,7,8,9,11,12,13,14: (*assurdi da fare *) cases daemon ]
752  #seq1 #opt_l #i1 #_ #EQcode_st3 change with (m_bind ?????) in ⊢ (??%? → ?);
753  cases daemon
754|8: #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
755    #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3
756    destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #IH #st1' #l1 whd in ⊢ (% → ?);
757    inversion(check_continuations ??????) [1,3: #_ *] * #H1 #l2 #EQcheck
758    normalize nodelta *** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1')
759    [1,2,3,4,5,7: (*assurdi da fare*) cases daemon] #f' #act_p' #opt_l' #i' #_
760    #EQcode_st1' #EQclean #EQstore #EQio
761    cut(∃env_it',n.lookup p p (env … trans_prog) f = return env_it' ∧
762          t_code … (call_post_trans … (f_body … env_it) n (nil ?)) = f_body … env_it')
763    [1,3: cases daemon (*TODO*) ] * #env_it' * #fresh' * #EQenv_it' #EQtrans
764    cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) l2 …)
765    [2: whd >EQcont12 change with (m_bind ??? (check_continuations ??????) ?) in match (check_continuations ??????);
766        >EQcheck >m_return_bind change with (m_bind ?????) in EQclean : (??%?);
767    inversion(call_post_clean ?????) in EQclean; [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
768    * #l3 #i'' #EQi'' >m_return_bind cases opt_l' in EQcode_st1'; [| #lbl'] #EQcode_st1'
769    normalize nodelta
770    [2: inversion(memb ???) normalize nodelta #Hlbl_keep
771        [ inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
772          #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta
773          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_
774          lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta
775          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' l3)
776          #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
777          #EQ destruct(EQ) whd in match ret_costed_abs; normalize nodelta >Hlbl_keep
778          normalize nodelta % // % // % [ % // % // % //] >EQcode12 <EQtrans
779          cases daemon (*TODO*)
780        | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
781          whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta
782          % // % // % [ % // % //]  >EQcode12 <EQtrans
783           * [ #_ #l3'
784    cases(bind_inversion ????? H) in ⊢ ?;
785
786   
787    >EQcost normalize
788   
789    %{l1}
790  xxxxxxxx
791   whd in match is_silent_cost_act_b; normalize nodelta
792    cases lab1 in H Hio11; normalize nodelta
793    [1,2,4: [1,2: #x [ #y]] #H #Hio11 #EQ destruct]
794    * normalize nodelta [2: #x #H #Hio11 #EQ destruct] #H #Hio11 #_
795    inversion(call_post_clean ?????)
796    [ #_ *** ] * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta *****
797    #EQ destruct(EQ) #HH1 #EQ destruct(EQ) >EQcode11
798    whd in match (call_post_clean ?????) in ⊢ (% → ?); whd in ⊢ (??%% → ?);
799    inversion(code … s1')
800    [| #x #EQ1 normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
801       destruct(EQ) |*: cases daemon (*ASSURDI!!*)] #EQcode_s1'
802    normalize in ⊢ (% → ?); #EQ destruct(EQ) #EQstore #EQio
803    cases(IH (mk_state ? new_code' new_cont' (store … s1') false)  l1 ?)
804    [2: whd whd in match check_continuations; normalize nodelta >EQHl2
805        normalize nodelta % // % // >EQcode_c_st12 % // ] #l3 * #st3' * #t' **
806    #Hst3st12' #EQcost #EQlen %{l3} %{st3'} %{(t_ind … (cost_act (None ?)) … t')}
807    [ whd @(empty ????? 〈(cost_act (None ?)),?〉)
808      [3: @hide_prf assumption |4: @hide_prf @EQconts1' |*: ] @hide_prf //
809      [ <EQio #H2 @⊥ lapply(Hio11 H2) * #F #eq destruct | % *]  ] %
810    [ %{Hst3st12'} whd in match (get_costlabels_of_trace ????); 
811      whd in match (get_costlabels_of_trace ????) in ⊢ (???%); //
812    | whd in match (len ????); whd in match (len ????) in ⊢ (???%);
813      >EQlen %
814    ]
815  | #non_sil_lab1 normalize nodelta inversion(call_post_clean ?????) [ #_ ****]
816    * #l3 #code' #EQcall' normalize nodelta inversion(ret_costed_abs ??)
817    [2: #x #H2 @⊥ cases lab1 in Hl1 H2; normalize
818        [ #f #c #_
819        | #x * #ABS @⊥ @ABS %
820        | #x #_
821        | #_
822        ]
823        #EQ destruct(EQ) ]
824    #Hlab1 normalize nodelta ***** #EQ destruct(EQ) #HH1 #EQ destruct(EQ)
825    >EQcode11  inversion(code … s1')
826    [| #x #EQ1 normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
827       destruct(EQ) |*: cases daemon (*ASSURDI!!*)] #EQcode_s1'
828    normalize in ⊢ (% → ?); #EQ destruct(EQ) #EQstore #EQio
829    cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l1 ?)
830    [2: whd whd in match check_continuations; normalize nodelta >EQHl2
831        normalize nodelta % // % // % // >EQcall' % ] #l4 * #st3' * #t' **
832        #Hst3st3' #EQcost #EQlen %{l4} %{st3'} %{(t_ind … lab1 … t')}
833        [ whd @(empty ????? 〈lab1,?〉)
834        [3: @hide_prf assumption |4: assumption |*:] @hide_prf // #H3 @Hio11 >EQio @H3]
835        % [2: whd in match (len ????); whd in match (len ????) in ⊢ (???%);
836              >EQlen % ]
837        %{Hst3st3'} >associative_append <EQcost <associative_append
838        >map_labels_on_trace_append <associative_append @eq_f2 //
839        cases new_code' in EQcall';
840        [| #y | #seq #opt_l #i1 | #cond #ltrue #i_true #lfalse #i_false #i1
841         | #cond #ltrue #i_true #lfalse #ifalse | #f #act_p #ret_opt #i | #l_in #io #l_out #i ]
842        whd in match (call_post_clean ?????);
843        [1,2: #EQ destruct(EQ) //
844       
845       
846         whd in match (get_costlabels_of_trace ??? ?) in ⊢ (??%%);
847       
848         @eq_f2  whd in ⊢ (??%?);
849         
850 
851 
852cases daemon (*TODO*)
853qed.
Note: See TracBrowser for help on using the repository browser.