source: LTS/Vm.ma @ 3464

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

static_dinamic in place

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