source: LTS/Vm.ma @ 3488

Last change on this file since 3488 was 3488, checked in by sacerdot, 5 years ago

One proof repaired.

File size: 42.2 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
19inductive AssemblerInstr (p : assembler_params) : Type[0] ≝
20| Seq : seq_instr p → option (NonFunctionalLabel) →  AssemblerInstr p
21| Ijmp: ℕ → AssemblerInstr p
22| CJump : jump_condition p → ℕ → NonFunctionalLabel → NonFunctionalLabel → AssemblerInstr p
23| Iio : NonFunctionalLabel → io_instr p → NonFunctionalLabel → AssemblerInstr p
24| Icall: FunctionName → AssemblerInstr p
25| Iret: AssemblerInstr p.
26
27definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (CostLabel × ℕ) ≝
28λp,i,program_counter.
29match i with
30  [ Seq _ opt_l ⇒ match opt_l with
31                  [ Some lbl ⇒ [〈(a_non_functional_label lbl),S program_counter〉]
32                  | None ⇒ [ ]
33                  ]
34  | Ijmp _ ⇒ [ ]
35  | CJump _ newpc ltrue lfalse ⇒ [〈(a_non_functional_label ltrue),newpc〉;
36                                  〈(a_non_functional_label lfalse),S program_counter〉]
37  | Iio lin _ lout ⇒ [〈(a_non_functional_label lin),program_counter〉;
38                      〈(a_non_functional_label lout),S program_counter〉]
39  | Icall f ⇒ [ ]
40  | Iret ⇒ [ ]
41  ].
42
43let rec labels_pc (p : assembler_params)
44(prog : list (AssemblerInstr p)) (call_label_fun : list (ℕ × CallCostLabel))
45              (return_label_fun : list (ℕ × ReturnPostCostLabel)) (i_act : NonFunctionalLabel)
46              (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝
47match prog with
48[ nil ⇒ [〈a_non_functional_label (i_act),O〉] @
49        map … (λx.let〈y,z〉 ≝ x in 〈(a_call z),y〉) (call_label_fun) @
50        map … (λx.let〈y,z〉 ≝ x in 〈(a_return_post z),y〉) (return_label_fun)
51| cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p is call_label_fun return_label_fun i_act (S program_counter)
52].
53
54include "basics/lists/listb.ma".
55
56(*doppione da mettere a posto*)
57let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝
58match l with
59[ nil ⇒ True
60| cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs
61].
62
63
64record AssemblerProgram (p : assembler_params) : Type[0] ≝
65{ instructions : list (AssemblerInstr p)
66; endmain : ℕ
67; endmain_ok : endmain < |instructions|
68; entry_of_function : FunctionName → ℕ
69; call_label_fun : list (ℕ × CallCostLabel)
70; return_label_fun : list (ℕ × ReturnPostCostLabel)
71; in_act : NonFunctionalLabel
72; asm_no_duplicates : no_duplicates … (map ?? \fst … (labels_pc … instructions call_label_fun return_label_fun in_act O))
73}.
74
75
76definition fetch: ∀p.AssemblerProgram p → ℕ → option (AssemblerInstr p) ≝
77 λp,l,n. nth_opt ? n (instructions … l).
78
79definition stackT: Type[0] ≝ list (nat).
80
81record sem_params (p : assembler_params) : Type[1] ≝
82{ m : monoid
83; asm_store_type : Type[0]
84; eval_asm_seq : seq_instr p → asm_store_type → option asm_store_type
85; eval_asm_cond : jump_condition p → asm_store_type → option bool
86; eval_asm_io : io_instr p → asm_store_type → option asm_store_type
87; cost_of_io : io_instr p → asm_store_type → m
88; cost_of : AssemblerInstr p → asm_store_type →  m
89}.
90
91record vm_state (p : assembler_params) (p' : sem_params p) : Type[0] ≝
92{ pc : ℕ
93; asm_stack : stackT
94; asm_store : asm_store_type … p'
95; asm_is_io : bool
96; cost : m … p'
97}.
98
99definition label_of_pc ≝ λL.λl.λpc.find …
100   (λp.let 〈x,y〉 ≝ p in if eqb x pc then Some L y else None ? ) l.
101   
102definition option_pop ≝
103  λA.λl:list A. match l with
104  [ nil ⇒ None ?
105  | cons a tl ⇒ Some ? (〈a,tl〉) ].
106
107
108inductive vmstep (p : assembler_params) (p' : sem_params p)
109   (prog : AssemblerProgram p)  :
110      ActionLabel → relation (vm_state p p') ≝
111| vm_seq : ∀st1,st2 : vm_state p p'.∀i,l.
112           fetch … prog (pc … st1) = return (Seq p i l) →
113           asm_is_io … st1 = false →
114           eval_asm_seq p p' i (asm_store … st1) = return asm_store … st2 → 
115           asm_stack … st1 = asm_stack … st2 →
116           asm_is_io … st1 = asm_is_io … st2 →
117           S (pc … st1) = pc … st2 →
118           op … (cost … st1) (cost_of p p' (Seq p i l) (asm_store … st1)) = cost … st2 →
119           vmstep … (cost_act l) st1 st2
120| vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ.
121           fetch … prog (pc … st1) = return (Ijmp p new_pc) →
122           asm_is_io … st1 = false →
123           asm_store … st1 = asm_store … st2 →
124           asm_stack … st1 = asm_stack … st2 →
125           asm_is_io … st1 = asm_is_io … st2 →
126           new_pc = pc … st2 →
127           op … (cost … st1) (cost_of p p' (Ijmp … new_pc) (asm_store … st1)) = cost … st2 →
128           vmstep … (cost_act (None ?)) st1 st2
129| vm_cjump_true :
130           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
131           eval_asm_cond p p' cond (asm_store … st1) = return true→
132           fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) →
133           asm_is_io … st1 = false →
134           asm_store … st1 = asm_store … st2 →
135           asm_stack … st1 = asm_stack … st2 →
136           asm_is_io … st1 = asm_is_io … st2 →
137           pc … st2 = new_pc →
138           op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 →
139           vmstep … (cost_act (Some ? ltrue)) st1 st2
140| vm_cjump_false :
141           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
142           eval_asm_cond p p' cond (asm_store … st1) = return false→
143           fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) →
144           asm_is_io … st1 = false →
145           asm_store … st1 = asm_store … st2 →
146           asm_stack … st1 = asm_stack … st2 →
147           asm_is_io … st1 = asm_is_io … st2 →
148           S (pc … st1) = pc … st2 →
149           op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 →
150           vmstep … (cost_act (Some ? lfalse)) st1 st2
151| vm_io_in : 
152           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
153           fetch … prog (pc … st1) = return (Iio p lin io lout) →
154           asm_is_io … st1 = false →
155           asm_store … st1 = asm_store … st2 →
156           asm_stack … st1 = asm_stack … st2 →
157           true = asm_is_io … st2 →
158           pc … st1 = pc … st2 →
159           cost … st1 = cost … st2 →
160           vmstep … (cost_act (Some ? lin)) st1 st2
161| vm_io_out :
162           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
163           fetch … prog (pc … st1) = return (Iio p lin io lout) →
164           asm_is_io … st1 = true →
165           eval_asm_io … io (asm_store … st1) = return asm_store … st2 →
166           asm_stack … st1 = asm_stack … st2 →
167           false = asm_is_io … st2 →
168           S (pc … st1) = pc … st2 →
169           op … (cost … st1) (cost_of_io p p' io (asm_store … st1)) = cost … st2 →
170           vmstep … (cost_act (Some ? lout)) st1 st2
171| vm_call :
172           ∀st1,st2 : vm_state p p'.∀f,lbl.
173           fetch … prog (pc … st1) = return (Icall p f) →
174           asm_is_io … st1 = false →
175           asm_store … st1 = asm_store … st2 →
176           S (pc … st1) ::  asm_stack … st1 = asm_stack … st2 →
177           asm_is_io … st1 = asm_is_io … st2 →
178           entry_of_function … prog f = pc … st2 →
179           op … (cost … st1) (cost_of p p' (Icall p f) (asm_store … st1)) = cost … st2 →
180           label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f) = return lbl →
181           vmstep … (call_act f lbl) st1 st2
182| vm_ret :
183          ∀st1,st2 : vm_state p p'.∀newpc,lbl.
184           fetch … prog (pc … st1) = return (Iret p) →
185           asm_is_io … st1 = false →
186           asm_store … st1 = asm_store … st2 →
187           asm_stack … st1 = newpc ::  asm_stack … st2  →
188           asm_is_io … st1 = asm_is_io … st2 →
189           newpc = pc … st2 →
190           label_of_pc ? (return_label_fun … prog) newpc = return lbl →
191           op … (cost … st1) (cost_of p p' (Iret p) (asm_store … st1)) = cost … st2 →
192           vmstep … (ret_act (Some ? lbl)) st1 st2.
193
194definition eval_vmstate : ∀p : assembler_params.∀p' : sem_params p.
195AssemblerProgram p → vm_state p p' → option (ActionLabel × (vm_state p p')) ≝
196λp,p',prog,st.
197! i ← fetch … prog (pc … st);
198match i with
199[ Seq x opt_l ⇒
200   if asm_is_io … st then
201     None ?
202   else
203     ! new_store ← eval_asm_seq p p' x (asm_store … st);
204     return 〈cost_act opt_l,
205             mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false
206                (op … (cost … st) (cost_of p p' (Seq p x opt_l) (asm_store … st)))〉
207| Ijmp newpc ⇒
208   if asm_is_io … st then
209     None ?
210   else
211     return 〈cost_act (None ?),
212             mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
213                (op … (cost … st) (cost_of p p' (Ijmp … newpc) (asm_store … st)))〉
214| CJump cond newpc ltrue lfalse ⇒
215   if asm_is_io … st then
216     None ?
217   else
218     ! b ← eval_asm_cond p p' cond (asm_store … st);
219     if b then
220       return 〈cost_act (Some ? ltrue),
221               mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
222                (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉
223     else
224       return 〈cost_act (Some ? lfalse),
225               mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false
226                (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉
227| Iio lin io lout ⇒
228              if asm_is_io … st then
229                 ! new_store ← eval_asm_io … io (asm_store … st);
230                 return 〈cost_act (Some ? lout),
231                         mk_vm_state ?? (S (pc … st)) (asm_stack … st)
232                         new_store false
233                         (op … (cost … st)
234                               (cost_of_io p p' io (asm_store … st)))〉   
235              else
236                return 〈cost_act (Some ? lin),
237                        mk_vm_state ?? (pc … st) (asm_stack … st) (asm_store … st)
238                                    true (cost … st)〉
239| Icall f ⇒
240    if asm_is_io … st then
241      None ?
242    else
243      ! lbl ← label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f);
244      return 〈call_act f lbl,
245              mk_vm_state ?? (entry_of_function … prog f)
246                             ((S (pc … st)) :: (asm_stack … st))
247                             (asm_store … st) false
248                             (op … (cost … st) (cost_of p p' (Icall p f) (asm_store … st)))〉
249| Iret ⇒ if asm_is_io … st then
250            None ?
251         else
252            ! 〈newpc,tl〉 ← option_pop … (asm_stack … st);
253            ! lbl ← label_of_pc ? (return_label_fun … prog) newpc;
254            return 〈ret_act (Some ? lbl),
255                    mk_vm_state ?? newpc tl (asm_store … st) false   
256                     (op … (cost … st) (cost_of p p' (Iret p) (asm_store … st)))〉
257].
258
259lemma eval_vmstate_to_Prop : ∀p,p',prog,st1,st2,l.
260eval_vmstate p p' prog st1 = return 〈l,st2〉 → vmstep … prog l st1 st2.
261#p #p' #prog #st1 #st2 #l whd in match eval_vmstate; normalize nodelta
262#H cases(bind_inversion ????? H) -H * normalize nodelta
263[ #seq #opt_l * #EQfetch inversion(asm_is_io ???) normalize nodelta
264  [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H)
265  #newstore * #EQnewstore whd in ⊢ (??%% → ?); #EQ destruct
266  @vm_seq //
267| #newpc * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
268  [ whd in ⊢ (??%% → ?); #EQ destruct] whd in ⊢ (??%% → ?); #EQ destruct
269  @vm_ijump //
270| #cond #new_pc #ltrue #lfase * #EQfetch inversion(asm_is_io ???) normalize nodelta
271  [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H) -H
272  * normalize nodelta * #EQcond whd in ⊢ (??%% → ?); #EQ destruct
273  [ @(vm_cjump_true … EQfetch) // | @(vm_cjump_false … EQfetch) //]
274| #lin #io #lout * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
275  [ #H cases(bind_inversion ????? H) -H #newstore * #EQnewstore ]
276  whd in ⊢ (??%% → ?); #EQ destruct
277  [ @(vm_io_out … EQfetch) // | @(vm_io_in … EQfetch) // ]
278| #f * #EQfetch inversion(asm_is_io ???) #EQio normalize nodelta
279  [ whd in ⊢ (??%% → ?); #EQ destruct ] #H cases (bind_inversion ????? H) -H
280  #lbl * #EQlb whd in ⊢ (??%% → ?); #EQ destruct @(vm_call … EQfetch) //
281| * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
282  [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H
283  * #newpc #tl * whd in match option_pop; normalize nodelta inversion(asm_stack ???)
284  normalize nodelta [#_ whd in ⊢ (??%% → ?); #EQ destruct] #newpc1 #tl1 #_
285  #EQstack whd in ⊢ (??%% → ?); #EQ destruct #H cases(bind_inversion ????? H) #lbl
286  * #EQlbl whd in ⊢ (??%% → ?); #EQ destruct @vm_ret //
287]
288qed.
289
290 
291lemma vm_step_to_eval : ∀p,p',prog,st1,st2,l.vmstep … prog l st1 st2 →
292eval_vmstate p p' prog st1 = return 〈l,st2〉.
293#p #p' #prog * #pc1 #stack1 #store1 #io1 #cost1
294* #pc2 #stack2 #store2 #io2 #cost2 #l #H inversion H
295[ #s1 #s2 #i #opt_l #EQfetch #EQio #EQstore #EQstack #EQio1 #EQpc #EQcost
296  #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta   
297  >EQfetch >m_return_bind normalize nodelta >EQio normalize nodelta >EQstore
298  >m_return_bind <EQio1 >EQio <EQpc >EQstack >EQcost %
299| #s1 #s2 #newpc #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc #EQcost
300  #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta
301  >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta <EQio2 >EQio1
302  >EQstore >EQstack <EQcost >EQstore %
303|3,4: #s1 #s2 #cond #newoc #ltrue #lfalse #EQev_cond #EQfetch #EQio1 #EQstore
304  #EQstack #EQio2 #EQnewoc #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct
305  whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind
306  normalize nodelta >EQio1 normalize nodelta >EQev_cond >m_return_bind
307  normalize nodelta <EQio1 >EQio2 >EQstore >EQstack <EQcost >EQstore [%] >EQnewoc %
308|5,6: #s1 #s2 #lin #io #lout #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQpc
309   #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
310   normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1
311   normalize nodelta >EQstack <EQpc >EQcost [ >EQstore <EQio2 %]
312   >EQstore >m_return_bind <EQpc <EQio2 %
313| #s1 #s2 #f #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQentry
314  #EQcost #EQlab_pc #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
315  normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1
316  normalize nodelta >EQlab_pc >m_return_bind >EQentry >EQcost <EQio2 >EQio1
317  <EQstack >EQstore %
318| #s1 #s2 #newpc #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc
319  #EQlab_pc #EQcosts #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
320  normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta
321  >EQstack whd in match option_pop; normalize nodelta >m_return_bind
322  >EQlab_pc >m_return_bind >EQcosts >EQstore  <EQio2 >EQio1 %
323]
324qed.
325
326coercion vm_step_to_eval.
327
328include "../src/utilities/hide.ma".
329
330discriminator option.
331
332inductive vm_ass_state  (p : assembler_params) (p' : sem_params p) : Type[0] ≝
333| INITIAL : vm_ass_state p p'
334| FINAL : vm_ass_state p p'
335| STATE : vm_state p p' → vm_ass_state p p'.
336
337definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p →  abstract_status ≝
338λp,p',prog.let init_act ≝ cost_act (Some ? (in_act … prog)) in
339           let end_act ≝ cost_act (Some ? (in_act … prog)) in
340    mk_abstract_status
341                (vm_ass_state p p')
342                (λl.λs1,s2 : vm_ass_state p p'.
343                    match s1 with
344                    [ STATE st1 ⇒
345                        match s2 with
346                        [ STATE st2 ⇒ 
347                            (eqb (pc ?? st1) (endmain … prog)) = false ∧ vmstep p p' prog l st1 st2
348                        | INITIAL ⇒ False
349                        | FINAL ⇒ eqb (pc … st1) (endmain … prog) = true ∧ l = end_act
350                        ]
351                    | INITIAL ⇒ match s2 with
352                                [ STATE st2 ⇒ eqb (pc … st2) O = true ∧ l = init_act
353                                | _ ⇒ False
354                                ]
355                    | FINAL ⇒ False
356                    ])
357                (λ_.λ_.True)
358                (λst.match st with
359                    [ INITIAL ⇒ cl_other | FINAL ⇒ cl_other |
360                     STATE s ⇒
361                      match fetch … prog (pc … s) with
362                      [ Some i ⇒ match i with
363                               [ Seq _ _ ⇒ cl_other
364                               | Ijmp _ ⇒ cl_other
365                               | CJump _ _ _ _ ⇒ cl_jump
366                               | Iio _ _ _ ⇒ if asm_is_io … s then cl_io else cl_other
367                               | Icall _ ⇒ cl_other
368                               | Iret ⇒ cl_other
369                               ]
370                     | None ⇒ cl_other
371                     ]
372                    ]
373                )
374                (λ_.true)
375                (λs.match s with [ INITIAL ⇒ true | _ ⇒ false])
376                (λs.match s with [ FINAL ⇒ true | _ ⇒ false])
377                ???.
378@hide_prf
379[ #s1 #s2 #l
380 cases s1 normalize nodelta [1,2: #abs destruct] -s1 #s1
381 cases s2 normalize nodelta [1: #_ * |2: #_ * #_ #EQ >EQ normalize /2/ ] #s2 
382 inversion(fetch ???) normalize nodelta
383  [ #_ #EQ destruct] * normalize nodelta
384  [ #seq #lbl #_
385  | #n #_
386  | #cond #newpc #ltrue #lfalse #EQfetch
387  | #lin #io #lout #_ cases (asm_is_io ??) normalize nodelta
388  | #f #_
389  | #_
390  ]
391  #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate;
392  normalize nodelta >EQfetch >m_return_bind normalize nodelta cases(asm_is_io ??)
393  normalize nodelta [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H
394  * * #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct % //
395| #s1 #s2 #l
396  cases s1 normalize nodelta [2: #_ * |3: #s1 ]
397  cases s2 normalize nodelta [1,2,4,5: #abs destruct ] #s2 [2: #_ * #_ /2/ ]
398  inversion(fetch ???) normalize nodelta
399  [ #_ #EQ destruct] * normalize nodelta
400  [ #seq #lbl #_
401  | #n #_
402  | #cond #newpc #ltrue #lfalse #_
403  | #lin #io #lout #EQfetch inversion (asm_is_io ??) #EQio normalize nodelta
404  | #f #_
405  | #_
406  ]
407  #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate;
408  normalize nodelta #H cases(bind_inversion ????? H) -H *
409  [ #seq1 #lbl1
410  | #n1
411  | #cond1 #newpc1 #ltrue1 #lfalse1
412  | #lin1 #io1 #lout1
413  | #f
414  |
415  ]
416  normalize nodelta * #_ cases(asm_is_io ??) normalize nodelta
417  [1,3,5,9,11: whd in ⊢ (??%% → ?); #EQ destruct
418  |2,6,7,10,12: #H cases(bind_inversion ????? H) -H #x * #_
419    [2: cases x normalize nodelta
420    |5: #H cases(bind_inversion ????? H) -H #y * #_
421    ]
422  ]
423  whd in ⊢ (??%% → ?); #EQ destruct destruct % //
424| #s1 #s2 #l
425  cases s1 normalize nodelta [1,2: #abs destruct ] #s1
426  cases s2 normalize nodelta [ #_ * | #_ * /2/ ] #s2
427  inversion(fetch ???) normalize nodelta
428  [ #_ #EQ destruct] * normalize nodelta
429  [ #seq #lbl #_
430  | #n #_
431  | #cond #newpc #ltrue #lfalse #_
432  | #lin #io #lout #EQfetch inversion(asm_is_io ??) normalize nodelta #EQio
433  | #f #_
434  | #_
435  ]
436  #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate;
437  normalize nodelta  >EQfetch >m_return_bind normalize nodelta >EQio
438  normalize nodelta #H cases(bind_inversion ????? H) -H #x * #_
439  whd in ⊢ (??%% → ?); #EQ destruct % //
440qed.
441
442definition asm_concrete_trans_sys ≝
443λp,p',prog.mk_concrete_transition_sys …
444             (asm_operational_semantics p p' prog) (m … p')
445             (λs.match s with [STATE st ⇒ cost … st | _ ⇒ e …] ).
446
447definition emits_labels ≝
448λp.λinstr : AssemblerInstr p.match instr with
449        [ Seq _ opt_l ⇒ match opt_l with
450                        [ None ⇒ Some ? (λpc.S pc)
451                        | Some _ ⇒ None ?
452                        ]
453        | Ijmp newpc ⇒ Some ? (λ_.newpc)
454        | _ ⇒ None ?
455        ].
456
457definition fetch_state : ∀p,p'.AssemblerProgram p → vm_state p p' → option (AssemblerInstr p) ≝
458λp,p',prog,st.fetch … prog (pc … st).
459
460definition asm_static_analisys_data ≝ λp,p',prog,abs_t,instr_m.
461mk_static_analysis_data (asm_concrete_trans_sys p p' prog) abs_t
462 … (λs.match s with [ STATE st ⇒ fetch_state p p' prog st | _ ⇒ None ? ]) instr_m.
463
464definition non_empty_list : ∀A.list A → bool ≝
465λA,l.match l with [ nil ⇒ false | _ ⇒  true ].
466
467let rec block_cost (p : assembler_params)
468 (prog: AssemblerProgram p) (abs_t : monoid)
469 (instr_m : AssemblerInstr p → abs_t)
470 (prog_c: option ℕ)
471    (program_size: ℕ)
472        on program_size: option abs_t ≝
473match prog_c with
474[ None ⇒ return e … abs_t
475| Some program_counter ⇒
476  match program_size with
477    [ O ⇒ None ?
478    | S program_size' ⇒
479       if eqb program_counter (endmain … prog) then
480        return e … abs_t
481      else
482      ! instr ← fetch … prog program_counter;
483      ! n ← (match emits_labels … instr with
484            [ Some f ⇒ block_cost … prog abs_t instr_m (Some ? (f program_counter)) program_size'
485            | None ⇒ return e …
486            ]);
487      return (op … abs_t (instr_m … instr) n)
488    ]
489].
490
491
492record cost_map_T (dom : DeqSet) (codom : Type[0]) : Type[1] ≝
493{ map_type :> Type[0]
494; empty_map : map_type
495; get_map : map_type → dom → option codom
496; set_map : map_type → dom → codom → map_type
497; get_set_hit : ∀k,v,m.get_map (set_map m k v) k = return v
498; get_set_miss : ∀k1,k2,v,m.(k1 == k2) = false → get_map (set_map m k1 v) k2 = get_map m k2
499}.
500
501
502
503lemma labels_pc_ok : ∀p,prog,l1,l2,i_act,i,lbl,pc,m.
504nth_opt ? pc prog = return i →
505mem ? lbl (labels_pc_of_instr … i (m+pc)) →
506mem ? lbl (labels_pc p prog l1 l2 i_act m).
507#p #instrs #l1 #l2 #iact #i #lbl #pc
508whd in match fetch; normalize nodelta lapply pc -pc
509elim instrs
510[ #pc #m whd in ⊢ (??%% → ?); #EQ destruct]
511#x #xs #IH * [|#pc'] #m  whd in ⊢ (??%% → ?);
512[ #EQ destruct #lbl_addr whd in match (labels_pc ???);
513  /2 by mem_append_l1/
514| #EQ #H2 whd in match (labels_pc ???); @mem_append_l2 @(IH … EQ) //
515]
516qed.
517
518lemma labels_pc_return: ∀p,prog,l1,l2,iact,x1,x2.
519 label_of_pc ReturnPostCostLabel l2 x1=return x2 →
520 ∀m.
521   mem … 〈(a_return_post x2),x1〉 (labels_pc p prog l1 l2 iact m).
522 #p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l
523[ #m @mem_append_l2 @mem_append_l2 whd in H:(??%?);
524  elim l2 in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
525  * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim
526  normalize nodelta
527  [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/
528  | #NEQ #H2 %2 @IH // ]
529| #hd #tl #IH #m @mem_append_l2 @IH ]
530qed.
531
532lemma labels_pc_call: ∀p,prog,l1,l2,iact,x1,x2.
533 label_of_pc CallCostLabel l1 x1=return x2 →
534 ∀m.
535   mem … 〈(a_call x2),x1〉 (labels_pc p prog l1 l2 iact m).
536 #p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l
537[ #m @mem_append_l2 @mem_append_l1 whd in H:(??%?);
538  elim l1 in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
539  * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim
540  normalize nodelta
541  [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/
542  | #NEQ #H2 %2 @IH // ]
543| #hd #tl #IH #m @mem_append_l2 @IH ]
544qed.
545
546(*
547lemma labels_pc_bounded : ∀p.∀prog : AssemblerProgram p.∀lbl,pc.∀m.
548mem ? 〈lbl,pc〉 (labels_pc p (instructions … prog) m) →
549(m + pc) < (|(instructions … prog)|).
550#p * #instr #endmain #_  #H1 #H2 elim instr
551[ #H3 @⊥ /2/ ] #x #xs #IH #_ #lbl #pc #m whd in match (labels_pc ???);
552#H cases(mem_append ???? H) -H
553[ whd in match labels_pc_of_instr; normalize nodelta
554  cases x normalize nodelta
555  [ #seq * [|#lab]
556  | #newpc
557  | #cond #newpc #ltrue #lfalse
558  | #lin #io #lout
559  | #f
560  |
561  ]
562  normalize [1,3,6,7: *] * [2,4,6: * [2,4:*] ]
563  #EQ destruct
564*) 
565
566let rec m_foldr (M : Monad) (X,Y : Type[0]) (f : X→Y→M Y) (l : list X) (y : Y) on l : M Y ≝
567match l with
568[ nil ⇒ return y
569| cons x xs ⇒ ! z ← m_foldr M X Y f xs y; f x z
570].
571
572definition static_analisys : ∀p : assembler_params.∀abs_t : monoid.(AssemblerInstr p → abs_t) →
573∀mT : cost_map_T DEQCostLabel abs_t.AssemblerProgram p → option mT ≝
574λp,abs_t,instr_m,mT,prog.
575let prog_size ≝ S (|instructions … prog|) in
576m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m (Some ? w) prog_size; 
577                               return set_map … m z k) (labels_pc … (instructions … prog)
578                                         (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)
579      (empty_map ?? mT).
580     
581
582(*falso: necessita di no_duplicates*)
583
584definition eq_deq_prod : ∀D1,D2 : DeqSet.D1 × D2 → D1 × D2 → bool ≝
585λD1,D2,x,y.\fst x == \fst y ∧ \snd x == \snd y.
586
587definition DeqProd ≝ λD1 : DeqSet.λD2 : DeqSet.
588mk_DeqSet (D1 × D2) (eq_deq_prod D1 D2) ?.
589@hide_prf
590* #x1 #x2 * #y1 #y2 whd in match eq_deq_prod; normalize nodelta
591% [2: #EQ destruct @andb_Prop >(\b (refl …)) %]
592inversion (? ==?) #EQ1 whd in match (andb ??); #EQ2 destruct
593>(\P EQ1) >(\P EQ2) %
594qed.
595(*
596unification hint  0 ≔ D1,D2 ;
597    X ≟ DeqProd D1 D2
598(* ---------------------------------------- *) ⊢
599    D1 × D2 ≡ carr X.
600
601
602unification hint  0 ≔ D1,D2,p1,p2;
603    X ≟ DeqProd D1 D2
604(* ---------------------------------------- *) ⊢
605    eq_deq_prod D1 D2 p1 p2 ≡ eqb X p1 p2.
606   
607definition deq_prod_to_prod : ∀D1,D2 : DeqSet.DeqProd D1 D2 → D1 × D2 ≝
608λD1,D2,x.x.
609
610coercion deq_prod_to_prod.
611*)
612
613lemma map_mem : ∀A,B,f,l,a.mem A a l → ∃b : B.mem B b (map A B f l)
614∧ b = f a.
615#A #B #f #l elim l [ #a *] #x #xs #IH #a *
616[ #EQ destruct %{(f x)} % // % // | #H cases(IH … H)
617  #b * #H1 #EQ destruct %{(f a)} % // %2 //
618]
619qed.
620
621lemma static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map.
622static_analisys p abs_t instr_m mT prog = return map →
623mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) (call_label_fun … prog)
624                   (return_label_fun … prog) (in_act … prog) O) →
625get_map … map lbl =
626block_cost … prog abs_t instr_m (Some ? pc) (S (|(instructions … prog)|)) ∧
627block_cost … prog abs_t instr_m (Some ? pc) (S (|(instructions … prog)|)) ≠ None ?.
628#p #abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta
629#endmain #Hendmain #entry_fun #call_label_fun #return_label_fun #inact
630#nodup generalize in match nodup in ⊢ (∀_.∀_.∀_. (??(????%??)?) → %); #Hnodup lapply nodup -nodup
631lapply (labels_pc ??????) #l elim l [ #x #y #z #w #h * ]
632* #hd1 #hd2 #tl #IH * #H1 #H2 #lbl #pc #map #H
633cases(bind_inversion ????? H) -H #map1 * #EQmap1 normalize nodelta #H
634cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); #EQ
635destruct *
636[ #EQ destruct % [ >get_set_hit >EQelem % | >EQelem % whd in ⊢ (??%% → ?); #EQ destruct]
637| #H %
638  [ >get_set_miss [ @(proj1 … (IH …)) //] inversion (? == ?) [2: #_ %]
639    #ABS cases H1 -H1 #H1 @⊥ @H1 >(\P ABS) >mem_to_memb //
640    cases(map_mem … \fst … H) #z1 * #Hz1 #EQ destruct @Hz1
641  | @(proj2 … (IH …)) //
642  ]
643]
644qed.
645
646include "Simulation.ma".
647
648definition terminated_trace : ∀S : abstract_status.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝
649λS,s1,s3,t.bool_to_Prop (as_final … s3) ∨
650       ∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind ? s2 s3 s3 l prf … (t_base … s3))
651∧ ((is_costlabelled_act l ∨ is_labelled_ret_act l) ∧
652   (is_call_act l → bool_to_Prop (is_call_post_label … s2))).
653
654definition big_op: ∀M: monoid. list M → M ≝
655 λM. foldl … (op … M) (e … M).
656
657lemma big_op_associative:
658 ∀M:monoid. ∀l1,l2.
659  big_op M (l1@l2) = op M (big_op … l1) (big_op … l2).
660 #M #l1 whd in match big_op; normalize nodelta
661 generalize in match (e M) in ⊢ (? → (??%(??%?))); elim l1
662 [ #c #l2 whd in match (append ???); normalize lapply(neutral_r … c)
663   generalize in match c in ⊢ (??%? → ???%); lapply c -c lapply(e M)
664   elim l2 normalize
665   [ #c #c1 #c2 #EQ @sym_eq //
666   | #x #xs #IH #c1 #c2 #c3 #EQ <EQ <IH [% | <is_associative % |]
667   ]
668 | #x #xs #IH #c #l2 @IH
669 ]
670qed.
671
672lemma act_big_op : ∀M,B. ∀act : monoid_action M B.
673 ∀l1,l2,x.
674   act (big_op M (l1@l2)) x = act (big_op … l2) (act (big_op … l1) x).
675 #M #B #act #l1 elim l1
676 [ #l2 #x >act_neutral //
677 | #hd #tl #IH #l2 #x change with ([?]@(tl@l2)) in match ([?]@(tl@l2));
678   >big_op_associative >act_op >IH change with ([hd]@tl) in match ([hd]@tl);
679   >big_op_associative >act_op in ⊢ (???%); %
680 ]
681qed.
682
683lemma monotonicity_of_block_cost : ∀p,prog,abs_t,instr_m,pc,size,k.
684block_cost p prog abs_t instr_m (Some ? pc) size = return k →
685∀size'.size ≤ size' →
686block_cost p prog abs_t instr_m (Some ? pc) size' = return k.
687#p #prog #abs_t #instr_m #pc #size lapply pc elim size
688[ #pc #k whd in ⊢ (??%% → ?); #EQ destruct]
689#n #IH #pc #k whd in ⊢ (??%% → ?); @eqb_elim
690[ #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct
691  #size' * [2: #m #_] whd in ⊢ (??%%); @eqb_elim try( #_ %) * #H @⊥ @H %
692| #Hpc normalize nodelta #H cases(bind_inversion ????? H) -H #i
693  * #EQi #H cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?);
694  #EQ destruct #size' *
695  [ whd in ⊢ (??%?); @eqb_elim
696    [ #EQ @⊥ @(absurd ?? Hpc) assumption ]
697    #_ normalize nodelta >EQi >m_return_bind >EQelem %
698  | #m #Hm whd in ⊢ (??%?); @eqb_elim
699    [ #EQ @⊥ @(absurd ?? Hpc) assumption ]
700    #_ normalize nodelta >EQi >m_return_bind
701    cases (emits_labels ??) in EQelem; normalize nodelta
702    [ whd in ⊢ (??%%→ ??%%); #EQ destruct %]
703    #f #EQelem >(IH … EQelem) [2: /2/ ] %
704  ]
705]
706qed.
707
708lemma step_emit : ∀p,p',prog,st1,st2,l,i.
709fetch p prog (pc … st1) = return i →
710eval_vmstate p p' … prog st1 = return 〈l,st2〉 → 
711emits_labels … i = None ? → ∃x.
712match l in ActionLabel return λ_:ActionLabel.(list CostLabel) with 
713[call_act f c ⇒ [a_call c]
714|ret_act x ⇒
715   match x with [None⇒[]|Some c⇒[a_return_post c]]
716|cost_act x ⇒
717   match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
718] = [x] ∧
719 (mem … 〈x,pc … st2〉 (labels_pc p (instructions … prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)).
720#p #p' #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta
721>EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta
722[ #seq * [|#lab]
723| #newpc
724| #cond #newpc #ltrue #lfalse
725| #lin #io #lout
726| #f
727|
728]
729#EQi cases(asm_is_io ???) normalize nodelta
730[1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
731|2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1
732  [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta
733  |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2
734  ]
735]
736whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels;
737normalize nodelta #EQ destruct % [2,4,6,8,10,12,14: % try % |*:]
738[1,2,4,5,7: @(labels_pc_ok … EQi) normalize /3 by or_introl,or_intror/ ]
739/2 by labels_pc_return, labels_pc_call/
740qed.
741
742lemma step_non_emit : ∀p,p',prog,st1,st2,l,i,f.
743fetch p prog (pc … st1) = return i →
744eval_vmstate p p' … prog st1 = return 〈l,st2〉 → 
745emits_labels … i = Some ? f →
746match l in ActionLabel return λ_:ActionLabel.(list CostLabel) with 
747[call_act f c ⇒ [a_call c]
748|ret_act x ⇒
749   match x with [None⇒[]|Some c⇒[a_return_post c]]
750|cost_act x ⇒
751   match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
752] = [ ] ∧ pc … st2 = f (pc … st1).
753#p #p' #prog #st1 #st2 #l #i #f #EQi whd in match eval_vmstate; normalize nodelta
754>EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta
755[ #seq * [|#lab]
756| #newpc
757| #cond #newpc #ltrue #lfalse
758| #lin #io #lout
759| #f
760|
761]
762#EQi cases(asm_is_io ???) normalize nodelta
763[1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
764|2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1
765  [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta
766  |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2
767  ]
768]
769whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels;
770normalize nodelta #EQ destruct /2 by refl, conj/
771qed.
772
773lemma labels_of_trace_are_in_code :
774∀p,p',prog.∀st1,st2 :  vm_ass_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
775∀lbl.
776mem … lbl (get_costlabels_of_trace … t) →
777mem … (lbl) (map ?? \fst … (labels_pc … (instructions p prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)).
778cases daemon (*
779#p #p' #prog #st1 #st2 #t elim t
780[ #st #lbl *
781| #st1 #st2 #st3 #l * #H1 #H2 #tl #IH #lbl whd in match (get_costlabels_of_trace ????);
782  #H cases(mem_append ???? H) -H [2: #H @IH //]
783  lapply(vm_step_to_eval … H2) whd in match eval_vmstate;
784  normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi #_
785  inversion(emits_labels … i)
786  [ #EQemit cases(step_emit … (vm_step_to_eval … H2)) // #x * #EQ1 #EQ2 >EQ1 *
787    [2: *] #EQ destruct cases(map_mem … \fst … EQ2) #y * #H3 #EQ destruct //
788  | #f #EQemit >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H2) … EQemit))
789    *
790  ]
791]  *)
792qed.
793
794let rec dependent_map (A,B : Type[0]) (l : list A) (f : ∀a : A.mem … a l → B) on l : list B ≝
795(match l return λx.l=x → ? with
796[ nil ⇒ λ_.nil ?
797| cons x xs ⇒ λprf.(f x ?) :: dependent_map A B xs (λx,prf1.f x ?)
798])(refl …).
799[ >prf %% | >prf %2 assumption]
800qed.
801
802lemma dependent_map_append : ∀A,B,l1,l2,f.
803dependent_map A B (l1 @ l2) (λa,prf.f a prf) =
804(dependent_map A B l1 (λa,prf.f a ?)) @ (dependent_map A B l2 (λa,prf.f a ?)).
805[2: @hide_prf /2/ | 3: @hide_prf /2/]
806#A #B #l1 elim l1 normalize /2/
807qed.
808
809lemma rewrite_in_dependent_map : ∀A,B,l1,l2,f.
810        ∀EQ:l1 = l2.
811         dependent_map A B l1 (λa,prf.f a prf) =
812         dependent_map A B l2 (λa,prf.f a ?).
813[2: >EQ // | #A #B #l1 #l2 #f #EQ >EQ in f; #f % ]
814qed.
815
816definition get_pc : ∀p,p'.vm_ass_state p p' → ℕ → option ℕ ≝
817λp,p',st,endmain.match st with
818[ STATE s ⇒ Some ? (pc … s)
819| INITIAL ⇒ None ?
820| FINAL ⇒ Some ? endmain
821].
822
823
824lemma static_dynamic : ∀p,p',prog.
825∀abs_t : abstract_transition_sys (m … p').∀instr_m.
826∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1.
827∀EQmap : static_analisys p ? instr_m mT prog = return map1.
828∀st1,st2 : vm_ass_state p p'.
829∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
830terminated_trace … t →
831∀k.
832pre_measurable_trace … t →
833block_cost p prog … instr_m (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k →
834∀a1.rel_galois … good st1 a1 →
835∀labels.
836labels = dependent_map CostLabel ? (get_costlabels_of_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
837rel_galois … good st2 (act_abs … abs_t (big_op … labels) (act_abs … abs_t k a1)).
838[2: @hide_prf
839    cases(mem_map ????? (labels_of_trace_are_in_code … prf)) *
840    #lbl' #pc * #Hmem #EQ destruct   
841    >(proj1 … (static_analisys_ok … EQmap … Hmem))
842    @(proj2 … (static_analisys_ok … EQmap … Hmem))
843]
844#p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #t elim t
845[ #st * [| * #st3 * #t1 * #l * #prf * #ABS @⊥ cases t1 in ABS; ]
846  #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta
847  [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st
848    normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
849    #a1 #rel_st_a1 whd in match (map ????); #costs #EQ >EQ >act_neutral >act_neutral assumption
850  | ** #H1 #H2 * #H3 #H4 whd in ⊢ (??%% → ?); >H3 normalize nodelta
851    #H cases(bind_inversion ????? H) -H *
852    [ #seq * [|#lbl1]
853    | #newpc
854    | #cond #newpc #ltrue #lfalse
855    | #lin #io #lout
856    | #f
857    |
858    ]
859    * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate;
860    normalize nodelta >EQfetch >m_return_bind normalize nodelta
861    cases(asm_is_io ??) normalize nodelta
862    [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
863    |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_
864      [3: cases x normalize nodelta
865      |6: #H cases(bind_inversion ????? H) -H #y * #_
866      ]
867    ]
868    whd in ⊢ (??%% → ?); #EQ destruct
869    [4,8: cases H1 [1,3: * |*: * #y #EQ destruct]]
870    >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
871    #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ >EQ >neutral_r
872    >act_neutral
873    @(instr_map_ok … good … EQfetch … good_st_a1) /2/
874  ]
875| -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H
876  #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????);
877  whd #costs >dependent_map_append
878  (*change with (list_cost_to_list_initcost ?) in match (list_cost_to_list_initcost ?);*) 
879  #EQ destruct whd in H2 : (??%?); lapply H2 >H3 in ⊢ (% → ?); -H2
880  normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi
881  inversion(emits_labels ??)
882  [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct  >big_op_associative >act_op @IH
883  | #f #EQemits normalize nodelta #H
884    cases(bind_inversion ????? H) -H #k' * #EQk' whd in ⊢ (??%% → ?);
885    #EQ destruct(EQ) >act_op whd in match (append ???); @IH
886  ]
887  [1,5: inversion H in ⊢ ?;
888    [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct
889    |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_
890      #EQ1 #EQ2 #EQ3 #EQ4 destruct
891    |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_
892      #EQ1 #EQ2 #EQ3 #EQ4 destruct
893    |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct
894      * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
895    |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
896    ] //
897  | cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx
898    >(rewrite_in_dependent_map … EQx)
899 
900    whd in match (dependent_map ????); whd in match (dependent_map ????); whd in match (big_op ??);
901    >neutral_l @opt_safe_elim #elem #EQget
902    cases (static_analisys_ok  … x … (pc … st2) … no_dup … EQmap) //
903    #EQ #_ <EQ assumption
904  | >neutral_r  @(instr_map_ok … good … EQi … good_a1) /2/
905  | %
906  | >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
907    >(monotonicity_of_block_cost … EQk') //
908  | @(instr_map_ok … good … EQi … good_a1) /2/
909  | lapply (proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
910    #EQ >(rewrite_in_dependent_map … EQ) %
911  ]
912]
913qed.
914
915definition actionlabel_to_costlabel : ActionLabel → list CostLabel ≝
916λa.match a with
917[ call_act f l ⇒ [a_call l]
918| ret_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_return_post l]]
919| cost_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_non_functional_label l]]
920].
921
922definition get_costlabels_of_measurable_trace : ∀S : abstract_status.measurable_trace S → list CostLabel ≝
923λS,t.
924 match L_label … t with
925 [ None ⇒ [i_act]
926 | Some l ⇒ actionlabel_to_costlabel l
927 ] @
928 get_costlabels_of_trace … (trace … t).
929
930lemma i_act_in_map :  ∀p,prog.
931mem … 〈i_act,O〉 (labels_pc … (instructions p prog) O).
932#p *#instr #n #_ generalize in match O in ⊢ (???%); elim instr
933[ normalize /2/] #i #xs #IH #m whd in match (labels_pc ???);
934@mem_append_l2 @IH
935qed.
936
937
938lemma as_execute_labelled_ok : ∀p,p',prog,c,l,st1,st2.
939eval_vmstate p p' prog st1 = return 〈l,st2〉 → actionlabel_to_costlabel l = [c] →
940∃n.
941mem … 〈c,n〉 (labels_pc … (instructions p prog) O).
942#p #p' * #instr #endmain #Hendmain #c #l #st1 #st2 #H2 lapply H2 whd in match eval_vmstate; normalize nodelta
943#H cases(bind_inversion ????? H) -H #i * #EQfetch #_
944 inversion(emits_labels … i)
945 [ #EQemit cases(step_emit … H2) // #x * #EQ1 #EQ2 whd in match actionlabel_to_costlabel;
946   normalize nodelta >EQ1 #EQ destruct /2 by ex_intro/
947  | #f #EQemit whd in match actionlabel_to_costlabel; normalize nodelta  >(proj1 … (step_non_emit … EQfetch H2 … EQemit))
948    #EQ destruct
949 ]
950qed.
951 
952
953(*get_costlabels_of_measurable_trace deve aggiungere la label iniziale.*)
954theorem static_dynamic_meas : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog.
955∀abs_t : abstract_transition_sys (m … p').∀instr_m.
956∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1.
957∀EQmap : static_analisys p ? instr_m mT prog = return map1.
958∀t : measurable_trace (asm_operational_semantics p p' prog).
959let start_state ≝ match L_pre_state … t with [None ⇒ L_s1 … t | Some x ⇒ x ] in
960∀a1.rel_galois … good start_state a1 →
961∀abs_trace.
962abs_trace = dependent_map CostLabel ? (get_costlabels_of_measurable_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
963rel_galois … good (R_s2 … t) (act_abs … abs_t (big_op … abs_trace) a1).
964[2: @hide_prf
965    whd in match get_costlabels_of_measurable_trace in prf; normalize nodelta in prf;
966    cases(mem_append ???? prf) -prf
967    [2: #prf cases(mem_map ????? (labels_of_trace_are_in_code … prf)) *
968        #lbl' #pc * #Hmem #EQ destruct   
969        >(proj1 … (static_analisys_ok … no_dup … EQmap … Hmem))
970        @(proj2 … (static_analisys_ok … no_dup … EQmap … Hmem))
971    | inversion(L_label … t) normalize nodelta [| #lbl'] #EQleft
972      [ * [2: *] #EQ destruct >(proj1 … (static_analisys_ok … no_dup … EQmap … (i_act_in_map …)))
973        @(proj2 … (static_analisys_ok … no_dup … EQmap … (i_act_in_map …)))
974      | #H lapply(L_init_ok … t) inversion(L_pre_state … t) [ #_ normalize nodelta * #_ >EQleft #EQ destruct]
975        #st_pre #EQst_pre normalize nodelta * #l' ** >EQleft #EQ destruct cases l' in H;
976        [ #x1 #x2 | * [|#x1] | * [|#x1]] whd in ⊢ (% → %→ ?); * [2,4,6: *] #EQ destruct * * #_
977        #H cases(as_execute_labelled_ok … H) [3,6,9:% |*:] #w #EQw
978        >(proj1 … (static_analisys_ok … no_dup … EQmap … EQw))
979       @(proj2 … (static_analisys_ok … no_dup … EQmap … EQw))
980      ]
981    ]
982]
983#p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap1 #t #a1 #rel_galois #abs_trace #EQabs_trace
984@(static_dynamic …)
985
986xxxxxx
987lapply(static_dynamic … (trace …t) … abs_trace) try //
988
989
Note: See TracBrowser for help on using the repository browser.