source: LTS/Language.ma @ 3400

Last change on this file since 3400 was 3400, checked in by piccolo, 6 years ago
File size: 56.4 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
117record state (p : state_params) : Type[0] ≝
118{ code : Instructions p
119; cont : list (ActionLabel × (Instructions p))
120; store : store_type p
121; io_info : bool
122}.
123
124definition is_io : ∀p.state p → Prop ≝ λp,st.io_info … st = true.
125
126record sem_state_params (p : state_params) : Type[0] ≝
127{ eval_seq : seq_instr p → state p → option (store_type p)
128; eval_io : io_instr p → state p → option (store_type p)
129; eval_cond_cond : cond_instr p → state p → option (bool × (store_type p))
130; eval_loop_cond : loop_instr p → state p → option (bool × (store_type p))
131; eval_call : signature p p → act_params_type p → store_type p → option (store_type p)
132; eval_after_return : return_type p → store_type p → option (store_type p)
133; init_store : store_type p
134}.
135
136
137let rec lookup (p : env_params) (p' : instr_params) (l : list (env_item p p'))
138 on l : FunctionName → option (env_item p p') ≝
139match l with
140[ nil ⇒ λ_.None ?
141| cons x xs ⇒  λf.if (eq_function_name f (f_name … x))
142                  then Some ? x
143                  else lookup … xs f
144].
145
146definition is_ret_act : ActionLabel → Prop ≝
147λa.match a with [ret_act _ ⇒ True | _ ⇒ False ].
148
149inductive execute_l (p : state_params) (p' : sem_state_params p) (env : list (env_item p p)) :
150                                         ActionLabel → relation (state p) ≝
151| empty : ∀st,st',hd,tl.(code ? st) = (EMPTY p)→ (cont ? st) = hd :: tl →
152           (code ? st') = \snd hd → (cont … st') = tl → (store … st) = (store … st') →
153           (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'
154| seq_sil : ∀st,st',i,cd,s,opt_l.(code ? st) = SEQ … i opt_l cd →
155             eval_seq … p' i st = return s → (code ? st') = cd →
156             (cont … st) = (cont … st') → (store … st') = s →
157             io_info … st = false →  io_info ? st' = false → execute_l … (cost_act opt_l) st st'
158| cond_true : ∀st,st',exp,ltrue,i_true,lfalse,i_false,cd,new_m.
159   (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp st = return 〈true,new_m〉 →
160   cont ? st' = 〈cost_act (None ?),cd〉 ::(cont … st) → code … st' = i_true → store … st' = new_m →
161   io_info … st = false →  io_info … st' = false → execute_l … (cost_act (Some ? ltrue)) st st'
162| cond_false : ∀st,st',exp,ltrue,i_true,lfalse,i_false,cd,new_m.
163   (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp st = return 〈false,new_m〉 →
164   cont ? st' = 〈cost_act (None ?),cd〉 ::(cont … st) → code … st' = i_false → store … st' = new_m →
165   io_info … st = false →  io_info … st' = false → execute_l … (cost_act (Some ? lfalse)) st st'
166| loop_true : ∀st,st',exp,ltrue,i_true,lfalse,i_false,new_m.
167   code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp st = return 〈true,new_m〉 →
168   cont ? st' = 〈cost_act (None ?),LOOP … exp ltrue i_true lfalse i_false〉 :: (cont … st) →
169   code … st' = i_true → store … st' = new_m → io_info … st = false →  io_info … st' = false →
170   execute_l … (cost_act (Some ? ltrue)) st st'
171| loop_false : ∀st,st',exp,ltrue,i_true,lfalse,i_false,new_m.
172   code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp st = return 〈false,new_m〉 →
173   cont ? st' = cont … st → code … st' = i_false → store … st = store … st' →
174   io_info … st = false →  io_info … st' = false → execute_l … (cost_act (Some ? lfalse)) st st'
175| io_in : ∀st,st',lin,io,lout,cd,mem.(code ? st) = IO … lin io lout cd →
176    eval_io … p' io st = return mem → code ? st' = EMPTY p →
177    cont … st' = 〈cost_act (Some ? lout),cd〉 :: (cont … st) → store … st' = mem →
178    io_info … st' = true → execute_l … (cost_act (Some ? lin)) st st'
179| call : ∀st,st',f,act_p,r_lb,cd,mem,env_it.(code ? st) = CALL … f act_p r_lb cd →
180    lookup … env f = return env_it →
181    eval_call ? p' env_it act_p (store … st) = return mem →
182    store ? st' = mem → code … st' = f_body … env_it →
183     cont … st' =
184       〈(ret_act r_lb),cd〉 :: (cont … st) → 
185    io_info … st = false →  (io_info … st') = false →
186    execute_l … (call_act f (f_lab ?? env_it)) st st'
187| ret_instr : ∀st,st',r_t,mem,tl',rb,cd.code ? st = RETURN … r_t →
188   cont … st = 〈ret_act rb,cd〉 :: tl' → cont ? st' = tl' →
189   io_info … st = false →  io_info ? st' = false →
190   eval_after_return … p' r_t (store … st) = return mem → code … st' = cd →
191   store … st' = mem → execute_l … (ret_act rb) st st'.
192   
193let rec get_labels_of_code (p : instr_params) (i : Instructions p) on i : list CostLabel ≝
194match i with
195[ EMPTY ⇒ [ ]
196| RETURN x ⇒ [ ]
197| SEQ x lab instr ⇒ let ih ≝ get_labels_of_code … instr in
198  match lab with [ None ⇒ ih | Some lbl ⇒ a_non_functional_label lbl :: ih ]
199| COND x ltrue i1 lfalse i2 i3 ⇒
200   let ih3 ≝ get_labels_of_code … i3 in
201   let ih2 ≝ get_labels_of_code … i2 in
202   let ih1 ≝ get_labels_of_code … i1 in
203   ltrue :: lfalse :: (ih1 @ ih2 @ih3)
204| LOOP x ltrue i1 lfalse i2 ⇒
205   let ih2 ≝ get_labels_of_code … i2 in
206   let ih1 ≝ get_labels_of_code … i1 in
207   a_non_functional_label ltrue :: a_non_functional_label lfalse :: (ih1 @ ih2)
208| CALL f act_p r_lb i1 ⇒
209   let ih1 ≝ get_labels_of_code … i1 in
210   match r_lb with [ None ⇒ ih1 | Some lbl ⇒ a_return_post lbl :: ih1]
211| IO lin io lout i1 ⇒
212   let ih1 ≝ get_labels_of_code … i1 in
213   a_non_functional_label lin :: a_non_functional_label lout :: ih1
214].
215
216include "basics/lists/listb.ma".
217include "../src/utilities/hide.ma".
218
219let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝
220match l with
221[ nil ⇒ True
222| cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs
223].
224
225lemma no_duplicates_append_r : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) →
226no_duplicates … l2.
227#A #l1 elim l1 // #x #xs normalize #IH #l2 * /2/
228qed.
229
230lemma no_duplicates_append_l : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) →
231no_duplicates … l1.
232#A #l1 elim l1 // #x #xs normalize #IH #l2 * #H1 #H2 % [2: /2/ ]
233inversion(x ∈ xs @l2) in H1; normalize [ #_ * #H @⊥ @H %] #H1 #_
234% inversion(x ∈ xs) normalize [2: //] #H3 #_ >(memb_append_l1 … H3) in H1;
235#EQ destruct(EQ)
236qed.
237   
238record Program (p : env_params) (p' : instr_params) : Type[0] ≝
239{ env : list (env_item p p')
240; main : Instructions p'
241}.
242
243
244definition no_duplicates_labels : ∀p,p'.Program p p' → Prop ≝
245λp,p',prog.
246   no_duplicates …
247    (foldr … (λitem,acc.((a_call (f_lab … item)) :: get_labels_of_code … (f_body … item)) @ acc) (get_labels_of_code … (main … prog)) (env … prog)).
248
249lemma no_duplicates_domain_of_fun:
250 ∀p,p',prog.no_duplicates_labels … prog →
251 ∀f,env_it.lookup p p' (env … prog) f = return env_it →
252 no_duplicates … (get_labels_of_code … (f_body … env_it)).
253#p #p' * #env elim env [ #main normalize #_ #f #env_it #EQ destruct(EQ)]
254#x #xs #IH #main whd in ⊢ (% → ?); whd in match (foldr ?????); #H #f #env_it
255whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta
256[ whd in ⊢ (? → ???% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) cases H #_ /2/ ]
257#H1 #EQenv_it @IH cases H /2/
258qed.
259
260
261definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2.True.
262(* bisognerebbe confrontare la coda dell'istruzione corrente e la parte di stack fino alla prima label.
263 match (code … s1) with
264 [ CALL f act_p r_lb i1 ⇒ code … s2 = i1
265 | _ ⇒ False
266 ].
267*)
268
269definition operational_semantics : ∀p : state_params.∀p'.Program p p → abstract_status ≝
270λp,p',prog.mk_abstract_status
271                (state p)
272                (execute_l ? p' (env … prog))
273                (is_synt_succ …)
274                (λs.match (code … s) with
275                    [ COND _ _ _ _ _ _ ⇒ cl_jump
276                    | LOOP _ _ _ _ _ ⇒ cl_jump
277                    | EMPTY ⇒ if io_info … s then cl_io else cl_other
278                    | _ ⇒ cl_other
279                    ])
280                (λs.match (code … s) with
281                    [CALL _ _ m _ ⇒ match m with [ Some _ ⇒ true | None ⇒ false ]
282                    | _ ⇒ false
283                    ])
284                (λs.eq_instructions … (code … s) (main … prog) ∧ isnilb … (cont … s) ∧ store … s == init_store … p' ∧ io_info … s)
285                (λs.match (cont … s) with
286                    [ nil ⇒ match (code … s) with
287                            [ EMPTY ⇒ true
288                            | RETURN _ ⇒ true
289                            | _ ⇒ false
290                            ]
291                    | _ ⇒ false
292                    ])
293                ???.
294@hide_prf
295[ #s1 #s2 #l #H #H1 inversion H1 #st #st'
296 [ #hd #tl
297 | #i #cd #s #opt_l
298 |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m
299 |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m
300 | #lin #io #lout #cd #mem
301 | #f #act_p #r_lb #cd #mem #env_it
302 | #r_t #mem #tl #rb #cd
303 ]
304 #EQcode
305 [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQ5 #H2 #EQ' #EQ6 #EQ7
306 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9
307 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9
308 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9
309 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9
310 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9
311 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8
312 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
313 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
314 ]
315 #_ destruct >EQcode in H; normalize nodelta /2 by ex_intro/
316 [ cases(io_info ??) normalize nodelta] #EQ destruct
317| #s1 #s2 #l #H #H1 inversion H1 #st #st'
318 [ #hd #tl
319 | #i #cd #s #opt_l
320 |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m
321 |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m
322 | #lin #io #lout #cd #mem
323 | #f #act_p #r_lb #cd #mem #env_it
324 | #r_t #mem #tl #rb #cd
325 ]
326 #EQcode
327 [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQiost' #H2 #EQ' #EQ6 #EQ7
328 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9
329 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9
330 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9
331 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9
332 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9
333 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost' #EQ6 #EQ7 #EQ8
334 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQiost' #EQ8 #EQ9 #EQ10
335 | #EQ1 #EQ2 #EQ3 #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
336 ]
337 #_ destruct
338 cases(code ? st') in H; normalize nodelta >EQiost' normalize nodelta
339 #eq destruct try (#eq1 destruct) try (#eq2 destruct) try (#eq3 destruct)
340 try (#eq4 destruct) try (#eq5 destruct) try (#eq6 destruct) %{lin} %
341| #s1 #s2 #l #H #H1 inversion H1 #st #st'
342 [ #hd #tl
343 | #i #cd #s #opt_l
344 |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m
345 |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m
346 | #lin #io #lout #cd #mem
347 | #f #act_p #r_lb #cd #mem #env_it
348 | #r_t #mem #tl #rb #cd
349 ]
350 #EQcode
351 [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQiost' #H2 #EQ' #EQ6 #EQ7
352 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9
353 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9
354 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9
355 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9
356 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9
357 | #EQ1 #EQ2 #EQ3 #EQiost #EQiost' #EQ6 #EQ7 #EQ8
358 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost #EQiost' #EQ8 #EQ9 #EQ10
359 | #EQ1 #EQ2 #EQiost #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
360 ]
361 #_ destruct >EQcode in H; normalize nodelta [|*: #EQ destruct]
362 cases(io_info … st) in x; normalize nodelta [2: #_ #EQ destruct]
363 #H3 #_ @H3 %
364]
365qed.
366
367let rec eqb_list (D : DeqSet) (l1 : list D) on l1 : list D → bool ≝
368match l1 with
369[ nil ⇒ λl2.match l2 with [nil ⇒ true | _ ⇒ false ]
370| cons x xs ⇒ λl2.match l2 with [ cons y ys ⇒ x == y ∧ eqb_list … xs ys | _ ⇒ false ]
371].
372
373definition DeqSet_List : DeqSet → DeqSet ≝
374λX.mk_DeqSet (list X) (eqb_list …) ?.
375#x elim x [ * /2 by refl, conj/ #y #ys normalize % #EQ destruct] -x
376#x #xs #IH * [ normalize % #EQ destruct] #y #ys normalize % inversion(x == y)
377#EQ normalize nodelta
378[ #H >(proj1 … (IH ys) H) @eq_f2 [2: %] @(proj1 … (eqb_true …)) assumption
379| #EQ destruct
380| #EQ1 destruct @(proj2 … (IH …)) %
381| #EQ1 destruct <EQ @(proj2 … (eqb_true …)) %
382]
383qed.
384
385unification hint  0 ≔ C;
386    X ≟ DeqSet_List C
387(* ---------------------------------------- *) ⊢
388    list C ≡ carr X.
389
390
391unification hint  0 ≔ D,p1,p2;
392    X ≟ DeqSet_List D
393(* ---------------------------------------- *) ⊢
394    eqb_list D p1 p2 ≡ eqb X p1 p2.
395    check NonFunctionalLabel
396
397definition associative_list : DeqSet → Type[0] → Type[0] ≝
398λA,B.list (A × (list B)).
399
400let rec update_list (A : DeqSet) (B : Type[0]) (l : associative_list A B)
401   on l : A → list B → associative_list A B ≝
402λa,b.match l with
403    [ nil ⇒ [〈a,b〉]
404    | cons x xs ⇒ if (a == (\fst x)) then 〈a,b〉 :: xs
405                  else x :: (update_list … xs a b) 
406    ].
407
408let rec get_element (A :DeqSet) (B : Type[0]) (l: associative_list A B) on l : A → list B ≝
409λa.match l with [ nil ⇒ nil ?
410                | cons x xs ⇒ if (a == \fst x) then \snd x else get_element … xs a
411                ].
412 
413definition fresh_nf_label : ℕ → NonFunctionalLabel × ℕ ≝
414λx.〈a_non_functional_label x,S x〉.
415
416definition fresh_cc_labe : ℕ → CallCostLabel × ℕ ≝
417λx.〈a_call_label x,S x〉.
418
419definition fresh_rc_label : ℕ → ReturnPostCostLabel × ℕ ≝
420λx.〈a_return_cost_label x,S x〉.
421
422record call_post_info (p : instr_params) : Type[0] ≝
423{ gen_labels : list CostLabel
424; t_code : Instructions p
425; fresh : ℕ
426; lab_map : associative_list DEQCostLabel CostLabel
427; lab_to_keep : list CostLabel
428}.
429
430let rec call_post_trans (p : instr_params) (i : Instructions p) (n : ℕ) on i :
431list CostLabel → call_post_info p ≝
432λabs.
433match i with
434[ EMPTY ⇒ mk_call_post_info ? abs (EMPTY …) n (nil ?) (nil ?)
435| RETURN x ⇒ mk_call_post_info ? abs (RETURN … x) n (nil ?) (nil ?)
436| SEQ x lab instr ⇒
437   let ih ≝ call_post_trans … instr n abs in
438   match lab with
439   [ None ⇒ mk_call_post_info ? (gen_labels … ih) (SEQ … x (None ?) (t_code … ih))
440             (fresh … ih) (lab_map … ih) (lab_to_keep … ih)
441   | Some lbl ⇒
442      mk_call_post_info ? (nil ?) (SEQ … x (Some ? lbl) (t_code …  ih)) (fresh … ih)
443      (〈a_non_functional_label lbl,(a_non_functional_label lbl :: (gen_labels … ih))〉 :: (lab_map … ih))
444      (lab_to_keep … ih)
445   ]
446| COND x ltrue i1 lfalse i2 i3 ⇒
447   let ih3 ≝ call_post_trans … i3 n abs in
448   let ih2 ≝ call_post_trans … i2 (fresh … ih3) (gen_labels … ih3) in
449   let ih1 ≝ call_post_trans … i1 (fresh … ih2) (gen_labels … ih3) in
450   mk_call_post_info ? (nil ?) (COND … x ltrue (t_code … ih1) lfalse (t_code … ih2) (t_code … ih3))
451    (fresh … ih1) 
452    (〈a_non_functional_label ltrue,(a_non_functional_label ltrue :: (gen_labels … ih1))〉::
453      〈a_non_functional_label lfalse,(a_non_functional_label lfalse :: (gen_labels … ih2))〉::
454       ((lab_map … ih1) @ (lab_map …  ih2) @ (lab_map … ih3)))
455    ((lab_to_keep … ih1) @ (lab_to_keep … ih2) @ (lab_to_keep … ih3))
456| LOOP x ltrue i1 lfalse i2 ⇒
457   let ih2 ≝ call_post_trans … i2 n abs in
458   let ih1 ≝ call_post_trans … i1 (fresh … ih2) (nil ?) in
459   mk_call_post_info ? (nil ?) (LOOP … x ltrue (t_code … ih1) lfalse (t_code … ih2)) (fresh … ih1)
460    (〈a_non_functional_label lfalse,(a_non_functional_label lfalse :: (gen_labels … ih2))〉 ::
461     〈a_non_functional_label ltrue,(a_non_functional_label ltrue :: (gen_labels … ih1))〉 ::
462      ((lab_map … ih1) @ (lab_map … ih2)))
463    ((lab_to_keep … ih1) @ (lab_to_keep … ih2))
464| CALL f act_p r_lb i1 ⇒
465   let ih ≝ call_post_trans … i1 n abs in
466   match r_lb with
467   [ None ⇒ let 〈l',f''〉 ≝ fresh_rc_label (fresh … ih) in
468       mk_call_post_info ? ((a_return_post l')::(gen_labels … ih))
469         (CALL … f act_p (Some ? l') (t_code … ih))  f'' (lab_map … ih) (lab_to_keep … ih)
470   | Some lbl ⇒
471      mk_call_post_info ? (nil ?) (CALL ? f act_p (Some ? lbl) (t_code … ih)) (fresh … ih)
472       (〈a_return_post lbl,(a_return_post lbl :: (gen_labels … ih))〉 :: (lab_map … ih))
473       (a_return_post lbl :: lab_to_keep … ih)
474   ]
475| IO lin io lout i1 ⇒
476    let ih ≝ call_post_trans … i1 n abs in
477    mk_call_post_info ? (nil ?) (IO ? lin io lout (t_code … ih)) (fresh … ih)
478     (〈a_non_functional_label lout,(a_non_functional_label lout :: (gen_labels … ih))〉 ::
479      〈a_non_functional_label lin,[a_non_functional_label lin]〉 :: (lab_map … ih)) (lab_to_keep … ih)
480].
481
482
483let rec call_post_clean (p : instr_params) (i : Instructions p) on i :
484associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel →
485option ((list CostLabel) × (Instructions p)) ≝
486λm,keep,abs.
487 match i with
488[ EMPTY ⇒ Some ? 〈abs,EMPTY …〉
489| RETURN x ⇒ Some ? 〈abs,RETURN … x〉
490| SEQ x lab instr ⇒
491   ! 〈l,i1〉 ← call_post_clean … instr m keep abs;
492   match lab with
493   [ None ⇒ return 〈l,SEQ … x (None ?) i1〉
494   | Some lbl ⇒ if ((get_element … m lbl) == lbl :: l)
495                then return 〈nil ?,SEQ … x (Some ? lbl) i1〉
496                else None ?
497   ]
498| COND x ltrue i1 lfalse i2 i3 ⇒
499    ! 〈l3,instr3〉 ← call_post_clean … i3 m keep abs;
500    ! 〈l2,instr2〉 ← call_post_clean … i2 m keep l3;
501    ! 〈l1,instr1〉 ← call_post_clean … i1 m keep l3;
502    if ((get_element … m ltrue) == ltrue :: l1) ∧
503       ((get_element … m lfalse) == lfalse :: l2)
504    then return 〈nil ?,COND … x ltrue instr1 lfalse instr2 instr3〉
505    else None ?
506| LOOP x ltrue i1 lfalse i2 ⇒
507   ! 〈l2,instr2〉 ← call_post_clean … i2 m keep abs;
508   ! 〈l1,instr1〉 ← call_post_clean … i1 m keep (nil ?);
509   if ((get_element … m ltrue) == ltrue :: l1) ∧
510      ((get_element … m lfalse) == lfalse :: l2)
511   then return 〈nil ?,LOOP … x ltrue instr1 lfalse instr2〉
512   else None ?
513| CALL f act_p r_lb i1 ⇒
514  ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs;
515  match r_lb with
516  [ None ⇒ return 〈l1,CALL … f act_p (None ?) instr1〉
517  | Some lbl ⇒ if ((a_return_post lbl ∈ keep))
518               then if ((get_element … m lbl) == lbl :: l1)
519                    then return 〈nil ?,CALL … f act_p (Some ? lbl) instr1〉
520                    else None ?
521               else return 〈(a_return_post lbl) :: l1,CALL … f act_p (None ?) instr1〉
522  ]
523| IO lin io lout i1 ⇒
524   ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs;
525   if ((get_element … m lout) == lout :: l1) ∧ ((get_element … m lin) == [lin])
526   then return 〈nil ?,IO … lin io lout instr1〉
527   else None ?   
528].
529
530let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (a : A) (l1 : list B)
531(l2 : list C) (f : A → B → C → A) on l1 : option A≝
532match l1 with
533[ nil ⇒ match l2 with [ nil ⇒ return a | cons y ys ⇒ None ? ]
534| cons x xs ⇒
535        match l2 with
536        [ nil ⇒ None ?
537        | cons y ys ⇒ ! ih ← (foldr2 … a xs ys f);
538                      return f ih x y
539        ]
540].
541
542definition is_silent_cost_act_b : ActionLabel → bool ≝
543λact. match act with
544 [ cost_act x ⇒ match x with [None ⇒ true | _ ⇒ false ] | _ ⇒ false].
545
546definition eq_ActionLabel : ActionLabel → ActionLabel → bool ≝
547λc1,c2.
548match c1 with
549[ call_act f l ⇒ match c2 with [ call_act f' l' ⇒ f == f' ∧ l == l' | _ ⇒ false]
550| ret_act x ⇒ match c2 with [ret_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true | _ ⇒ false]
551                                                      | Some l ⇒ match y with [ Some l' ⇒ l == l' | _ ⇒ false]
552                                                      ]
553                            | _ ⇒ false
554                            ]
555| cost_act x ⇒ match c2 with [cost_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true | _ ⇒ false]
556                                                        | Some l ⇒ match y with [ Some l' ⇒ l == l' | _ ⇒ false]
557                                                        ]
558                             | _ ⇒ false
559                             ]
560| init_act ⇒ match c2 with [init_act ⇒ true | _ ⇒ false]
561].
562
563definition ret_costed_abs : list CostLabel → option ReturnPostCostLabel → option CostLabel ≝
564λkeep,x.
565 match x with
566              [ Some lbl ⇒ if (a_return_post lbl) ∈ keep then return (a_return_post lbl)
567                           else None ?
568              | None ⇒ None ?
569              ].
570
571
572definition check_continuations : ∀p : instr_params.
573∀l1,l2 : list (ActionLabel × (Instructions p)).
574associative_list DEQCostLabel CostLabel →
575list CostLabel →  option (Prop × (list CostLabel) × (list CostLabel)) ≝
576λp,cont1,cont2,m,keep.
577foldr2 ??? 〈True,nil ?,nil ?〉 cont1 cont2
578 (λx,y,z.
579   let 〈cond,abs_top',abs_tail'〉 ≝ x in
580   match call_post_clean p (\snd z) m keep abs_top' with
581   [ None ⇒ 〈False,nil ?,nil ?〉
582   | Some w ⇒
583      match \fst z with
584       [ ret_act opt_x ⇒
585           match ret_costed_abs keep opt_x with
586           [ Some lbl ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧
587                               get_element … m lbl = lbl :: (\fst w),(nil ?),abs_tail'〉
588           | None ⇒
589              〈\fst y = ret_act (None ?) ∧ cond ∧ \snd w = \snd y,(nil ?),(\fst w) @ abs_tail'〉
590           ]
591       | cost_act opt_x ⇒
592           match opt_x with
593           [ None ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y,\fst w,abs_tail'〉
594           | Some xx ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧
595                               get_element … m xx = xx :: (\fst w),(nil ?),abs_tail'〉]
596       | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]).
597
598(*
599definition check_continuations : ∀p : instr_params.
600∀l1,l2 : list (ActionLabel × (Instructions p)).
601associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel →
602list (list CostLabel) →  option (Prop × (list CostLabel) × (list (list CostLabel))) ≝
603λp,cont1,cont2,m,keep,abs_top,abs_tail.
604foldr2 ??? 〈True,abs_top,abs_tail〉 cont1 cont2
605 (λx,y,z.
606   let 〈cond,abs_top',abs_tail'〉 ≝ x in
607   match call_post_clean p (\snd z) m keep abs_top' with
608   [ None ⇒ 〈False,nil ?,nil ?〉
609   | Some w ⇒
610      match \fst z with
611       [ ret_act opt_x ⇒
612           match ret_costed_abs keep opt_x with
613           [ Some lbl ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧
614                               get_element … m lbl = lbl :: (\fst w),(nil ?),(nil ?) :: abs_tail'〉
615           | None ⇒
616              〈\fst y = ret_act (None ?) ∧ cond ∧ \snd w = \snd y,(nil ?),(\fst w) :: abs_tail'〉
617           ]
618       | cost_act opt_x ⇒
619           match opt_x with
620           [ None ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y,\fst w,abs_tail'〉
621           | Some xx ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧
622                               get_element … m xx = xx :: (\fst w),(nil ?),abs_tail'〉]
623       | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]). *)
624(* in input :
625     abs_top is the list of labels to be propageted to the deepest level of the call stack
626     abs_tail are the lists of labels to be propagated to the levels "below" the deepest level
627   in output :
628     abs_top is the list of labels to be propageted from the current level of the call stack
629     abs_tail are the lists of labels to be propagated from the levels "below" the current level
630  *)       
631       
632
633definition state_rel : ∀p.
634associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel →(list CostLabel) →
635relation (state p) ≝ λp,m,keep,abs_top,abs_tail,st1,st2.
636match check_continuations ? (cont ? st1) (cont … st2) m keep with
637[ Some x ⇒ let 〈prf1,abs_top',abs_tail'〉 ≝ x in
638           prf1 ∧ call_post_clean … (code … st2) m keep abs_top' = return 〈abs_top,(code … st1)〉
639           ∧ store … st1 = store … st2 ∧ io_info … st1 = io_info … st2 ∧ abs_tail = abs_tail'
640| None ⇒ False
641].
642
643include "Simulation.ma".
644
645let rec len (S : abstract_status) (st1 : S) (st2 : S) (t : raw_trace S st1 st2)
646on t : ℕ ≝
647match t with
648[ t_base s ⇒ O
649| t_ind s1 s2 s3 l prf lt ⇒ (len … lt) + 1
650].
651(*
652lemma associative_max : ∀n1,n2,n3.max (max n1 n2) n3 = max n1 (max n2 n3).
653#n1 #n2 #n3 normalize @leb_elim normalize
654[ @leb_elim normalize
655  [ #H1 #H2 @leb_elim normalize
656    [ @leb_elim normalize // * #H @⊥ @H assumption 
657    | @leb_elim normalize
658      [ #H3 * #H @⊥ @H @(transitive_le … H1) assumption
659      | * #H @⊥ @H assumption
660      ]
661    ]
662  | #H1 #H2 @leb_elim normalize
663    [ @leb_elim normalize // #_ #H cases H1 #H1 @⊥ @H1 assumption
664    | @leb_elim normalize
665      [ #_ * #H @⊥ @H assumption
666      | * #H @⊥ @H @(transitive_le … H2)
667*)
668let rec compute_max_n (p : instr_params) (i : Instructions p) on i : ℕ ≝
669match i with
670[ EMPTY ⇒ O
671| RETURN x ⇒ O
672| SEQ x lab instr ⇒ let n ≝ compute_max_n … instr in
673                    match lab with
674                    [ None ⇒ n
675                    | Some l ⇒
676                        match l with
677                        [ a_non_functional_label n' ⇒ S (max n n') ]
678                    ]
679| COND x ltrue i1 lfalse i2 i3 ⇒
680  let n1 ≝ compute_max_n … i1 in
681  let n2 ≝ compute_max_n … i2 in
682  let n3 ≝ compute_max_n … i3 in
683  let mx ≝ max (max n1 n2) n3 in
684  match ltrue with
685  [ a_non_functional_label lt ⇒
686    match lfalse with
687    [a_non_functional_label lf ⇒ S (max (max mx lt) lf) ] ]
688| LOOP x ltrue i1 lfalse i2 ⇒
689   let n1 ≝ compute_max_n … i1 in
690   let n2 ≝ compute_max_n … i2 in
691   let mx ≝ max n1 n2 in
692   match ltrue with
693  [ a_non_functional_label lt ⇒
694    match lfalse with
695    [a_non_functional_label lf ⇒ S (max (max mx lt) lf) ] ]
696| CALL f act_p r_lb i1 ⇒
697   let n ≝ compute_max_n … i1 in
698   match r_lb with
699   [ None ⇒ n
700   | Some lbl ⇒ match lbl with [a_return_cost_label l ⇒ S(max l n) ]
701   ]
702| IO lin io lout i1 ⇒
703  let n ≝ compute_max_n … i1 in
704  match lin with
705  [a_non_functional_label l1 ⇒
706    match lout with
707    [a_non_functional_label l2 ⇒ S(max (max n l1) l2) ] ]
708].
709
710
711definition same_fresh_map_on : list CostLabel →
712relation (associative_list DEQCostLabel CostLabel) ≝
713λdom,m1,m2.∀x.bool_to_Prop (x ∈ dom) → get_element … m1 x = get_element … m2 x.
714
715definition same_to_keep_on : list CostLabel → relation (list CostLabel) ≝
716λdom,keep1,keep2.∀x. bool_to_Prop (x ∈ dom) → (x ∈ keep1) = (x ∈ keep2).
717
718lemma memb_not_append : ∀D : DeqSet.∀l1,l2 : list D.∀x : D.
719x ∈ l1 = false → x ∈ l2 = false → x ∈ (l1 @ l2) = false.
720#D #l1 elim l1
721[ #l2 #x #_ #H @H ]
722#x #xs #IH #l2 #x1 whd in match (memb ???); inversion (x1 == x) normalize nodelta
723[ #_ #EQ destruct] #EQx1 #EQxs #EQl2 whd in match (memb ???); >EQx1
724normalize nodelta @IH //
725qed.
726
727lemma lab_to_keep_in_domain : ∀p.∀i : Instructions p.
728∀x,n,l.
729x ∈ lab_to_keep … (call_post_trans … i n l) → x ∈ get_labels_of_code …  i.
730#p #i elim i //
731[ #seq #opt_l #instr #IH #x #n #l whd in match (call_post_trans ????);
732  cases opt_l -opt_l normalize nodelta [|#lbl]
733  whd in match (get_labels_of_code ??); #H [2: @orb_Prop_r] /2/
734| #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #x #n #l
735  whd in match (call_post_trans ????); whd in match (get_labels_of_code ??);
736  #H cases(memb_append … H) -H #H @orb_Prop_r @orb_Prop_r
737  [ >memb_append_l1 // @IH1 [3: >H // |*: ]
738  | >memb_append_l2 // cases(memb_append … H) -H #H
739     [>memb_append_l1 // @IH2 [3: >H // |*: ]
740     | >memb_append_l2 // @IH3 [3: >H // |*: ]
741     ]
742  ]
743| #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #x #n #l
744  whd in match (call_post_trans ????); whd in match (get_labels_of_code ??);
745  #H cases(memb_append … H) -H #H @orb_Prop_r @orb_Prop_r
746  [ >memb_append_l1 | >memb_append_l2 ] // [ @IH1 | @IH2 ] [3,6: >H |*: ] //
747| #f #act_p * [|#lbl] #i1 #IH #x #n #l whd in match (call_post_trans ????);
748  whd in match (get_labels_of_code ??); /2/ whd in match (memb ???);
749  inversion(x == lbl) #Hlbl normalize nodelta
750  [*  >(\P Hlbl) @orb_Prop_l @eq_costlabel_elim // * #H @H %
751  | #H @orb_Prop_r @IH //
752  ]
753| #lin #io #lout #i1 #IH #x #n #l whd in match (call_post_trans ????);
754  whd in match (get_labels_of_code ??); #H @orb_Prop_r @orb_Prop_r @IH //
755]
756qed.
757 
758lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A .
759no_duplicates … (l1 @ l2) → x ∈  l1 → x ∈ l2 → False.
760#A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???);
761inversion (x == x1) normalize nodelta
762[ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H %
763| #_ @IH //
764]
765qed.
766 
767lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.
768let dom ≝ get_labels_of_code … i1 in
769no_duplicates … dom →
770∀m,keep.
771∀info,l.call_post_trans p i1 n l = info →
772same_fresh_map_on dom (lab_map … info) m →
773same_to_keep_on dom (lab_to_keep … info) keep →
774call_post_clean … (t_code … info) m keep l
775 = return 〈gen_labels … info,i1〉.
776#p #i1 elim i1
777[ #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?);
778  #EQ destruct(EQ) //
779| #x #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?);
780  #EQ destruct(EQ) //
781| #seq * [|#lbl] #instr #IH #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep
782  #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #H1 #H2 whd in ⊢ (??%%); normalize nodelta
783  >IH //
784  [1,4: whd whd in H2; #x #Hx @H2 whd in match (get_labels_of_code ??); //
785        @orb_Prop_r //
786  |2,5: whd whd in H1; #x #Hx [ @H1 // ] cases no_dup #H3 #_ <H1
787       [2: whd in match (get_labels_of_code ??); @orb_Prop_r // ]
788       whd in ⊢ (???%); cases(eqb_true … x lbl) inversion(x == lbl) normalize nodelta
789       [2: //] #_ #H4 >H4 in Hx; // #H5 >H5 in H3; * #ABS @⊥ @ABS %
790  |6: cases no_dup //
791  ]
792  normalize nodelta <(H1 lbl)
793  [2: whd in match (get_labels_of_code ??); @orb_Prop_l cases(eqb_true … (a_non_functional_label lbl) lbl)
794      #H3 #H4 >H4 % ]
795  whd in match (get_element ????); >(\b (refl …)) normalize nodelta
796  >(\b (refl …)) %
797| #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #n normalize nodelta
798  #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?);
799  #EQ destruct(EQ) #H1 #H2 whd in ⊢ (??%?); >IH3 //
800  [2: #x #Hx whd in H2; inversion(x ∈ lab_to_keep … (call_post_trans …))
801    [ #EQkeep <H2 [ >memb_append_l2 // >memb_append_l2 // ]
802      whd in match (get_labels_of_code ??); @orb_Prop_r @orb_Prop_r >memb_append_l2 //
803      >memb_append_l2 // >Hx %
804    | #EQno_keep <H2
805      [2: whd in match (get_labels_of_code ??); @orb_Prop_r @orb_Prop_r
806          >memb_append_l2 // >memb_append_l2 // >Hx % ] @sym_eq @memb_not_append
807         [| @memb_not_append //] inversion(x ∈ lab_to_keep ??) // #Hlab @⊥
808         lapply(lab_to_keep_in_domain ????? (eq_true_to_b … Hlab)) #ABS     
809         cases no_dup #_ * #_ #ABS1
810         [ @(memb_no_duplicates_append … x … ABS1) // >memb_append_l2 //
811         | <associative_append in ABS1; #ABS1       
812           @(memb_no_duplicates_append … x … ABS1) // >memb_append_l2 // >ABS %
813         ]
814         >Hx %
815    ]
816  |3: whd in H1; #x #Hx <H1 (*no duplicates *) cases daemon
817  |4: cases no_dup #_ * #_ #H @no_duplicates_append_r [2: @(no_duplicates_append_r … H) |]
818  ]
819 
820  normalize nodelta >IH2 //
821  [2: #x #Hx whd in H2; (*come sopra*) cases daemon
822  |3: (*no duplicates ok *) cases daemon
823  |4: (* come sopra *) cases daemon
824  ]
825  >m_return_bind >IH1 //
826  [2,3,4: cases daemon (*come sopra*) ]
827  >m_return_bind normalize nodelta whd in H1; <H1
828  [2: whd in match (get_labels_of_code ??); whd in match (memb ???);
829      >(\b (refl …)) % ] whd in match (get_element ????); >(\b (refl …))
830      normalize nodelta >(\b (refl …)) <H1
831      [2: whd in match (get_labels_of_code ??); >memb_cons //
832      whd in match (memb ???); >(\b (refl …)) % ]
833      whd in match (get_element ????); @eq_costlabel_elim normalize nodelta
834      [ #ABS cases daemon (*no duplicates *) ] #_ whd in match (get_element ????);
835      >(\b (refl …)) normalize nodelta >(\b (refl …)) %
836|*: cases daemon (*TODO*)
837]
838qed.
839
840
841definition trans_prog : ∀p,p'.Program p p' →
842(Program p p') × (associative_list DEQCostLabel CostLabel) × (list CostLabel)≝
843λp,p',prog.
844let max_all ≝ foldl … (λn,i.max n (compute_max_n … (f_body … i))) O (env … prog) in
845let 〈t_env,n,m,keep〉 ≝ (foldr ??
846           (λi,x.let 〈t_env,n,m,keep〉 ≝ x in
847           let info ≝ call_post_trans … (f_body … i) n (nil ?) in
848                   〈(mk_env_item ??
849                       (mk_signature ??(f_name ?? i) (f_pars … i) (f_ret … i))
850                       (f_lab … i) (t_code … info)) :: t_env,
851                     fresh … info, 〈a_call (f_lab … i),(a_call (f_lab … i)) :: (gen_labels ? info)〉 ::
852                                     ((lab_map … info) @ m),(lab_to_keep … info) @ keep〉)
853          (〈nil ?,max_all,nil ?,nil ?〉) (env … prog)) in
854〈mk_Program ?? t_env (t_code … (call_post_trans … (main … prog) n (nil ?))),m,keep〉 .
855
856definition map_labels_on_trace :
857(associative_list DEQCostLabel CostLabel) → list CostLabel → list CostLabel ≝
858λm,l.foldr … (λlab,t.(get_element … m lab) @ t) (nil ?) l.
859
860lemma map_labels_on_trace_append:
861 ∀m,l1,l2. map_labels_on_trace m (l1@l2) =
862  map_labels_on_trace m l1 @ map_labels_on_trace m l2.
863 #m #l1 elim l1 // #hd #tl #IH #l2 >associative_append <IH //
864qed.
865
866include "../src/common/Errors.ma".
867
868axiom is_permutation: ∀A.list A → list A → Prop.
869axiom is_permutation_eq : ∀A.∀l : list A.is_permutation … l l.
870axiom is_permutation_cons : ∀A.∀l1,l2,x.is_permutation A l1 l2 →
871                                       is_permutation A (x :: l1) (x :: l2).
872
873(*
874inductive is_permutation (A : Type[0]) : list A → list A → Prop ≝
875| p_empty : is_permutation A (nil ?) (nil ?)
876| p_append : ∀x,x1,x2,y,y1,y2.
877               x = y → is_permutation A (x1 @ x2) (y1 @ y2) →
878                 is_permutation A (x1 @ [x] @ x2) (y1 @ [y] @ y2).
879
880lemma is_permutation_eq : ∀A.∀l : list A.is_permutation … l l.
881#A #l elim l // #x #xs #IH
882change with ((nil ?) @ (x :: xs)) in ⊢ (??%%);
883>append_cons >associative_append
884@(p_append ? x (nil ?) xs x (nil ?) xs (refl …)) @IH
885qed.
886
887lemma is_permutation_append : ∀A.∀l1,l2,l3,l4 : list A.
888is_permutation A l1 l3 → is_permutation A l2 l4 →
889is_permutation A (l1 @ l2) (l3 @ l4).
890#A #l1 inversion (|l1|)  [2: #n lapply l1 elim n
891[ #l2 #l3 #l4 #H inversion H // #x #x1 #x2 #y #y1 #y2 #EQ #H1 #_
892 #ABS cases(nil_to_nil … (sym_eq ??? ABS)) -ABS #_ #ABS
893 cases(nil_to_nil … ABS) #EQ1 destruct(EQ1) ]
894#x #xs #IH #l2 #l3 #l4 #H inversion H
895[#EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ) ]
896#y #y1 #y2 #z #z1 #z2 #EQ destruct(EQ) #H1 #_ #EQx_xs #EQ destruct(EQ) #_
897*)
898
899lemma trans_env_ok : ∀p : state_params.∀ prog.
900no_duplicates_labels … prog →
901let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
902∀f,env_it.lookup p p (env … prog) f = return env_it →
903let dom ≝ get_labels_of_code … (f_body … env_it) in
904∃env_it',n.lookup p p (env … t_prog) f = return env_it' ∧
905let info ≝ call_post_trans … (f_body … env_it) n (nil ?) in
906t_code … info = f_body … env_it' ∧
907get_element … m (a_call (f_lab … env_it')) = (a_call (f_lab … env_it')) :: gen_labels … info ∧
908f_sig … env_it = f_sig … env_it' ∧ f_lab … env_it = f_lab … env_it' ∧
909same_fresh_map_on dom m (lab_map … info) ∧ same_to_keep_on dom keep (lab_to_keep … info).
910#p * #env #main @pair_elim * #t_prog #m #keep whd in match trans_prog;
911normalize nodelta @pair_elim generalize in match O; xxxx (*probably needs invariant *) elim env
912[ * #env' #fresh #x #_ #_ #_ #f #env_it normalize in ⊢ (% → ?);  #ABS destruct]
913* #hd_sig #hd_lab #hd_code #tail #IH * #env' #fresh * #m' #keep'
914normalize in ⊢ (% → ?); normalize nodelta @pair_elim * #env_tail #fresh_tail
915* #m_tail #keep_tail #EQtail normalize nodelta #EQ1 #EQ2 destruct(EQ1 EQ2)
916whd in ⊢ (% → ?); whd in match (foldr ?????); * #Hhd_lab #H lapply(no_duplicates_append_r … H)
917change with (no_duplicates_labels p p (mk_Program p p tail main)) in match
918(no_duplicates_labels p p (mk_Program p p tail main)); #no_dup_tail
919lapply(no_duplicates_append_l … H) #no_dup_head normalize nodelta
920#f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta
921[ #EQ destruct(EQ) whd in ⊢ (???% → ?); #EQ destruct(EQ)
922  inversion (call_post_trans … hd_code fresh_tail [])
923  #gen_labs #t_hd_code #t_fresh #t_lab_map #t_lab_to_keep #EQ_trans_code
924  %{(mk_env_item … hd_sig hd_lab t_hd_code)} %{fresh_tail} %
925  [ whd in ⊢ (??%?); @eq_function_name_elim [2: * #H @⊥ @H %] #_ normalize nodelta
926    @eq_f cases hd_sig // ] >EQ_trans_code % [% [ % [ % [% // whd in ⊢ (??%?); >(\b (refl …)) %] % ] % | whd
927    #x #Hx whd in ⊢ (??%?); >(? : (x == hd_lab) = false) [2: cases daemon (*per Hhd_lab*)]
928    normalize nodelta cases daemon (* needs lemma on maps *)]
929  | whd cases daemon (*using lab_to_keep_in_domain and H *)
930  ]
931| #Hf #Henv_it cases(IH … no_dup_tail … Henv_it)
932  [4: >EQtail in ⊢ (??%?);
933   
934   
935    [ >EQ_trans_code % | >EQ_trans_code
936    [ >EQ_trans_code % | >EQ_trans_code whd in ⊢ (??%?);
937      cases(eqb_true … (a_call hd_lab) hd_lab) #_ #H1 >(H1 (refl …)) // ]]
938
939  #EQt_prog
940
941
942
943lemma correctness : ∀p,p',prog.
944let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
945∀s1,s2,s1' : state p.∀abs_top,abs_tail.
946∀t : raw_trace (operational_semantics … p' prog) s1 s2.
947state_rel … m keep abs_top abs_tail s1 s1' →
948∃abs_top',abs_tail'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'.
949state_rel  … m keep abs_top' abs_tail' s2 s2' ∧
950is_permutation ? ((abs_top @ (map_labels_on_trace m (get_costlabels_of_trace … t))) @ abs_tail) 
951                 (((get_costlabels_of_trace … t') @ abs_top' ) @ abs_tail') ∧
952 len … t = len … t'.
953#p #p' #prog @pair_elim * #t_prog #m #keep #EQtrans
954#s1 #s2 #s1' #abs_top #abs_tail #t lapply abs_top -abs_top lapply abs_tail
955-abs_tail lapply s1' -s1' elim t
956[ #st #s1' #abs_tail #abs_top #H %{abs_top} %{abs_tail} %{s1'} %{(t_base …)}
957  % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil
958  @is_permutation_eq
959]
960#st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
961[ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore
962  #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #EQ4 destruct #tl #IH #s1' #abs_tail #abs_top
963  whd in match state_rel in ⊢ (% → ?); normalize nodelta >EQcont11 in ⊢ (% → ?);
964  whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????);
965  inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1'
966  normalize nodelta change with (check_continuations ?????) in match (foldr2 ???????);
967  inversion(check_continuations ?????) [ #_ *] ** #H1 #l2 #ll2 #EQHl2
968  >m_return_bind normalize nodelta inversion (call_post_clean ?????) [ #_ ***** ]
969  * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta
970  cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta
971  [1,4: [ #x #y ] #_ (*#_ #_ #_ #H*) *****
972  | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] ******[|*] #EQ @⊥ >EQ in Hl1;
973    normalize * /2/ ] *
974  [ #EQconts1' normalize nodelta ****** #EQ destruct(EQ)
975    #HH1 #EQ destruct(EQ) >EQcode11 in ⊢ (% → ?); inversion(code … s1')
976    [
977    | #x
978    | #seq #lbl #i #_
979    | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
980    | #cond #ltrue #i1 #lfalse #i2 #_ #_
981    | #f #act_p #ret_post #i #_
982    | #l_in #io #l_out #i #_
983    ]
984    [|*: #_ whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)]
985         cases(call_post_clean ?????) normalize nodelta
986         [1,3,5,7,9: #EQ destruct(EQ)] cases daemon (* da fare assurdi!!!*) ]
987    #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11 #EQ destruct(EQ)
988    cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 abs_top …)
989    [2: whd whd in match check_continuations; normalize nodelta
990       change with (check_continuations ?????) in match (foldr2 ???????); >EQHl2
991        normalize nodelta % // % // % // % // @EQcode_c_st12 ]
992    #abs_top' * #abs_tail' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen
993    %{abs_top'} %{abs_tail'} %{st3'} %{(t_ind … (cost_act (None ?)) …  t')}
994    [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉)
995      [3: assumption |4: assumption |*:] /3 by nmk/ ]
996    % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts
997  | #lbl #EQconts1' normalize nodelta ******* #EQ destruct(EQ)
998    #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 in ⊢ (% → ?);
999    inversion(code … s1')
1000    [
1001    | #x
1002    | #seq #lbl #i #_
1003    | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
1004    | #cond #ltrue #i1 #lfalse #i2 #_ #_
1005    | #f #act_p #ret_post #i #_
1006    | #l_in #io #l_out #i #_
1007    ]
1008    [|*: #_ whd in ⊢ (??%% → ?); #EQ cases daemon (* da fare assurdi !!!*) ]
1009    #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio #EQ destruct(EQ)
1010    cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 l3 …)
1011    [2: whd whd in match check_continuations; normalize nodelta
1012       change with (check_continuations ?????) in match (foldr2 ???????);
1013       >EQHl2 in ⊢ (match % with [ _⇒ ? | _ ⇒ ?]);
1014        normalize nodelta % // % // % // % // @EQcode_c_st12 ]
1015    #abs_top' * #abs_tail' * #st3' * #t' ** #Hst3st3' #EQcost #EQlen
1016    %{abs_top'} %{abs_tail'} %{st3'}
1017    %{(t_ind … (cost_act (Some ? lbl)) … t')}
1018    [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉)
1019      [3: assumption |4: assumption |*:] /3 by nmk/ ]
1020    % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append
1021    whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el
1022    @is_permutation_cons assumption
1023  ]
1024(*     
1025| #seq #i #store * [| #lbl] #EQcode11 #EQstore #EQ destruct(EQ) #EQcont
1026  #EQ destruct(EQ) #Hio_st11 #Hio_st12 #EQ destruct(EQ) #EQ1 #EQ2 destruct(EQ1 EQ2)
1027  #EQ destruct(EQ) #tl #IH #st3 #l1 whd in ⊢ (% → ?);
1028  inversion(check_continuations ?????) [1,3: #_ *] * #H1 #l2
1029  [ >EQcont in ⊢ (% → ?); | >EQcont in ⊢ (% → ?); ] #EQcheck normalize nodelta
1030  *** #HH1 [ >EQcode11 in ⊢ (% → ?); | >EQcode11 in ⊢ (% → ?); ]
1031  inversion(code … st3)
1032  [1,2,4,5,6,7,8,9,11,12,13,14: (*assurdi da fare *) cases daemon ]
1033  #seq1 #opt_l #i1 #_ #EQcode_st3 change with (m_bind ?????) in ⊢ (??%? → ?);
1034  cases daemon *)
1035|8: #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
1036    #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3
1037    destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #IH #st1' #abs_top #abs_tail
1038    whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1
1039    #abs_top_cont #abs_tail_cont #EQcheck
1040    normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1')
1041    [1,2,3,4,5,7: (*assurdi da fare*) cases daemon] #f' #act_p' #opt_l' #i' #_
1042    #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ)
1043    cut(∃env_it',n.lookup p p (env … t_prog) f = return env_it' ∧
1044          t_code … (call_post_trans … (f_body … env_it) n (nil ?)) = f_body … env_it' ∧
1045          get_element … m (a_call (f_lab … env_it')) = (a_call (f_lab … env_it')) :: gen_labels … (call_post_trans … (f_body … env_it) n (nil ?)) ∧
1046          f_sig … env_it = f_sig … env_it' ∧ f_lab … env_it = f_lab … env_it')
1047    [ cases daemon (*TODO*) ] * #env_it' * #fresh' **** #EQenv_it' #EQtrans #EQgen_labels #EQsignature #EQlab_env_it
1048    change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean;
1049    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind
1050    inversion opt_l' in EQcode_st1'; [| #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta
1051    [2: inversion(memb ???) normalize nodelta #Hlbl_keep
1052        [  inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
1053           #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta
1054          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_
1055          lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta
1056          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'')
1057          #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
1058          #EQ destruct(EQ)
1059          cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) (abs_tail_cont) (gen_labels … (call_post_trans … (f_body … env_it) fresh' (nil ?))))
1060          [2: whd >EQcont12
1061            change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????);
1062            >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta >EQopt_l'
1063            whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta
1064            % // % // % // % [/5 by conj/] >EQgen_labels >EQcode12 <EQtrans
1065            @(inverse_call_post_trans … fresh') [2: % |*: cases daemon (*TODO*) ]
1066          ]
1067          #abs_top''' * #abs_tail''' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen %{abs_top'''}
1068          %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
1069          [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [2: whd in ⊢ (??%%); >EQlen %]
1070          %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
1071          >EQlab_env_it >associative_append whd in match (append ???); >associative_append
1072          >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%);
1073          whd in match (map_labels_on_trace ??); >EQgen_labels @is_permutation_cons
1074          >append_nil whd in match (append ???) in ⊢ (???%); //
1075        | 
1076          xxxxxxxxxx
1077           
1078           
1079           
1080                   
1081            inversion(memb ???) normalize nodelta #Hlbl_keep
1082            [ inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
1083          #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta
1084          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_
1085          lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta
1086          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'')
1087          #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
1088          #EQ destruct(EQ) whd in match ret_costed_abs; normalize nodelta >Hlbl_keep
1089          normalize nodelta >EQi' normalize nodelta % // % // % [ % // % // % //]
1090   
1091   
1092   
1093   
1094    cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) (abs_top'' @ abs_tail_cont) (get_element … m (a_call (f_lab … env_it'))))
1095    [2: whd >EQcont12
1096     change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????);
1097     >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta
1098     cases opt_l' in EQcode_st1' EQclean; [| #lbl'] #EQcode_st1' normalize nodelta
1099    [2: inversion(memb ???) normalize nodelta #Hlbl_keep
1100        [ inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
1101          #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta
1102          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_
1103          lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta
1104          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'')
1105          #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
1106          #EQ destruct(EQ) whd in match ret_costed_abs; normalize nodelta >Hlbl_keep
1107          normalize nodelta >EQi' normalize nodelta % // % // % [ % // % // % //] >EQcode12 <EQtrans
1108          cases daemon (*TODO*)
1109        | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1110          whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta
1111          % // % // % [ % // % //]  >EQcode12 <EQtrans
1112           * [ #_ #l3'
1113    cases(bind_inversion ????? H) in ⊢ ?;
1114
1115   
1116    >EQcost normalize
1117   
1118    %{l1}
1119  xxxxxxxx
1120   whd in match is_silent_cost_act_b; normalize nodelta
1121    cases lab1 in H Hio11; normalize nodelta
1122    [1,2,4: [1,2: #x [ #y]] #H #Hio11 #EQ destruct]
1123    * normalize nodelta [2: #x #H #Hio11 #EQ destruct] #H #Hio11 #_
1124    inversion(call_post_clean ?????)
1125    [ #_ *** ] * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta *****
1126    #EQ destruct(EQ) #HH1 #EQ destruct(EQ) >EQcode11
1127    whd in match (call_post_clean ?????) in ⊢ (% → ?); whd in ⊢ (??%% → ?);
1128    inversion(code … s1')
1129    [| #x #EQ1 normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
1130       destruct(EQ) |*: cases daemon (*ASSURDI!!*)] #EQcode_s1'
1131    normalize in ⊢ (% → ?); #EQ destruct(EQ) #EQstore #EQio
1132    cases(IH (mk_state ? new_code' new_cont' (store … s1') false)  l1 ?)
1133    [2: whd whd in match check_continuations; normalize nodelta >EQHl2
1134        normalize nodelta % // % // >EQcode_c_st12 % // ] #l3 * #st3' * #t' **
1135    #Hst3st12' #EQcost #EQlen %{l3} %{st3'} %{(t_ind … (cost_act (None ?)) … t')}
1136    [ whd @(empty ????? 〈(cost_act (None ?)),?〉)
1137      [3: @hide_prf assumption |4: @hide_prf @EQconts1' |*: ] @hide_prf //
1138      [ <EQio #H2 @⊥ lapply(Hio11 H2) * #F #eq destruct | % *]  ] %
1139    [ %{Hst3st12'} whd in match (get_costlabels_of_trace ????); 
1140      whd in match (get_costlabels_of_trace ????) in ⊢ (???%); //
1141    | whd in match (len ????); whd in match (len ????) in ⊢ (???%);
1142      >EQlen %
1143    ]
1144  | #non_sil_lab1 normalize nodelta inversion(call_post_clean ?????) [ #_ ****]
1145    * #l3 #code' #EQcall' normalize nodelta inversion(ret_costed_abs ??)
1146    [2: #x #H2 @⊥ cases lab1 in Hl1 H2; normalize
1147        [ #f #c #_
1148        | #x * #ABS @⊥ @ABS %
1149        | #x #_
1150        | #_
1151        ]
1152        #EQ destruct(EQ) ]
1153    #Hlab1 normalize nodelta ***** #EQ destruct(EQ) #HH1 #EQ destruct(EQ)
1154    >EQcode11  inversion(code … s1')
1155    [| #x #EQ1 normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
1156       destruct(EQ) |*: cases daemon (*ASSURDI!!*)] #EQcode_s1'
1157    normalize in ⊢ (% → ?); #EQ destruct(EQ) #EQstore #EQio
1158    cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l1 ?)
1159    [2: whd whd in match check_continuations; normalize nodelta >EQHl2
1160        normalize nodelta % // % // % // >EQcall' % ] #l4 * #st3' * #t' **
1161        #Hst3st3' #EQcost #EQlen %{l4} %{st3'} %{(t_ind … lab1 … t')}
1162        [ whd @(empty ????? 〈lab1,?〉)
1163        [3: @hide_prf assumption |4: assumption |*:] @hide_prf // #H3 @Hio11 >EQio @H3]
1164        % [2: whd in match (len ????); whd in match (len ????) in ⊢ (???%);
1165              >EQlen % ]
1166        %{Hst3st3'} >associative_append <EQcost <associative_append
1167        >map_labels_on_trace_append <associative_append @eq_f2 //
1168        cases new_code' in EQcall';
1169        [| #y | #seq #opt_l #i1 | #cond #ltrue #i_true #lfalse #i_false #i1
1170         | #cond #ltrue #i_true #lfalse #ifalse | #f #act_p #ret_opt #i | #l_in #io #l_out #i ]
1171        whd in match (call_post_clean ?????);
1172        [1,2: #EQ destruct(EQ) //
1173       
1174       
1175         whd in match (get_costlabels_of_trace ??? ?) in ⊢ (??%%);
1176       
1177         @eq_f2  whd in ⊢ (??%?);
1178         
1179 
1180 
1181cases daemon (*TODO*)
1182qed.
Note: See TracBrowser for help on using the repository browser.