source: LTS/Language.ma @ 3396

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

correctness proof in developping

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