source: LTS/Vm.ma @ 3457

Last change on this file since 3457 was 3457, checked in by piccolo, 6 years ago
File size: 25.4 KB
Line 
1include "costs.ma".
2include "basics/lists/list.ma".
3include "../src/utilities/option.ma".
4include "basics/jmeq.ma".
5
6lemma bind_inversion : ∀A,B : Type[0].∀m : option A.
7∀f : A → option B.∀y : B.
8! x ← m; f x = return y →
9∃ x.(m = return x) ∧ (f x = return y).
10#A #B * [| #a] #f #y normalize #EQ [destruct]
11%{a} %{(refl …)} //
12qed.
13
14record assembler_params : Type[1] ≝
15{ seq_instr : Type[0]
16; jump_condition : Type[0]
17; io_instr : Type[0]
18; entry_of_function : FunctionName → ℕ
19; call_label_fun : list (ℕ × CallCostLabel)
20; return_label_fun : list (ℕ × ReturnPostCostLabel)
21}.
22
23inductive AssemblerInstr (p : assembler_params) : Type[0] ≝
24| Seq : seq_instr p → option (NonFunctionalLabel) →  AssemblerInstr p
25| Ijmp: ℕ → AssemblerInstr p
26| CJump : jump_condition p → ℕ → NonFunctionalLabel → NonFunctionalLabel → AssemblerInstr p
27| Iio : NonFunctionalLabel → io_instr p → NonFunctionalLabel → AssemblerInstr p
28| Icall: FunctionName → AssemblerInstr p
29| Iret: AssemblerInstr p.
30
31definition AssemblerProgram ≝λp.list (AssemblerInstr p) × ℕ.
32
33definition fetch: ∀p.AssemblerProgram p → ℕ → option (AssemblerInstr p) ≝
34 λp,l,n. nth_opt ? n (\fst l).
35
36definition stackT: Type[0] ≝ list (nat).
37
38record sem_params (p : assembler_params) : Type[1] ≝
39{ m : monoid
40; asm_store_type : Type[0]
41; eval_asm_seq : seq_instr p → asm_store_type → option asm_store_type
42; eval_asm_cond : jump_condition p → asm_store_type → option bool
43; eval_asm_io : io_instr p → asm_store_type → option asm_store_type
44; cost_of_io : io_instr p → asm_store_type → m
45; cost_of : AssemblerInstr p → m
46}.
47
48record vm_state (p : assembler_params) (p' : sem_params p) : Type[0] ≝
49{ pc : ℕ
50; asm_stack : stackT
51; asm_store : asm_store_type … p'
52; asm_is_io : bool
53; cost : m … p'
54}.
55
56definition label_of_pc ≝ λL.λl.λpc.find …
57   (λp.let 〈x,y〉 ≝ p in if eqb x pc then Some L y else None ? ) l.
58   
59definition option_pop ≝
60  λA.λl:list A. match l with
61  [ nil ⇒ None ?
62  | cons a tl ⇒ Some ? (〈a,tl〉) ].
63
64
65inductive vmstep (p : assembler_params) (p' : sem_params p)
66   (prog : AssemblerProgram p)  :
67      ActionLabel → relation (vm_state p p') ≝
68| vm_seq : ∀st1,st2 : vm_state p p'.∀i,l.
69           fetch … prog (pc … st1) = return (Seq p i l) →
70           asm_is_io … st1 = false →
71           eval_asm_seq p p' i (asm_store … st1) = return asm_store … st2 → 
72           asm_stack … st1 = asm_stack … st2 →
73           asm_is_io … st1 = asm_is_io … st2 →
74           S (pc … st1) = pc … st2 →
75           op … (cost … st1) (cost_of p p' (Seq p i l)) = cost … st2 →
76           vmstep … (cost_act l) st1 st2
77| vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ.
78           fetch … prog (pc … st1) = return (Ijmp p new_pc) →
79           asm_is_io … st1 = false →
80           asm_store … st1 = asm_store … st2 →
81           asm_stack … st1 = asm_stack … st2 →
82           asm_is_io … st1 = asm_is_io … st2 →
83           new_pc = pc … st2 →
84           op … (cost … st1) (cost_of p p' (Ijmp … new_pc)) = cost … st2 →
85           vmstep … (cost_act (None ?)) st1 st2
86| vm_cjump_true :
87           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
88           eval_asm_cond p p' cond (asm_store … st1) = return true→
89           fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) →
90           asm_is_io … st1 = false →
91           asm_store … st1 = asm_store … st2 →
92           asm_stack … st1 = asm_stack … st2 →
93           asm_is_io … st1 = asm_is_io … st2 →
94           pc … st2 = new_pc →
95           op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse)) = cost … st2 →
96           vmstep … (cost_act (Some ? ltrue)) st1 st2
97| vm_cjump_false :
98           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
99           eval_asm_cond p p' cond (asm_store … st1) = return false→
100           fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) →
101           asm_is_io … st1 = false →
102           asm_store … st1 = asm_store … st2 →
103           asm_stack … st1 = asm_stack … st2 →
104           asm_is_io … st1 = asm_is_io … st2 →
105           S (pc … st1) = pc … st2 →
106           op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse)) = cost … st2 →
107           vmstep … (cost_act (Some ? lfalse)) st1 st2
108| vm_io_in : 
109           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
110           fetch … prog (pc … st1) = return (Iio p lin io lout) →
111           asm_is_io … st1 = false →
112           asm_store … st1 = asm_store … st2 →
113           asm_stack … st1 = asm_stack … st2 →
114           true = asm_is_io … st2 →
115           pc … st1 = pc … st2 →
116           cost … st1 = cost … st2 →
117           vmstep … (cost_act (Some ? lin)) st1 st2
118| vm_io_out :
119           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
120           fetch … prog (pc … st1) = return (Iio p lin io lout) →
121           asm_is_io … st1 = true →
122           eval_asm_io … io (asm_store … st1) = return asm_store … st2 →
123           asm_stack … st1 = asm_stack … st2 →
124           false = asm_is_io … st2 →
125           S (pc … st1) = pc … st2 →
126           op … (cost … st1) (cost_of_io p p' io (asm_store … st1)) = cost … st2 →
127           vmstep … (cost_act (Some ? lout)) st1 st2
128| vm_call :
129           ∀st1,st2 : vm_state p p'.∀f,lbl.
130           fetch … prog (pc … st1) = return (Icall p f) →
131           asm_is_io … st1 = false →
132           asm_store … st1 = asm_store … st2 →
133           S (pc … st1) ::  asm_stack … st1 = asm_stack … st2 →
134           asm_is_io … st1 = asm_is_io … st2 →
135           entry_of_function p  f = pc … st2 →
136           op … (cost … st1) (cost_of p p' (Icall p f)) = cost … st2 →
137           label_of_pc ? (call_label_fun p) (entry_of_function p f) = return lbl →
138           vmstep … (call_act f lbl) st1 st2
139| vm_ret :
140          ∀st1,st2 : vm_state p p'.∀newpc,lbl.
141           fetch … prog (pc … st1) = return (Iret p) →
142           asm_is_io … st1 = false →
143           asm_store … st1 = asm_store … st2 →
144           asm_stack … st1 = newpc ::  asm_stack … st2  →
145           asm_is_io … st1 = asm_is_io … st2 →
146           newpc = pc … st2 →
147           label_of_pc ? (return_label_fun p) newpc = return lbl →
148           op … (cost … st1) (cost_of p p' (Iret p)) = cost … st2 →
149           vmstep … (ret_act (Some ? lbl)) st1 st2.
150
151definition eval_vmstate : ∀p : assembler_params.∀p' : sem_params p.
152AssemblerProgram p → vm_state p p' → option (ActionLabel × (vm_state p p')) ≝
153λp,p',prog,st.
154! i ← fetch … prog (pc … st);
155match i with
156[ Seq x opt_l ⇒
157   if asm_is_io … st then
158     None ?
159   else
160     ! new_store ← eval_asm_seq p p' x (asm_store … st);
161     return 〈cost_act opt_l,
162             mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false
163                (op … (cost … st) (cost_of p p' (Seq p x opt_l)))〉
164| Ijmp newpc ⇒
165   if asm_is_io … st then
166     None ?
167   else
168     return 〈cost_act (None ?),
169             mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
170                (op … (cost … st) (cost_of p p' (Ijmp … newpc)))〉
171| CJump cond newpc ltrue lfalse ⇒
172   if asm_is_io … st then
173     None ?
174   else
175     ! b ← eval_asm_cond p p' cond (asm_store … st);
176     if b then
177       return 〈cost_act (Some ? ltrue),
178               mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
179                (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse)))〉
180     else
181       return 〈cost_act (Some ? lfalse),
182               mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false
183                (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse)))〉
184| Iio lin io lout ⇒
185              if asm_is_io … st then
186                 ! new_store ← eval_asm_io … io (asm_store … st);
187                 return 〈cost_act (Some ? lout),
188                         mk_vm_state ?? (S (pc … st)) (asm_stack … st)
189                         new_store false
190                         (op … (cost … st)
191                               (cost_of_io p p' io (asm_store … st)))〉   
192              else
193                return 〈cost_act (Some ? lin),
194                        mk_vm_state ?? (pc … st) (asm_stack … st) (asm_store … st)
195                                    true (cost … st)〉
196| Icall f ⇒
197    if asm_is_io … st then
198      None ?
199    else
200      ! lbl ← label_of_pc ? (call_label_fun p) (entry_of_function p f);
201      return 〈call_act f lbl,
202              mk_vm_state ?? (entry_of_function p f)
203                             ((S (pc … st)) :: (asm_stack … st))
204                             (asm_store … st) false
205                             (op … (cost … st) (cost_of p p' (Icall p f)))〉
206| Iret ⇒ if asm_is_io … st then
207            None ?
208         else
209            ! 〈newpc,tl〉 ← option_pop … (asm_stack … st);
210            ! lbl ← label_of_pc ? (return_label_fun p) newpc;
211            return 〈ret_act (Some ? lbl),
212                    mk_vm_state ?? newpc tl (asm_store … st) false   
213                     (op … (cost … st) (cost_of p p' (Iret p)))〉
214].
215
216lemma eval_vmstate_to_Prop : ∀p,p',prog,st1,st2,l.
217eval_vmstate p p' prog st1 = return 〈l,st2〉 → vmstep … prog l st1 st2.
218#p #p' #prog #st1 #st2 #l whd in match eval_vmstate; normalize nodelta
219#H cases(bind_inversion ????? H) -H * normalize nodelta
220[ #seq #opt_l * #EQfetch inversion(asm_is_io ???) normalize nodelta
221  [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H)
222  #newstore * #EQnewstore whd in ⊢ (??%% → ?); #EQ destruct
223  @vm_seq //
224| #newpc * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
225  [ whd in ⊢ (??%% → ?); #EQ destruct] whd in ⊢ (??%% → ?); #EQ destruct
226  @vm_ijump //
227| #cond #new_pc #ltrue #lfase * #EQfetch inversion(asm_is_io ???) normalize nodelta
228  [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H) -H
229  * normalize nodelta * #EQcond whd in ⊢ (??%% → ?); #EQ destruct
230  [ @(vm_cjump_true … EQfetch) // | @(vm_cjump_false … EQfetch) //]
231| #lin #io #lout * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
232  [ #H cases(bind_inversion ????? H) -H #newstore * #EQnewstore ]
233  whd in ⊢ (??%% → ?); #EQ destruct
234  [ @(vm_io_out … EQfetch) // | @(vm_io_in … EQfetch) // ]
235| #f * #EQfetch inversion(asm_is_io ???) #EQio normalize nodelta
236  [ whd in ⊢ (??%% → ?); #EQ destruct ] #H cases (bind_inversion ????? H) -H
237  #lbl * #EQlb whd in ⊢ (??%% → ?); #EQ destruct @(vm_call … EQfetch) //
238| * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
239  [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H
240  * #newpc #tl * whd in match option_pop; normalize nodelta inversion(asm_stack ???)
241  normalize nodelta [#_ whd in ⊢ (??%% → ?); #EQ destruct] #newpc1 #tl1 #_
242  #EQstack whd in ⊢ (??%% → ?); #EQ destruct #H cases(bind_inversion ????? H) #lbl
243  * #EQlbl whd in ⊢ (??%% → ?); #EQ destruct @vm_ret //
244]
245qed.
246
247include "../src/utilities/hide.ma".
248
249discriminator option.
250
251definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p →  abstract_status ≝
252λp,p',prog.mk_abstract_status
253                (vm_state p p')
254                (λl.λst1,st2 : vm_state p p'.(eqb (pc ?? st1) (\snd prog)) = false ∧
255                               vmstep p p' prog l st1 st2)
256                (λ_.λ_.True)
257                (λs.match fetch … prog (pc … s) with
258                    [ Some i ⇒ match i with
259                               [ Seq _ _ ⇒ cl_other
260                               | Ijmp _ ⇒ cl_other
261                               | CJump _ _ _ _ ⇒ cl_jump
262                               | Iio _ _ _ ⇒ if asm_is_io … s then cl_io else cl_other
263                               | Icall _ ⇒ cl_other
264                               | Iret ⇒ cl_other
265                               ]
266                    | None ⇒ cl_other
267                    ]
268                )
269                (λ_.true)
270                (λs.eqb (pc ?? s) O)
271                (λs.eqb (pc … s) (\snd prog))
272                ???.
273@hide_prf cases daemon (*
274[ #s1 #s2 #l inversion(fetch ???) normalize nodelta
275  [ #_ #EQ destruct] * normalize nodelta
276  [ #seq #lbl #_
277  | #n #_
278  | #cond #newpc #ltrue #lfalse #EQfetch
279  | #lin #io #lout #_ cases (asm_is_io ??) normalize nodelta
280  | #f #_
281  | #_
282  ]
283  #EQ destruct * #_ #H inversion H in ⊢ ?;
284  [ #st1 #st2 #i #lbl #EQ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11
285  | #st1 #st2 #new_pc #EQ #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23
286  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35
287  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47
288  | #st1 #st2 #lin #io #lout #EQ #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59
289  | #st1 #st2 #lin #io #lout #EQ #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71
290  | #st1 #st2 #f #EQ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83
291  | #st1 #st2 #new_pc #EQ #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95
292  ]   
293  destruct >EQfetch in EQ; whd in ⊢ (??%% → ?); #EQ
294  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct % //
295| #s1 #s2 #l inversion(fetch ???) normalize nodelta
296  [ #_ #EQ destruct] * normalize nodelta
297  [ #seq #lbl #_
298  | #n #_
299  | #cond #newpc #ltrue #lfalse #_
300  | #lin #io #lout #EQfetch inversion (asm_is_io ??) #EQio normalize nodelta
301  | #f #_
302  | #_
303  ]
304  #EQ destruct * #_ #H inversion H in ⊢ ?;
305  [ #st1 #st2 #i #lbl #EQf #EQio1 #H2 #H3 #H4 #EQio2 #H6 #H7 #H8 #H9 #H10 #H11
306  | #st1 #st2 #new_pc #EQf #EQio1 #H13 #H14 #H15 #EQio2 #H17 #H18 #H19 #H20 #H21 #H22
307  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQf #EQio1 #H26 #H27 #H28 #EQio2 #H30 #H31 #H32 #H33 #H34 #H35
308  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQf #EQio1 #H38 #H39 #H40 #EQio2 #H42 #H43 #H44 #H45 #H46 #H47
309  | #st1 #st2 #lin #io #lout #EQf #EQio1 #H50 #H51 #H52 #EQio2 #H54 #H55 #H56 #H57 #H58 #H59
310  | #st1 #st2 #lin #io #lout #EQf #EQio1 #H61 #H62 #H63 #EQio2 #H65 #H66 #H67 #H68 #H69 #H70
311  | #st1 #st2 #f #EQf #EQio1 #H74 #H75 #H76 #EQio2 #H78 #H79 #H80 #H81 #H82 #H83
312  | #st1 #st2 #new_pc #EQf #EQio1 #H86 #H87 #H88 #EQio2 #H90 #H91 #H92 #H93 #H94 #H95
313  ]   
314  destruct >EQio in EQio2; >EQio1 #EQ destruct %{lin} //
315|  #s1 #s2 #l inversion(fetch ???) normalize nodelta
316  [ #_ #EQ destruct] * normalize nodelta
317  [ #seq #lbl #_
318  | #n #_
319  | #cond #newpc #ltrue #lfalse #EQfetch
320  | #lin #io #lout #EQfetch cases (asm_is_io ??) normalize nodelta
321  | #f #_
322  | #_
323  ]
324  #EQ destruct * #_ #H inversion H in ⊢ ?;
325  [ #st1 #st2 #i #lbl #EQ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11
326  | #st1 #st2 #new_pc #EQ #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23
327  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35
328  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47
329  | #st1 #st2 #lin1 #io1 #lout1 #EQ #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59
330  | #st1 #st2 #lin1 #io1 #lout1 #EQ #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71
331  | #st1 #st2 #f #EQ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83
332  | #st1 #st2 #new_pc #EQ #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95
333  ]   
334  destruct >EQfetch in EQ; whd in ⊢ (??%% → ?); #EQ
335  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct % //
336]*)
337qed.
338
339definition asm_concrete_trans_sys ≝
340λp,p',prog.mk_concrete_transition_sys …
341             (asm_operational_semantics p p' prog) (m … p') (cost …).
342
343definition emits_labels ≝
344λp.λinstr : AssemblerInstr p.match instr with
345        [ Seq _ opt_l ⇒ match opt_l with
346                        [ None ⇒ Some ? (λpc.S pc)
347                        | Some _ ⇒ None ?
348                        ]
349        | Ijmp newpc ⇒ Some ? (λ_.newpc)
350        | _ ⇒ None ?
351        ].
352
353definition fetch_state : ∀p,p'.AssemblerProgram p → vm_state p p' → option (AssemblerInstr p) ≝
354λp,p',prog,st.fetch … prog (pc … st).
355
356definition asm_static_analisys_data ≝ λp,p',prog,abs_t,instr_m.
357mk_static_analysis_data (asm_concrete_trans_sys p p' prog) abs_t
358 … (fetch_state p p' prog) instr_m.
359
360
361let rec block_cost (p : assembler_params)
362 (prog: AssemblerProgram p) (abs_t : monoid)
363 (instr_m : AssemblerInstr p → abs_t)
364 (program_counter: ℕ)
365    (program_size: ℕ)
366        on program_size: option abs_t ≝
367match program_size with
368  [ O ⇒ None ?
369  | S program_size' ⇒
370    if eqb program_counter (\snd prog) then
371       return e … abs_t
372    else
373    ! instr ← fetch … prog program_counter;
374    ! n ← (match emits_labels … instr with
375          [ Some f ⇒ block_cost … prog abs_t instr_m (f program_counter) program_size'
376          | None ⇒ return e …
377          ]);
378    return (op … abs_t (instr_m … instr) n)
379  ].
380 
381axiom initial_act : CostLabel.
382 
383record cost_map_T (dom : DeqSet) (codom : Type[0]) : Type[1] ≝
384{ map_type :> Type[0]
385; empty_map : map_type
386; get_map : map_type → dom → option codom
387; set_map : map_type → dom → codom → map_type
388; get_set_hit : ∀k,v,m.get_map (set_map m k v) k = return v
389; get_set_miss : ∀k1,k2,v,m.(k1 == k2) = false → get_map (set_map m k1 v) k2 = get_map m k2
390}.
391
392let rec labels_pc (p : assembler_params)
393(prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝
394match prog with
395[ nil ⇒ [〈initial_act,O〉] @
396        map … (λx.let〈y,z〉 ≝ x in 〈a_call z,y〉) (call_label_fun … p) @
397        map … (λx.let〈y,z〉 ≝ x in 〈a_return_post z,y〉) (return_label_fun … p)
398| cons i is ⇒
399  match i with
400  [ Seq _ opt_l ⇒ match opt_l with
401                  [ Some lbl ⇒ [〈a_non_functional_label lbl,S program_counter〉]
402                  | None ⇒ [ ]
403                  ]
404  | Ijmp _ ⇒ [ ]
405  | CJump _ newpc ltrue lfalse ⇒ [〈a_non_functional_label ltrue,newpc〉;〈a_non_functional_label lfalse,S program_counter〉]
406  | Iio lin _ lout ⇒ [〈a_non_functional_label lout,S program_counter〉]
407  | Icall f ⇒ [ ]
408  | Iret ⇒ [ ]
409  ] @ labels_pc p is (S program_counter)             
410].
411
412definition static_analisys : ∀p : assembler_params.∀abs_t : monoid.(AssemblerInstr p → abs_t) →
413∀mT : cost_map_T DEQCostLabel abs_t.AssemblerProgram p → option mT ≝
414λp,abs_t,instr_m,mT,prog.
415let 〈instrs,final〉 ≝ prog in
416let prog_size ≝ S (|instrs|) in
417m_fold Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m w prog_size; 
418                               return set_map … m z k) (labels_pc … instrs O)
419      (empty_map ?? mT).
420
421(*falso: necessita di no_duplicates*)
422axiom static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map.
423static_analisys p abs_t instr_m mT prog = return map →
424mem … 〈lbl,pc〉 (labels_pc … (\fst prog) O) →
425get_map … map lbl = block_cost … prog abs_t instr_m pc (S (|(\fst prog)|)). 
426
427include "Simulation.ma".
428
429record terminated_trace (S : abstract_status) (R_s2 : S) : Type[0] ≝
430{  R_post_step : option (ActionLabel × S)
431 ; R_fin_ok : match R_post_step with
432               [ None ⇒ bool_to_Prop (as_final … R_s2)
433               | Some x ⇒ let 〈l,R_post_state〉≝ x in
434                          (is_costlabelled_act l ∨ is_labelled_ret_act l) ∧
435                          (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧
436                          as_execute … l R_s2 R_post_state
437               ]
438 }.
439 
440axiom vm_step_to_eval : ∀p,p',prog,st1,st2,l.vmstep … prog l st1 st2 →
441eval_vmstate p p' prog st1 = return 〈l,st2〉.
442
443coercion vm_step_to_eval.
444
445definition big_op: ∀M: monoid. list M → M ≝
446 λM. foldl … (op … M) (e … M).
447
448lemma big_op_associative:
449 ∀M:monoid. ∀l1,l2.
450  big_op M (l1@l2) = op M (big_op … l1) (big_op … l2).
451 #M #l1 whd in match big_op; normalize nodelta
452 generalize in match (e M) in ⊢ (? → (??%(??%?))); elim l1
453 [ #c #l2 whd in match (append ???); normalize lapply(neutral_r … c)
454   generalize in match c in ⊢ (??%? → ???%); lapply c -c lapply(e M)
455   elim l2 normalize
456   [ #c #c1 #c2 #EQ @sym_eq //
457   | #x #xs #IH #c1 #c2 #c3 #EQ <EQ <IH [% | <is_associative % |]
458   ]
459 | #x #xs #IH #c #l2 @IH
460 ]
461qed.
462
463lemma act_big_op : ∀M,B. ∀act : monoid_action M B.
464 ∀l1,l2,x.
465   act (big_op M (l1@l2)) x = act (big_op … l2) (act (big_op … l1) x).
466 #M #B #act #l1 elim l1
467 [ #l2 #x >act_neutral //
468 | #hd #tl #IH #l2 #x change with ([?]@(tl@l2)) in match ([?]@(tl@l2));
469   >big_op_associative >act_op >IH change with ([hd]@tl) in match ([hd]@tl);
470   >big_op_associative >act_op in ⊢ (???%); %
471 ]
472qed.
473
474lemma static_dynamic : ∀p,p',prog.
475∀abs_t : abstract_transition_sys (m … p').∀instr_m.
476∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1.
477static_analisys p ? instr_m mT prog = return map1 →
478∀st1,st2 : vm_state p p'.
479∀ter : terminated_trace (asm_operational_semantics p p' prog) st2.
480∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
481∀k.
482pre_measurable_trace … t →
483block_cost p prog … instr_m (pc … st1) (S (|(\fst prog)|)) = return k →
484∀a1.rel_galois … good st1 a1 →
485let stop_state ≝ match R_post_step … ter with [None ⇒ st2 | Some x ⇒ \snd x ] in
486∀costs.
487costs = map … (λlbl.(opt_safe … (get_map … map1 lbl) ?)) (get_costlabels_of_trace …  t) →
488rel_galois … good stop_state (act_abs … abs_t (big_op … costs) (act_abs … abs_t k a1)).
489[2: @hide_prf cases daemon]
490#p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #ter #t
491lapply ter -ter elim t
492[ #st #ter inversion(R_post_step … ter) normalize nodelta [| * #lbl #st3 ]
493  #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta
494  [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st
495    normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
496    #a1 #rel_st_a1 whd in match (map ????); #costs #EQ >EQ >act_neutral >act_neutral assumption
497  | ** #H1 #H2 * #H3 #H4 whd in ⊢ (??%% → ?); >H3 normalize nodelta
498    #H cases(bind_inversion ????? H) -H *
499    [ #seq * [|#lbl1]
500    | #newpc
501    | #cond #newpc #ltrue #lfalse
502    | #lin #io #lout
503    | #f
504    |
505    ]
506    * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate;
507    normalize nodelta >EQfetch >m_return_bind normalize nodelta
508    cases(asm_is_io ??) normalize nodelta
509    [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
510    |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_
511      [3: cases x normalize nodelta
512      |6: #H cases(bind_inversion ????? H) -H #y * #_
513      ]
514    ]
515    whd in ⊢ (??%% → ?); #EQ destruct
516    [4,8: cases H1 [1,3: * |*: * #y #EQ destruct]]
517    >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
518    #a1 #good_st_a1 whd in match (map ????); #costs #EQ >EQ >neutral_r
519    >act_neutral
520    @(instr_map_ok … good … EQfetch … good_st_a1) /2/
521  ]
522| -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H
523  #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????);
524  whd #costs <map_append #EQ destruct >big_op_associative >act_op @IH
525  [   
526  inversion H in ⊢ ?;
527  [ #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct
528  | #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_
529    #EQ1 #EQ2 #EQ3 #EQ4 destruct
530  | #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_
531    #EQ1 #EQ2 #EQ3 #EQ4 destruct
532  | #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct
533    * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
534  | #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
535  ] //
536  | whd in H2 : (??%?); >H3 in H2; normalize nodelta #H
537    cases(bind_inversion ????? H) #i * #EQi whd in match (emits_labels ??);
538 
539  inversion l [#fn #lbl | * [|#lbl] | * [|#lbl] ] #EQlbl normalize nodelta
540  inversion (R_post_step ???) [|2,4,6,8,10,12,14,16: * #post_lbl #post_state]
541  #EQR_post_step normalize nodelta lapply (IH ter) -IH
542  >EQR_post_step normalize nodelta #IH
543  whd in match (foldl ?????);
544  [ >act_op @IH
545  try (> act_op)
546
547
548
549
550
551
552  whd in ⊢ (??%% → ?); [ >H1 in ⊢ (% → ?); | >H1 in ⊢ (% → ?); | >H1 in ⊢ (% → ?);]
553  normalize nodelta lapply(vm_step_to_eval … H2) whd in match eval_vmstate;
554  normalize nodelta #H cases(bind_inversion ????? H) -H * normalize nodelta
555  [1,7,13: #seq * [2,4,6: #lbl1]
556  |2,8,14: #newpc
557  |3,9,15: #cond #newpc #ltrue #lfalse
558  |4,10,16: #lin #io #lout
559  |5,11,17: #f
560  |*:
561  ] * normalize nodelta #EQfetch
562  [13,14,15: whd in s1_noio : (?(??%?)); >EQfetch in s1_noio;
563    normalize nodelta cases(asm_is_io ???) normalize nodelta
564    [1,3,5: * #H @⊥ @H % ] #_
565  |*: cases(asm_is_io ???) normalize nodelta
566     [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35:
567        whd in ⊢ (??%% → ?); #EQ destruct]
568  [13   
569   
570     #i * #EQi #H cases(bind_inversion ????? H) -H #el
571    inversion H4
572    [ #s1 #s2 #i1 * [| #lbl] #EQfetch #no_io #EQstore #EQstack #EQio #EQpc
573      #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct >EQi in EQfetch; whd in ⊢ (??%% → ?);
574      #EQ destruct whd in match emits_labels; normalize nodelta
575      [ cases H1 whd in ⊢ (% → ?); [ * |  #EQ destruct]]
576      * whd in ⊢ (??%% → ?); #EQ destruct >neutral whd in ⊢ (??%% → ?);
577      #EQ destruct whd in match (foldr ?????);
578
579
580
581
Note: See TracBrowser for help on using the repository browser.