source: LTS/Vm.ma @ 3449

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

clean up

File size: 20.7 KB
Line 
1include "Traces.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 monoid: Type[1] ≝
15 { carrier :> Type[0]
16 ; op: carrier → carrier → carrier
17 ; e: carrier
18 ; neutral: ∀x. op … x e = x
19 ; is_associative: ∀x,y,z. op … (op … x y) z = op … x (op … y z)
20 }.
21
22record assembler_params : Type[1] ≝
23{ seq_instr : Type[0]
24; jump_condition : Type[0]
25; io_instr : Type[0]
26; entry_of_function : FunctionName → ℕ
27; call_label_fun : list (ℕ × CallCostLabel)
28; return_label_fun : list (ℕ × ReturnPostCostLabel)
29}.
30
31inductive AssemblerInstr (p : assembler_params) : Type[0] ≝
32| Seq : seq_instr p → option (NonFunctionalLabel) →  AssemblerInstr p
33| Ijmp: ℕ → AssemblerInstr p
34| CJump : jump_condition p → ℕ → NonFunctionalLabel → NonFunctionalLabel → AssemblerInstr p
35| Iio : NonFunctionalLabel → io_instr p → NonFunctionalLabel → AssemblerInstr p
36| Icall: FunctionName → AssemblerInstr p
37| Iret: AssemblerInstr p.
38
39definition AssemblerProgram ≝λp.list (AssemblerInstr p) × ℕ.
40
41definition fetch: ∀p.AssemblerProgram p → ℕ → option (AssemblerInstr p) ≝
42 λp,l,n. nth_opt ? n (\fst l).
43
44definition stackT: Type[0] ≝ list (nat).
45
46record sem_params (p : assembler_params) : Type[1] ≝
47{ m : monoid
48; asm_store_type : Type[0]
49; eval_asm_seq : seq_instr p → asm_store_type → option asm_store_type
50; eval_asm_cond : jump_condition p → asm_store_type → option bool
51; eval_asm_io : io_instr p → asm_store_type → option asm_store_type
52; cost_of_io : io_instr p → asm_store_type → m
53; cost_of : AssemblerInstr p → m
54}.
55
56record vm_state (p : assembler_params) (p' : sem_params p) : Type[0] ≝
57{ pc : ℕ
58; asm_stack : stackT
59; asm_store : asm_store_type … p'
60; asm_is_io : bool
61; cost : m … p'
62}.
63
64definition label_of_pc ≝ λL.λl.λpc.find …
65   (λp.let 〈x,y〉 ≝ p in if eqb x pc then Some L y else None ? ) l.
66   
67definition option_pop ≝
68  λA.λl:list A. match l with
69  [ nil ⇒ None ?
70  | cons a tl ⇒ Some ? (〈a,tl〉) ].
71
72
73inductive vmstep (p : assembler_params) (p' : sem_params p)
74   (prog : AssemblerProgram p)  :
75      ActionLabel → relation (vm_state p p') ≝
76| vm_seq : ∀st1,st2 : vm_state p p'.∀i,l.
77           fetch … prog (pc … st1) = return (Seq p i l) →
78           asm_is_io … st1 = false →
79           eval_asm_seq p p' i (asm_store … st1) = return asm_store … st2 → 
80           asm_stack … st1 = asm_stack … st2 →
81           asm_is_io … st1 = asm_is_io … st2 →
82           S (pc … st1) = pc … st2 →
83           op … (cost … st1) (cost_of p p' (Seq p i l)) = cost … st2 →
84           vmstep … (cost_act l) st1 st2
85| vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ.
86           fetch … prog (pc … st1) = return (Ijmp p new_pc) →
87           asm_is_io … st1 = false →
88           asm_store … st1 = asm_store … st2 →
89           asm_stack … st1 = asm_stack … st2 →
90           asm_is_io … st1 = asm_is_io … st2 →
91           new_pc = pc … st2 →
92           op … (cost … st1) (cost_of p p' (Ijmp … new_pc)) = cost … st2 →
93           vmstep … (cost_act (None ?)) st1 st2
94| vm_cjump_true :
95           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
96           eval_asm_cond p p' cond (asm_store … st1) = return true→
97           fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) →
98           asm_is_io … st1 = false →
99           asm_store … st1 = asm_store … st2 →
100           asm_stack … st1 = asm_stack … st2 →
101           asm_is_io … st1 = asm_is_io … st2 →
102           pc … st2 = new_pc →
103           op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse)) = cost … st2 →
104           vmstep … (cost_act (Some ? ltrue)) st1 st2
105| vm_cjump_false :
106           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
107           eval_asm_cond p p' cond (asm_store … st1) = return false→
108           fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) →
109           asm_is_io … st1 = false →
110           asm_store … st1 = asm_store … st2 →
111           asm_stack … st1 = asm_stack … st2 →
112           asm_is_io … st1 = asm_is_io … st2 →
113           S (pc … st1) = pc … st2 →
114           op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse)) = cost … st2 →
115           vmstep … (cost_act (Some ? lfalse)) st1 st2
116| vm_io_in : 
117           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
118           fetch … prog (pc … st1) = return (Iio p lin io lout) →
119           asm_is_io … st1 = false →
120           asm_store … st1 = asm_store … st2 →
121           asm_stack … st1 = asm_stack … st2 →
122           true = asm_is_io … st2 →
123           pc … st1 = pc … st2 →
124           cost … st1 = cost … st2 →
125           vmstep … (cost_act (Some ? lin)) st1 st2
126| vm_io_out :
127           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
128           fetch … prog (pc … st1) = return (Iio p lin io lout) →
129           asm_is_io … st1 = true →
130           eval_asm_io … io (asm_store … st1) = return asm_store … st2 →
131           asm_stack … st1 = asm_stack … st2 →
132           false = asm_is_io … st2 →
133           S (pc … st1) = pc … st2 →
134           op … (cost … st1) (cost_of_io p p' io (asm_store … st1)) = cost … st2 →
135           vmstep … (cost_act (Some ? lout)) st1 st2
136| vm_call :
137           ∀st1,st2 : vm_state p p'.∀f,lbl.
138           fetch … prog (pc … st1) = return (Icall p f) →
139           asm_is_io … st1 = false →
140           asm_store … st1 = asm_store … st2 →
141           S (pc … st1) ::  asm_stack … st1 = asm_stack … st2 →
142           asm_is_io … st1 = asm_is_io … st2 →
143           entry_of_function p  f = pc … st2 →
144           op … (cost … st1) (cost_of p p' (Icall p f)) = cost … st2 →
145           label_of_pc ? (call_label_fun p) (entry_of_function p f) = return lbl →
146           vmstep … (call_act f lbl) st1 st2
147| vm_ret :
148          ∀st1,st2 : vm_state p p'.∀newpc,lbl.
149           fetch … prog (pc … st1) = return (Iret p) →
150           asm_is_io … st1 = false →
151           asm_store … st1 = asm_store … st2 →
152           asm_stack … st1 = newpc ::  asm_stack … st2  →
153           asm_is_io … st1 = asm_is_io … st2 →
154           newpc = pc … st2 →
155           label_of_pc ? (return_label_fun p) newpc = return lbl →
156           op … (cost … st1) (cost_of p p' (Iret p)) = cost … st2 →
157           vmstep … (ret_act (Some ? lbl)) st1 st2.
158
159definition eval_vmstate : ∀p : assembler_params.∀p' : sem_params p.
160AssemblerProgram p → vm_state p p' → option (ActionLabel × (vm_state p p')) ≝
161λp,p',prog,st.
162! i ← fetch … prog (pc … st);
163match i with
164[ Seq x opt_l ⇒
165   if asm_is_io … st then
166     None ?
167   else
168     ! new_store ← eval_asm_seq p p' x (asm_store … st);
169     return 〈cost_act opt_l,
170             mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false
171                (op … (cost … st) (cost_of p p' (Seq p x opt_l)))〉
172| Ijmp newpc ⇒
173   if asm_is_io … st then
174     None ?
175   else
176     return 〈cost_act (None ?),
177             mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
178                (op … (cost … st) (cost_of p p' (Ijmp … newpc)))〉
179| CJump cond newpc ltrue lfalse ⇒
180   if asm_is_io … st then
181     None ?
182   else
183     ! b ← eval_asm_cond p p' cond (asm_store … st);
184     if b then
185       return 〈cost_act (Some ? ltrue),
186               mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
187                (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse)))〉
188     else
189       return 〈cost_act (Some ? lfalse),
190               mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false
191                (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse)))〉
192| Iio lin io lout ⇒
193              if asm_is_io … st then
194                 ! new_store ← eval_asm_io … io (asm_store … st);
195                 return 〈cost_act (Some ? lout),
196                         mk_vm_state ?? (S (pc … st)) (asm_stack … st)
197                         new_store false
198                         (op … (cost … st)
199                               (cost_of_io p p' io (asm_store … st)))〉   
200              else
201                return 〈cost_act (Some ? lin),
202                        mk_vm_state ?? (pc … st) (asm_stack … st) (asm_store … st)
203                                    true (cost … st)〉
204| Icall f ⇒
205    if asm_is_io … st then
206      None ?
207    else
208      ! lbl ← label_of_pc ? (call_label_fun p) (entry_of_function p f);
209      return 〈call_act f lbl,
210              mk_vm_state ?? (entry_of_function p f)
211                             ((S (pc … st)) :: (asm_stack … st))
212                             (asm_store … st) false
213                             (op … (cost … st) (cost_of p p' (Icall p f)))〉
214| Iret ⇒ if asm_is_io … st then
215            None ?
216         else
217            ! 〈newpc,tl〉 ← option_pop … (asm_stack … st);
218            ! lbl ← label_of_pc ? (return_label_fun p) newpc;
219            return 〈ret_act (Some ? lbl),
220                    mk_vm_state ?? newpc tl (asm_store … st) false   
221                     (op … (cost … st) (cost_of p p' (Iret p)))〉
222].
223
224lemma eval_vmstate_to_Prop : ∀p,p',prog,st1,st2,l.
225eval_vmstate p p' prog st1 = return 〈l,st2〉 → vmstep … prog l st1 st2.
226#p #p' #prog #st1 #st2 #l whd in match eval_vmstate; normalize nodelta
227#H cases(bind_inversion ????? H) -H * normalize nodelta
228[ #seq #opt_l * #EQfetch inversion(asm_is_io ???) normalize nodelta
229  [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H)
230  #newstore * #EQnewstore whd in ⊢ (??%% → ?); #EQ destruct
231  @vm_seq //
232| #newpc * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
233  [ whd in ⊢ (??%% → ?); #EQ destruct] whd in ⊢ (??%% → ?); #EQ destruct
234  @vm_ijump //
235| #cond #new_pc #ltrue #lfase * #EQfetch inversion(asm_is_io ???) normalize nodelta
236  [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H) -H
237  * normalize nodelta * #EQcond whd in ⊢ (??%% → ?); #EQ destruct
238  [ @(vm_cjump_true … EQfetch) // | @(vm_cjump_false … EQfetch) //]
239| #lin #io #lout * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
240  [ #H cases(bind_inversion ????? H) -H #newstore * #EQnewstore ]
241  whd in ⊢ (??%% → ?); #EQ destruct
242  [ @(vm_io_out … EQfetch) // | @(vm_io_in … EQfetch) // ]
243| #f * #EQfetch inversion(asm_is_io ???) #EQio normalize nodelta
244  [ whd in ⊢ (??%% → ?); #EQ destruct ] #H cases (bind_inversion ????? H) -H
245  #lbl * #EQlb whd in ⊢ (??%% → ?); #EQ destruct @(vm_call … EQfetch) //
246| * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
247  [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H
248  * #newpc #tl * whd in match option_pop; normalize nodelta inversion(asm_stack ???)
249  normalize nodelta [#_ whd in ⊢ (??%% → ?); #EQ destruct] #newpc1 #tl1 #_
250  #EQstack whd in ⊢ (??%% → ?); #EQ destruct #H cases(bind_inversion ????? H) #lbl
251  * #EQlbl whd in ⊢ (??%% → ?); #EQ destruct @vm_ret //
252]
253qed.
254
255include "../src/utilities/hide.ma".
256
257discriminator option.
258
259definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p →  abstract_status ≝
260λp,p',prog.mk_abstract_status
261                (vm_state p p')
262                (λl.λst1,st2 : vm_state p p'.(eqb (pc ?? st1) (\snd prog)) = false ∧
263                               vmstep p p' prog l st1 st2)
264                (λ_.λ_.True)
265                (λs.match fetch … prog (pc … s) with
266                    [ Some i ⇒ match i with
267                               [ Seq _ _ ⇒ cl_other
268                               | Ijmp _ ⇒ cl_other
269                               | CJump _ _ _ _ ⇒ cl_jump
270                               | Iio _ _ _ ⇒ if asm_is_io … s then cl_io else cl_other
271                               | Icall _ ⇒ cl_other
272                               | Iret ⇒ cl_other
273                               ]
274                    | None ⇒ cl_other
275                    ]
276                )
277                (λ_.true)
278                (λs.eqb (pc ?? s) O)
279                (λs.eqb (pc … s) (\snd prog))
280                ???.
281@hide_prf cases daemon (*
282[ #s1 #s2 #l inversion(fetch ???) normalize nodelta
283  [ #_ #EQ destruct] * normalize nodelta
284  [ #seq #lbl #_
285  | #n #_
286  | #cond #newpc #ltrue #lfalse #EQfetch
287  | #lin #io #lout #_ cases (asm_is_io ??) normalize nodelta
288  | #f #_
289  | #_
290  ]
291  #EQ destruct * #_ #H inversion H in ⊢ ?;
292  [ #st1 #st2 #i #lbl #EQ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11
293  | #st1 #st2 #new_pc #EQ #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23
294  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35
295  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47
296  | #st1 #st2 #lin #io #lout #EQ #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59
297  | #st1 #st2 #lin #io #lout #EQ #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71
298  | #st1 #st2 #f #EQ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83
299  | #st1 #st2 #new_pc #EQ #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95
300  ]   
301  destruct >EQfetch in EQ; whd in ⊢ (??%% → ?); #EQ
302  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct % //
303| #s1 #s2 #l inversion(fetch ???) normalize nodelta
304  [ #_ #EQ destruct] * normalize nodelta
305  [ #seq #lbl #_
306  | #n #_
307  | #cond #newpc #ltrue #lfalse #_
308  | #lin #io #lout #EQfetch inversion (asm_is_io ??) #EQio normalize nodelta
309  | #f #_
310  | #_
311  ]
312  #EQ destruct * #_ #H inversion H in ⊢ ?;
313  [ #st1 #st2 #i #lbl #EQf #EQio1 #H2 #H3 #H4 #EQio2 #H6 #H7 #H8 #H9 #H10 #H11
314  | #st1 #st2 #new_pc #EQf #EQio1 #H13 #H14 #H15 #EQio2 #H17 #H18 #H19 #H20 #H21 #H22
315  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQf #EQio1 #H26 #H27 #H28 #EQio2 #H30 #H31 #H32 #H33 #H34 #H35
316  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQf #EQio1 #H38 #H39 #H40 #EQio2 #H42 #H43 #H44 #H45 #H46 #H47
317  | #st1 #st2 #lin #io #lout #EQf #EQio1 #H50 #H51 #H52 #EQio2 #H54 #H55 #H56 #H57 #H58 #H59
318  | #st1 #st2 #lin #io #lout #EQf #EQio1 #H61 #H62 #H63 #EQio2 #H65 #H66 #H67 #H68 #H69 #H70
319  | #st1 #st2 #f #EQf #EQio1 #H74 #H75 #H76 #EQio2 #H78 #H79 #H80 #H81 #H82 #H83
320  | #st1 #st2 #new_pc #EQf #EQio1 #H86 #H87 #H88 #EQio2 #H90 #H91 #H92 #H93 #H94 #H95
321  ]   
322  destruct >EQio in EQio2; >EQio1 #EQ destruct %{lin} //
323|  #s1 #s2 #l inversion(fetch ???) normalize nodelta
324  [ #_ #EQ destruct] * normalize nodelta
325  [ #seq #lbl #_
326  | #n #_
327  | #cond #newpc #ltrue #lfalse #EQfetch
328  | #lin #io #lout #EQfetch cases (asm_is_io ??) normalize nodelta
329  | #f #_
330  | #_
331  ]
332  #EQ destruct * #_ #H inversion H in ⊢ ?;
333  [ #st1 #st2 #i #lbl #EQ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11
334  | #st1 #st2 #new_pc #EQ #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23
335  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35
336  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47
337  | #st1 #st2 #lin1 #io1 #lout1 #EQ #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59
338  | #st1 #st2 #lin1 #io1 #lout1 #EQ #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71
339  | #st1 #st2 #f #EQ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83
340  | #st1 #st2 #new_pc #EQ #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95
341  ]   
342  destruct >EQfetch in EQ; whd in ⊢ (??%% → ?); #EQ
343  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct % //
344]*)
345qed.
346
347definition emits_labels ≝
348λp.λinstr : AssemblerInstr p.match instr with
349        [ Seq _ opt_l ⇒ match opt_l with
350                        [ None ⇒ Some ? (λpc.S pc)
351                        | Some _ ⇒ None ?
352                        ]
353        | Ijmp newpc ⇒ Some ? (λ_.newpc)
354        | _ ⇒ None ?
355        ].
356
357
358let rec block_cost (p : assembler_params) (p' : sem_params p)
359 (prog: AssemblerProgram p) (program_counter: ℕ)
360    (program_size: ℕ)
361        on program_size: option (m … p') ≝
362match program_size with
363  [ O ⇒ None ?
364  | S program_size' ⇒
365    if eqb program_counter (\snd prog) then
366       return e … (m … p')
367    else
368    ! instr ← fetch … prog program_counter;
369    ! n ← (match emits_labels … instr with
370          [ Some f ⇒ block_cost … prog (f program_counter) program_size'
371          | None ⇒ return e …
372          ]);
373    return (op … (m … p') (cost_of p p' instr) n)
374  ].
375 
376axiom initial_act : CostLabel.
377 
378record cost_map_T (dom : DeqSet) (codom : Type[0]) : Type[1] ≝
379{ map_type :> Type[0]
380; empty_map : map_type
381; get_map : map_type → dom → option codom
382; set_map : map_type → dom → codom → map_type
383; get_set_hit : ∀k,v,m.get_map (set_map m k v) k = return v
384; get_set_miss : ∀k1,k2,v,m.(k1 == k2) = false → get_map (set_map m k1 v) k2 = get_map m k2
385}.
386
387let rec labels_pc (p : assembler_params)
388(prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝
389match prog with
390[ nil ⇒ [〈initial_act,O〉] @
391        map … (λx.let〈y,z〉 ≝ x in 〈a_call z,y〉) (call_label_fun … p) @
392        map … (λx.let〈y,z〉 ≝ x in 〈a_return_post z,y〉) (return_label_fun … p)
393| cons i is ⇒
394  match i with
395  [ Seq _ opt_l ⇒ match opt_l with
396                  [ Some lbl ⇒ [〈a_non_functional_label lbl,S program_counter〉]
397                  | None ⇒ [ ]
398                  ]
399  | Ijmp _ ⇒ [ ]
400  | CJump _ newpc ltrue lfalse ⇒ [〈a_non_functional_label ltrue,newpc〉;〈a_non_functional_label lfalse,S program_counter〉]
401  | Iio lin _ lout ⇒ [〈a_non_functional_label lout,S program_counter〉]
402  | Icall f ⇒ [ ]
403  | Iret ⇒ [ ]
404  ] @ labels_pc p is (S program_counter)             
405].
406
407definition static_analisys : ∀p : assembler_params.∀ p' : sem_params p.
408∀mT : cost_map_T DEQCostLabel (m … p').AssemblerProgram p → option mT ≝
409λp,p',mT,prog.
410let 〈instrs,final〉 ≝ prog in
411let prog_size ≝ S (|instrs|) in
412m_fold Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost … prog w prog_size; 
413                               return set_map … m z k) (labels_pc … instrs O)
414      (empty_map ?? mT).
415
416(*falso: necessita di no_duplicates*)
417axiom static_analisys_ok : ∀p,p',mT,prog,lbl,pc,map.
418static_analisys p p' mT prog = return map →
419mem … 〈lbl,pc〉 (labels_pc … (\fst prog) O) →
420get_map … map lbl = block_cost … prog pc (S (|(\fst prog)|)). 
421
422include "Simulation.ma".
423
424record terminated_trace (S : abstract_status) (L_s1,R_s2) (trace: raw_trace S L_s1 R_s2)
425 : Prop ≝
426 { R_label : option ActionLabel
427 ; R_post_state : option S
428 ; R_fin_ok : match R_label with
429               [ None ⇒ bool_to_Prop (as_final … R_s2) ∧ R_post_state = None ?
430               | Some l ⇒ (is_costlabelled_act l ∨ is_unlabelled_ret_act l) ∧
431                          (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧
432                          ∃ s'.R_post_state = Some ? s' ∧ as_execute … l R_s2 s'
433               ]
434 }.
435 
436lemma static_dynamic : ∀p,p',prog,k,mT,map.
437static_analisys p p' mT prog = return map →
438∀st1,st2 : vm_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
439pre_measurable_trace … t → terminated_trace … t →
440block_cost … prog (pc … st1) (S (|(\fst prog)|)) = return k →
441op … (m … p') (cost … st1)
442 (foldr ?? (λlbl,k1.op … (opt_safe … (get_map … map lbl) ?) k1)
443     k (get_costlabels_of_trace … t)) = cost … st2.
444[2: cases daemon]
445#p #p' #prog #k #mT #map #EQmap #st1 #st2 #t elim t
446[ #st #_ ** [|#r_lab] normalize nodelta #opt_r_state
447  [ * whd in ⊢ (?% → ?); #final_st #_ whd in ⊢ (??%? → ?); >final_st
448    normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
449    >neutral %
450  | ** #H1 #H2 * #post_st * #EQ destruct * #H3 #H4 whd in ⊢ (??%? → ?);
451    >H3 normalize nodelta #H cases(bind_inversion ????? H) -H
452    #i * #EQi #H cases(bind_inversion ????? H) -H #el
453    inversion H4
454    [ #s1 #s2 #i1 * [| #lbl] #EQfetch #no_io #EQstore #EQstack #EQio #EQpc
455      #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct >EQi in EQfetch; whd in ⊢ (??%% → ?);
456      #EQ destruct whd in match emits_labels; normalize nodelta
457      [ cases H1 whd in ⊢ (% → ?); [ * |  #EQ destruct]]
458      * whd in ⊢ (??%% → ?); #EQ destruct >neutral whd in ⊢ (??%% → ?);
459      #EQ destruct whd in match (foldr ?????);
460
461
462
463
Note: See TracBrowser for help on using the repository browser.