source: LTS/Vm.ma @ 3553

Last change on this file since 3553 was 3552, checked in by piccolo, 5 years ago

closed all daemons

File size: 53.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) (l_p : label_params) : Type[0] ≝
20| Seq : seq_instr p → option (NonFunctionalLabel l_p) →  AssemblerInstr p l_p
21| Ijmp: ℕ → AssemblerInstr p l_p
22| CJump : jump_condition p → ℕ → NonFunctionalLabel l_p → NonFunctionalLabel l_p → AssemblerInstr p l_p
23| Iio : NonFunctionalLabel l_p → io_instr p → NonFunctionalLabel l_p → AssemblerInstr p l_p
24| Icall: FunctionName → AssemblerInstr p l_p
25| Iret: AssemblerInstr p l_p.
26
27definition labels_pc_of_instr : ∀p,l_p.AssemblerInstr p l_p → ℕ → list (CostLabel l_p × ℕ) ≝
28λp,l_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) (l_p : label_params)
44(prog : list (AssemblerInstr p l_p)) (call_label_fun : list (ℕ × (CallCostLabel l_p)))
45              (return_label_fun : list (ℕ × (ReturnPostCostLabel l_p))) (i_act : NonFunctionalLabel l_p)
46              (program_counter : ℕ) on prog : list ((CostLabel l_p) × ℕ) ≝
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 l_p is call_label_fun return_label_fun i_act (S program_counter)
52].
53
54include "basics/lists/listb.ma".
55
56
57record AssemblerProgram (p : assembler_params) (l_p : label_params) : Type[0] ≝
58{ instructions : list (AssemblerInstr p l_p)
59; endmain : ℕ
60; endmain_ok : endmain < |instructions|
61; entry_of_function : FunctionName → ℕ
62; call_label_fun : list (ℕ × (CallCostLabel l_p))
63; return_label_fun : list (ℕ × (ReturnPostCostLabel l_p))
64; in_act : NonFunctionalLabel l_p
65; asm_no_duplicates : no_duplicates … (map ?? \fst … (labels_pc … instructions call_label_fun return_label_fun in_act O))
66}.
67
68
69definition fetch: ∀p,l_p.AssemblerProgram p l_p → ℕ → option (AssemblerInstr p l_p) ≝
70 λp,l_p,l,n. nth_opt ? n (instructions … l).
71
72definition stackT: Type[0] ≝ list (nat).
73
74record sem_params (p : assembler_params) : Type[1] ≝
75{ asm_store_type : Type[0]
76; eval_asm_seq : seq_instr p → asm_store_type → option asm_store_type
77; eval_asm_cond : jump_condition p → asm_store_type → option bool
78; eval_asm_io : io_instr p → asm_store_type → option asm_store_type
79}.
80
81record vm_state (p : assembler_params) (p' : sem_params p) : Type[0] ≝
82{ pc : ℕ
83; asm_stack : stackT
84; asm_store : asm_store_type … p'
85; asm_is_io : bool
86}.
87
88definition label_of_pc ≝ λL.λl.λpc.find …
89   (λp.let 〈x,y〉 ≝ p in if eqb x pc then Some L y else None ? ) l.
90   
91definition option_pop ≝
92  λA.λl:list A. match l with
93  [ nil ⇒ None ?
94  | cons a tl ⇒ Some ? (〈a,tl〉) ].
95
96
97inductive vmstep (p : assembler_params) (p' : sem_params p) (l_p : label_params)
98   (prog : AssemblerProgram p l_p)  :
99      ActionLabel l_p → relation (vm_state p p') ≝
100| vm_seq : ∀st1,st2 : vm_state p p'.∀i,l.
101           fetch … prog (pc … st1) = return (Seq p l_p i l) →
102           asm_is_io … st1 = false →
103           eval_asm_seq p p' i (asm_store … st1) = return asm_store … st2 → 
104           asm_stack … st1 = asm_stack … st2 →
105           asm_is_io … st1 = asm_is_io … st2 →
106           S (pc … st1) = pc … st2 →
107           vmstep … (cost_act … l) st1 st2
108| vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ.
109           fetch … prog (pc … st1) = return (Ijmp p l_p new_pc) →
110           asm_is_io … st1 = false →
111           asm_store … st1 = asm_store … st2 →
112           asm_stack … st1 = asm_stack … st2 →
113           asm_is_io … st1 = asm_is_io … st2 →
114           new_pc = pc … st2 →
115           vmstep … (cost_act … (None ?)) st1 st2
116| vm_cjump_true :
117           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
118           eval_asm_cond p p' cond (asm_store … st1) = return true→
119           fetch … prog (pc … st1) = return (CJump p l_p cond new_pc ltrue lfalse) →
120           asm_is_io … st1 = false →
121           asm_store … st1 = asm_store … st2 →
122           asm_stack … st1 = asm_stack … st2 →
123           asm_is_io … st1 = asm_is_io … st2 →
124           pc … st2 = new_pc →
125           vmstep … (cost_act … (Some ? ltrue)) st1 st2
126| vm_cjump_false :
127           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
128           eval_asm_cond p p' cond (asm_store … st1) = return false→
129           fetch … prog (pc … st1) = return (CJump p l_p cond new_pc ltrue lfalse) →
130           asm_is_io … st1 = false →
131           asm_store … st1 = asm_store … st2 →
132           asm_stack … st1 = asm_stack … st2 →
133           asm_is_io … st1 = asm_is_io … st2 →
134           S (pc … st1) = pc … st2 →
135           vmstep … (cost_act … (Some ? lfalse)) st1 st2
136| vm_io_in : 
137           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
138           fetch … prog (pc … st1) = return (Iio p l_p lin io lout) →
139           asm_is_io … st1 = false →
140           asm_store … st1 = asm_store … st2 →
141           asm_stack … st1 = asm_stack … st2 →
142           true = asm_is_io … st2 →
143           pc … st1 = pc … st2 →
144           vmstep … (cost_act … (Some ? lin)) st1 st2
145| vm_io_out :
146           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
147           fetch … prog (pc … st1) = return (Iio p l_p lin io lout) →
148           asm_is_io … st1 = true →
149           eval_asm_io … io (asm_store … st1) = return asm_store … st2 →
150           asm_stack … st1 = asm_stack … st2 →
151           false = asm_is_io … st2 →
152           S (pc … st1) = pc … st2 →
153           vmstep … (cost_act … (Some ? lout)) st1 st2
154| vm_call :
155           ∀st1,st2 : vm_state p p'.∀f,lbl.
156           fetch … prog (pc … st1) = return (Icall p l_p f) →
157           asm_is_io … st1 = false →
158           asm_store … st1 = asm_store … st2 →
159           S (pc … st1) ::  asm_stack … st1 = asm_stack … st2 →
160           asm_is_io … st1 = asm_is_io … st2 →
161           entry_of_function … prog f = pc … st2 →
162           label_of_pc … (call_label_fun … prog) (entry_of_function … prog f) = return lbl →
163           vmstep … (call_act … f lbl) st1 st2
164| vm_ret :
165          ∀st1,st2 : vm_state p p'.∀newpc,lbl.
166           fetch … prog (pc … st1) = return (Iret p l_p) →
167           asm_is_io … st1 = false →
168           asm_store … st1 = asm_store … st2 →
169           asm_stack … st1 = newpc ::  asm_stack … st2  →
170           asm_is_io … st1 = asm_is_io … st2 →
171           newpc = pc … st2 →
172           label_of_pc … (return_label_fun … prog) newpc = return lbl →
173           vmstep … (ret_act … (Some ? lbl)) st1 st2.
174
175definition eval_vmstate : ∀p : assembler_params.∀p' : sem_params p.∀l_p : label_params.
176AssemblerProgram p l_p → vm_state p p' → option ((ActionLabel l_p) × (vm_state p p')) ≝
177λp,p',l_p,prog,st.
178! i ← fetch … prog (pc … st);
179match i with
180[ Seq x opt_l ⇒
181   if asm_is_io … st then
182     None ?
183   else
184     ! new_store ← eval_asm_seq p p' x (asm_store … st);
185     return 〈cost_act … opt_l,
186             mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false〉
187| Ijmp newpc ⇒
188   if asm_is_io … st then
189     None ?
190   else
191     return 〈cost_act … (None ?),
192             mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false〉
193| CJump cond newpc ltrue lfalse ⇒
194   if asm_is_io … st then
195     None ?
196   else
197     ! b ← eval_asm_cond p p' cond (asm_store … st);
198     if b then
199       return 〈cost_act …(Some ? ltrue),
200               mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false〉
201     else
202       return 〈cost_act … (Some ? lfalse),
203               mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false〉
204| Iio lin io lout ⇒
205              if asm_is_io … st then
206                 ! new_store ← eval_asm_io … io (asm_store … st);
207                 return 〈cost_act … (Some ? lout),
208                         mk_vm_state ?? (S (pc … st)) (asm_stack … st)
209                         new_store false〉   
210              else
211                return 〈cost_act … (Some ? lin),
212                        mk_vm_state ?? (pc … st) (asm_stack … st) (asm_store … st)
213                                    true〉
214| Icall f ⇒
215    if asm_is_io … st then
216      None ?
217    else
218      ! lbl ← label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f);
219      return 〈call_act … f lbl,
220              mk_vm_state ?? (entry_of_function … prog f)
221                             ((S (pc … st)) :: (asm_stack … st))
222                             (asm_store … st) false〉
223| Iret ⇒ if asm_is_io … st then
224            None ?
225         else
226            ! 〈newpc,tl〉 ← option_pop … (asm_stack … st);
227            ! lbl ← label_of_pc ? (return_label_fun … prog) newpc;
228            return 〈ret_act … (Some ? lbl),
229                    mk_vm_state ?? newpc tl (asm_store … st) false〉
230].
231
232lemma eval_vmstate_to_Prop : ∀p,p',l_p,prog,st1,st2,l.
233eval_vmstate p p' l_p prog st1 = return 〈l,st2〉 → vmstep … prog l st1 st2.
234#p #p' #l_p #prog #st1 #st2 #l whd in match eval_vmstate; normalize nodelta
235#H cases(bind_inversion ????? H) -H * normalize nodelta
236[ #seq #opt_l * #EQfetch inversion(asm_is_io ???) normalize nodelta
237  [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H)
238  #newstore * #EQnewstore whd in ⊢ (??%% → ?); #EQ destruct
239  @vm_seq //
240| #newpc * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
241  [ whd in ⊢ (??%% → ?); #EQ destruct] whd in ⊢ (??%% → ?); #EQ destruct
242  @vm_ijump //
243| #cond #new_pc #ltrue #lfase * #EQfetch inversion(asm_is_io ???) normalize nodelta
244  [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H) -H
245  * normalize nodelta * #EQcond whd in ⊢ (??%% → ?); #EQ destruct
246  [ @(vm_cjump_true … EQfetch) // | @(vm_cjump_false … EQfetch) //]
247| #lin #io #lout * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
248  [ #H cases(bind_inversion ????? H) -H #newstore * #EQnewstore ]
249  whd in ⊢ (??%% → ?); #EQ destruct
250  [ @(vm_io_out … EQfetch) // | @(vm_io_in … EQfetch) // ]
251| #f * #EQfetch inversion(asm_is_io ???) #EQio normalize nodelta
252  [ whd in ⊢ (??%% → ?); #EQ destruct ] #H cases (bind_inversion ????? H) -H
253  #lbl * #EQlb whd in ⊢ (??%% → ?); #EQ destruct @(vm_call … EQfetch) //
254| * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
255  [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H
256  * #newpc #tl * whd in match option_pop; normalize nodelta inversion(asm_stack ???)
257  normalize nodelta [#_ whd in ⊢ (??%% → ?); #EQ destruct] #newpc1 #tl1 #_
258  #EQstack whd in ⊢ (??%% → ?); #EQ destruct #H cases(bind_inversion ????? H) #lbl
259  * #EQlbl whd in ⊢ (??%% → ?); #EQ destruct @vm_ret //
260]
261qed.
262
263 
264lemma vm_step_to_eval : ∀p,p',l_p,prog,st1,st2,l.vmstep … prog l st1 st2 →
265eval_vmstate p p' l_p prog st1 = return 〈l,st2〉.
266#p #p' #l_p #prog * #pc1 #stack1 #store1 #io1
267* #pc2 #stack2 #store2 #io2 #l #H inversion H
268[ #s1 #s2 #i #opt_l #EQfetch #EQio #EQstore #EQstack #EQio1 #EQpc
269  #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta   
270  >EQfetch >m_return_bind normalize nodelta >EQio normalize nodelta >EQstore
271  >m_return_bind <EQio1 >EQio <EQpc >EQstack %
272| #s1 #s2 #newpc #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc
273  #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta
274  >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta <EQio2 >EQio1
275  >EQstore >EQstack >EQstore %
276|3,4: #s1 #s2 #cond #newoc #ltrue #lfalse #EQev_cond #EQfetch #EQio1 #EQstore
277  #EQstack #EQio2 #EQnewoc #EQ1 #EQ2 #EQ3 #EQ4 destruct
278  whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind
279  normalize nodelta >EQio1 normalize nodelta >EQev_cond >m_return_bind
280  normalize nodelta <EQio1 >EQio2 >EQstore >EQstack  >EQstore [%] >EQnewoc %
281|5,6: #s1 #s2 #lin #io #lout #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQpc
282   #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
283   normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1
284   normalize nodelta >EQstack <EQpc [ >EQstore <EQio2 %]
285   >EQstore >m_return_bind <EQpc <EQio2 %
286| #s1 #s2 #f #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQentry
287  #EQlab_pc #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
288  normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1
289  normalize nodelta >EQlab_pc >m_return_bind >EQentry <EQio2 >EQio1
290  <EQstack >EQstore %
291| #s1 #s2 #newpc #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc
292  #EQlab_pc #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
293  normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta
294  >EQstack whd in match option_pop; normalize nodelta >m_return_bind
295  >EQlab_pc >m_return_bind >EQstore  <EQio2 >EQio1 %
296]
297qed.
298
299coercion vm_step_to_eval.
300
301include "../src/utilities/hide.ma".
302
303discriminator option.
304
305inductive vm_ass_state  (p : assembler_params) (p' : sem_params p) : Type[0] ≝
306| INITIAL : vm_ass_state p p'
307| FINAL : vm_ass_state p p'
308| STATE : vm_state p p' → vm_ass_state p p'.
309
310definition ass_vmstep ≝
311 λp,p',l_p,prog.
312  λl.λs1,s2 : vm_ass_state p p'.
313                    match s1 with
314                    [ STATE st1 ⇒
315                        match s2 with
316                        [ STATE st2 ⇒ 
317                            (eqb (pc ?? st1) (endmain … prog)) = false ∧ vmstep p p' l_p prog l st1 st2
318                        | INITIAL ⇒ False
319                        | FINAL ⇒ eqb (pc … st1) (endmain … prog) = true ∧
320                           l = cost_act … (Some … (in_act … prog))
321                        ]
322                    | INITIAL ⇒ match s2 with
323                                [ STATE st2 ⇒ eqb (pc … st2) O = true ∧
324                                   l = cost_act … (Some … (in_act … prog))
325                                | _ ⇒ False
326                                ]
327                    | FINAL ⇒ False
328                    ].
329
330definition asm_operational_semantics : ∀p,l_p.sem_params p → AssemblerProgram p l_p →  abstract_status l_p ≝
331λp,l_p,p',prog.let init_act ≝ cost_act … (Some ? (in_act … prog)) in
332           let end_act ≝ cost_act … (Some ? (in_act … prog)) in
333    mk_abstract_status …
334                (vm_ass_state p p')
335                (ass_vmstep … prog)
336                (λ_.λ_.True)
337                (λst.match st with
338                    [ INITIAL ⇒ cl_other | FINAL ⇒ cl_other |
339                     STATE s ⇒
340                      match fetch … prog (pc … s) with
341                      [ Some i ⇒ match i with
342                               [ Seq _ _ ⇒ cl_other
343                               | Ijmp _ ⇒ cl_other
344                               | CJump _ _ _ _ ⇒ cl_jump
345                               | Iio _ _ _ ⇒ if asm_is_io … s then cl_io else cl_other
346                               | Icall _ ⇒ cl_other
347                               | Iret ⇒ cl_other
348                               ]
349                     | None ⇒ cl_other
350                     ]
351                    ]
352                )
353                (λ_.true)
354                (λs.match s with [ INITIAL ⇒ true | _ ⇒ false])
355                (λs.match s with [ FINAL ⇒ true | _ ⇒ false])
356                ???.
357@hide_prf
358[ #s1 #s2 #l
359 cases s1 normalize nodelta [1,2: #abs destruct] -s1 #s1
360 cases s2 normalize nodelta [1: #_ * |2: #_ * #_ #EQ >EQ normalize /2/ ] #s2 
361 inversion(fetch ???) normalize nodelta
362  [ #_ #EQ destruct] * normalize nodelta
363  [ #seq #lbl #_
364  | #n #_
365  | #cond #newpc #ltrue #lfalse #EQfetch
366  | #lin #io #lout #_ cases (asm_is_io ??) normalize nodelta
367  | #f #_
368  | #_
369  ]
370  #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate;
371  normalize nodelta >EQfetch >m_return_bind normalize nodelta cases(asm_is_io ??)
372  normalize nodelta [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H
373  * * #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct % //
374| #s1 #s2 #l
375  cases s1 normalize nodelta [2: #_ * |3: #s1 ]
376  cases s2 normalize nodelta [1,2,4,5: #abs destruct ] #s2 [2: #_ * #_ /2/ ]
377  inversion(fetch ???) normalize nodelta
378  [ #_ #EQ destruct] * normalize nodelta
379  [ #seq #lbl #_
380  | #n #_
381  | #cond #newpc #ltrue #lfalse #_
382  | #lin #io #lout #EQfetch inversion (asm_is_io ??) #EQio normalize nodelta
383  | #f #_
384  | #_
385  ]
386  #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate;
387  normalize nodelta #H cases(bind_inversion ????? H) -H *
388  [ #seq1 #lbl1
389  | #n1
390  | #cond1 #newpc1 #ltrue1 #lfalse1
391  | #lin1 #io1 #lout1
392  | #f
393  |
394  ]
395  normalize nodelta * #_ cases(asm_is_io ??) normalize nodelta
396  [1,3,5,9,11: whd in ⊢ (??%% → ?); #EQ destruct
397  |2,6,7,10,12: #H cases(bind_inversion ????? H) -H #x * #_
398    [2: cases x normalize nodelta
399    |5: #H cases(bind_inversion ????? H) -H #y * #_
400    ]
401  ]
402  whd in ⊢ (??%% → ?); #EQ destruct destruct % //
403| #s1 #s2 #l
404  cases s1 normalize nodelta [1,2: #abs destruct ] #s1
405  cases s2 normalize nodelta [ #_ * | #_ * /2/ ] #s2
406  inversion(fetch ???) normalize nodelta
407  [ #_ #EQ destruct] * normalize nodelta
408  [ #seq #lbl #_
409  | #n #_
410  | #cond #newpc #ltrue #lfalse #_
411  | #lin #io #lout #EQfetch inversion(asm_is_io ??) normalize nodelta #EQio
412  | #f #_
413  | #_
414  ]
415  #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate;
416  normalize nodelta  >EQfetch >m_return_bind normalize nodelta >EQio
417  normalize nodelta #H cases(bind_inversion ????? H) -H #x * #_
418  whd in ⊢ (??%% → ?); #EQ destruct % //
419qed.
420
421definition asm_concrete_trans_sys ≝
422λp,p',l_p,prog.mk_concrete_transition_sys …
423             (asm_operational_semantics p p' l_p prog).
424             
425         
426definition emits_labels ≝
427λp,l_p.λinstr : AssemblerInstr p l_p.match instr with
428        [ Seq _ opt_l ⇒ match opt_l with
429                        [ None ⇒ Some ? (λpc.S pc)
430                        | Some _ ⇒ None ?
431                        ]
432        | Ijmp newpc ⇒ Some ? (λ_.newpc)
433        | _ ⇒ None ?
434        ].
435
436definition fetch_state : ∀p,p',l_p.AssemblerProgram p l_p → vm_state p p' → option (AssemblerInstr p l_p) ≝
437λp,p',l_p,prog,st.fetch … prog (pc … st).
438
439record asm_galois_connection (p: assembler_params) (p': sem_params p) (l_p : label_params) (prog: AssemblerProgram p l_p) : Type[2] ≝
440{ aabs_d : abstract_transition_sys
441; agalois_rel:> galois_rel … (asm_concrete_trans_sys p l_p p' prog) aabs_d
442}.
443
444definition galois_connection_of_asm_galois_connection:
445 ∀p,p',l_p,prog. asm_galois_connection p p' l_p prog → galois_connection l_p ≝
446 λp,p',l_p,prog,agc.
447  mk_galois_connection …
448   (asm_concrete_trans_sys p l_p p' prog)
449   (aabs_d … agc)
450   (agalois_rel … agc).
451
452coercion galois_connection_of_asm_galois_connection.
453
454definition ass_fetch ≝
455 λp,p',l_p,prog.
456    λs.match s with [ STATE st ⇒ if eqb (pc … st) (endmain p l_p prog) then
457                                   Some ? (None ?)
458                               else ! x ← fetch_state p p' l_p prog st; Some ? (Some ? x)
459                    | INITIAL ⇒ Some ? (None ?)
460                    | FINAL  ⇒ None ? ].
461
462definition ass_instr_map ≝
463 λp,p',l_p,prog.λasm_galois_conn: asm_galois_connection p p' l_p prog.
464  λinstr_map: AssemblerInstr p l_p → (*option*) (abs_instr … (abs_d … asm_galois_conn)).
465  (λi.match i with [None ⇒ (*Some …*) (e …) |Some x ⇒ instr_map … x]).
466
467record asm_abstract_interpretation (p: assembler_params) (p': sem_params p) (l_p : label_params) (prog: AssemblerProgram p l_p) : Type[2] ≝
468{ asm_galois_conn: asm_galois_connection p p' l_p prog
469; instr_map : AssemblerInstr p l_p → (*option*) (abs_instr … (abs_d … asm_galois_conn))
470; instr_map_ok :
471   ∀s,s': concr … asm_galois_conn. ∀a: abs_d … asm_galois_conn.∀l,i.
472    as_execute … l s s' →
473     ass_fetch … prog s = Some ? i →
474      ∀I. ass_instr_map … instr_map i = (*Some ?*) I →
475       asm_galois_conn s a → asm_galois_conn s' (〚I〛 a)
476}.
477
478definition abstract_interpretation_of_asm_abstract_interpretation:
479 ∀p,p',l_p,prog. asm_abstract_interpretation p p' l_p prog → abstract_interpretation l_p
480
481λp,p',l_p,prog,aai.
482 mk_abstract_interpretation …
483  (asm_galois_conn … aai) (option (AssemblerInstr p l_p)) (ass_fetch p p' l_p prog)
484   (ass_instr_map … prog … (instr_map … aai)) (instr_map_ok … aai).
485
486coercion abstract_interpretation_of_asm_abstract_interpretation.
487
488definition non_empty_list : ∀A.list A → bool ≝
489λA,l.match l with [ nil ⇒ false | _ ⇒  true ].
490
491let rec block_cost (p : assembler_params) (l_p : label_params)
492 (prog: AssemblerProgram p l_p) (abs_t : monoid)
493 (instr_m : AssemblerInstr p l_p → abs_t)
494 (prog_c: option ℕ)
495    (program_size: ℕ)
496        on program_size: option abs_t ≝
497match prog_c with
498[ None ⇒ return e … abs_t
499| Some program_counter ⇒
500  match program_size with
501    [ O ⇒ None ?
502    | S program_size' ⇒
503       if eqb program_counter (endmain … prog) then
504        return e … abs_t
505      else
506      ! instr ← fetch … prog program_counter;
507      ! n ← (match emits_labels … instr with
508            [ Some f ⇒ block_cost … prog abs_t instr_m (Some ? (f program_counter)) program_size'
509            | None ⇒ return e …
510            ]);
511      return (op … abs_t (instr_m … instr) n)
512    ]
513].
514
515
516record cost_map_T (dom : DeqSet) (codom : Type[0]) : Type[1] ≝
517{ map_type :> Type[0]
518; empty_map : map_type
519; get_map : map_type → dom → option codom
520; set_map : map_type → dom → codom → map_type
521; get_set_hit : ∀k,v,m.get_map (set_map m k v) k = return v
522; get_set_miss : ∀k1,k2,v,m.(k1 == k2) = false → get_map (set_map m k1 v) k2 = get_map m k2
523}.
524
525
526
527lemma labels_pc_ok : ∀p,l_p,prog,l1,l2,i_act,i,lbl,pc,m.
528nth_opt ? pc prog = return i →
529mem ? lbl (labels_pc_of_instr … i (m+pc)) →
530mem ? lbl (labels_pc p l_p prog l1 l2 i_act m).
531#p #l_p #instrs #l1 #l2 #iact #i #lbl #pc
532whd in match fetch; normalize nodelta lapply pc -pc
533elim instrs
534[ #pc #m whd in ⊢ (??%% → ?); #EQ destruct]
535#x #xs #IH * [|#pc'] #m  whd in ⊢ (??%% → ?);
536[ #EQ destruct #lbl_addr whd in match (labels_pc ???);
537  /2 by mem_append_l1/
538| #EQ #H2 whd in match (labels_pc ???); @mem_append_l2 @(IH … EQ) //
539]
540qed.
541
542lemma labels_pf_in_act: ∀p,l_p,prog,pc.
543  mem (CostLabel l_p) (in_act p l_p prog)
544  (map ((CostLabel l_p)×ℕ) (CostLabel l_p) \fst
545   (labels_pc p … (instructions p …  prog) (call_label_fun p … prog)
546    (return_label_fun p …  prog) (in_act p … prog) pc)).
547 #p #l_p #prog elim (instructions … prog) normalize /2/
548qed.
549
550lemma labels_pc_return: ∀p,l_p,prog,l1,l2,iact,x1,x2.
551 label_of_pc (ReturnPostCostLabel l_p) l2 x1=return x2 →
552 ∀m.
553   mem … 〈(a_return_post … x2),x1〉 (labels_pc p l_p prog l1 l2 iact m).
554 #p #l_p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l
555[ #m @mem_append_l2 @mem_append_l2 whd in H:(??%?);
556  elim l2 in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
557  * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim
558  normalize nodelta
559  [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/
560  | #NEQ #H2 %2 @IH // ]
561| #hd #tl #IH #m @mem_append_l2 @IH ]
562qed.
563
564lemma labels_pc_call: ∀p,l_p,prog,l1,l2,iact,x1,x2.
565 label_of_pc (CallCostLabel l_p) l1 x1=return x2 →
566 ∀m.
567   mem … 〈(a_call l_p x2),x1〉 (labels_pc p l_p prog l1 l2 iact m).
568 #p #l_p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l
569[ #m @mem_append_l2 @mem_append_l1 whd in H:(??%?);
570  elim l1 in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
571  * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim
572  normalize nodelta
573  [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/
574  | #NEQ #H2 %2 @IH // ]
575| #hd #tl #IH #m @mem_append_l2 @IH ]
576qed.
577
578(*
579lemma labels_pc_bounded : ∀p.∀prog : AssemblerProgram p.∀lbl,pc.∀m.
580mem ? 〈lbl,pc〉 (labels_pc p (instructions … prog) m) →
581(m + pc) < (|(instructions … prog)|).
582#p * #instr #endmain #_  #H1 #H2 elim instr
583[ #H3 @⊥ /2/ ] #x #xs #IH #_ #lbl #pc #m whd in match (labels_pc ???);
584#H cases(mem_append ???? H) -H
585[ whd in match labels_pc_of_instr; normalize nodelta
586  cases x normalize nodelta
587  [ #seq * [|#lab]
588  | #newpc
589  | #cond #newpc #ltrue #lfalse
590  | #lin #io #lout
591  | #f
592  |
593  ]
594  normalize [1,3,6,7: *] * [2,4,6: * [2,4:*] ]
595  #EQ destruct
596*) 
597
598let rec m_foldr (M : Monad) (X,Y : Type[0]) (f : X→Y→M Y) (l : list X) (y : Y) on l : M Y ≝
599match l with
600[ nil ⇒ return y
601| cons x xs ⇒ ! z ← m_foldr M X Y f xs y; f x z
602].
603
604definition static_analisys : ∀p : assembler_params.∀l_p : label_params.∀abs_t : monoid.(AssemblerInstr p l_p → abs_t …) →
605∀mT : cost_map_T (DEQCostLabel l_p) (abs_t …).AssemblerProgram p l_p → option mT ≝
606λp,l_p,abs_t,instr_m,mT,prog.
607let prog_size ≝ S (|instructions … prog|) in
608m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p l_p prog abs_t instr_m (Some ? w) prog_size; 
609                               return set_map … m z k) (labels_pc … (instructions … prog)
610                                         (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)
611      (empty_map ?? mT).
612     
613
614definition eq_deq_prod : ∀D1,D2 : DeqSet.D1 × D2 → D1 × D2 → bool ≝
615λD1,D2,x,y.\fst x == \fst y ∧ \snd x == \snd y.
616
617definition DeqProd ≝ λD1 : DeqSet.λD2 : DeqSet.
618mk_DeqSet (D1 × D2) (eq_deq_prod D1 D2) ?.
619@hide_prf
620* #x1 #x2 * #y1 #y2 whd in match eq_deq_prod; normalize nodelta
621% [2: #EQ destruct @andb_Prop >(\b (refl …)) %]
622inversion (? ==?) #EQ1 whd in match (andb ??); #EQ2 destruct
623>(\P EQ1) >(\P EQ2) %
624qed.
625(*
626unification hint  0 ≔ D1,D2 ;
627    X ≟ DeqProd D1 D2
628(* ---------------------------------------- *) ⊢
629    D1 × D2 ≡ carr X.
630
631
632unification hint  0 ≔ D1,D2,p1,p2;
633    X ≟ DeqProd D1 D2
634(* ---------------------------------------- *) ⊢
635    eq_deq_prod D1 D2 p1 p2 ≡ eqb X p1 p2.
636   
637definition deq_prod_to_prod : ∀D1,D2 : DeqSet.DeqProd D1 D2 → D1 × D2 ≝
638λD1,D2,x.x.
639
640coercion deq_prod_to_prod.
641*)
642
643lemma map_mem : ∀A,B,f,l,a.mem A a l → ∃b : B.mem B b (map A B f l)
644∧ b = f a.
645#A #B #f #l elim l [ #a *] #x #xs #IH #a *
646[ #EQ destruct %{(f x)} % // % // | #H cases(IH … H)
647  #b * #H1 #EQ destruct %{(f a)} % // %2 //
648]
649qed.
650
651lemma static_analisys_ok : ∀p,l_p,abs_t,instr_m,mT,prog,lbl,pc,map.
652static_analisys p l_p abs_t instr_m mT prog = return map →
653mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) (call_label_fun … prog)
654                   (return_label_fun … prog) (in_act … prog) O) →
655get_map … map lbl =
656block_cost … prog abs_t instr_m (Some ? pc) (S (|(instructions … prog)|)) ∧
657block_cost … prog abs_t instr_m (Some ? pc) (S (|(instructions … prog)|)) ≠ None ?.
658#p #l_p #abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta
659#endmain #Hendmain #entry_fun #call_label_fun #return_label_fun #inact
660#nodup generalize in match nodup in ⊢ (∀_.∀_.∀_. (??(????%??)?) → %); #Hnodup lapply nodup -nodup
661lapply (labels_pc ???????) #l elim l [ #x #y #z #w #h * ]
662* #hd1 #hd2 #tl #IH * #H1 #H2 #lbl #pc #map #H
663cases(bind_inversion ????? H) -H #map1 * #EQmap1 normalize nodelta #H
664cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); #EQ
665destruct *
666[ #EQ destruct % [ >get_set_hit >EQelem % | >EQelem % whd in ⊢ (??%% → ?); #EQ destruct]
667| #H %
668  [ >get_set_miss [ @(proj1 … (IH …)) //] inversion (? == ?) [2: #_ %]
669    #ABS cases H1 -H1 #H1 @⊥ @H1 >(\P ABS) >mem_to_memb //
670    cases(map_mem … \fst … H) #z1 * #Hz1 #EQ destruct @Hz1
671  | @(proj2 … (IH …)) //
672  ]
673]
674qed.
675
676definition terminated_trace : ∀p : label_params.∀S : abstract_status p.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝
677λp,S,s1,s3,t.∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind p ? s2 s3 s3 l prf … (t_base … s3))
678∧ is_costlabelled_act … l ∧ pre_measurable_trace … t1.
679
680definition big_op: ∀M: monoid. list M → M ≝
681 λM. foldl … (op … M) (e … M).
682
683lemma big_op_associative:
684 ∀M:monoid. ∀l1,l2.
685  big_op M (l1@l2) = op M (big_op … l1) (big_op … l2).
686 #M #l1 whd in match big_op; normalize nodelta
687 generalize in match (e M) in ⊢ (? → (??%(??%?))); elim l1
688 [ #c #l2 whd in match (append ???); normalize lapply(neutral_r … c)
689   generalize in match c in ⊢ (??%? → ???%); lapply c -c lapply(e M)
690   elim l2 normalize
691   [ #c #c1 #c2 #EQ @sym_eq //
692   | #x #xs #IH #c1 #c2 #c3 #EQ <EQ <IH [% | <is_associative % |]
693   ]
694 | #x #xs #IH #c #l2 @IH
695 ]
696qed.
697
698lemma act_big_op : ∀M,B. ∀act : monoid_action M B.
699 ∀l1,l2,x.
700   act (big_op M (l1@l2)) x = act (big_op … l2) (act (big_op … l1) x).
701 #M #B #act #l1 elim l1
702 [ #l2 #x >act_neutral //
703 | #hd #tl #IH #l2 #x change with ([?]@(tl@l2)) in match ([?]@(tl@l2));
704   >big_op_associative >act_op >IH change with ([hd]@tl) in match ([hd]@tl);
705   >big_op_associative >act_op in ⊢ (???%); %
706 ]
707qed.
708
709lemma monotonicity_of_block_cost : ∀p,l_p,prog,abs_t,instr_m,pc,size,k.
710block_cost p l_p prog abs_t instr_m (Some ? pc) size = return k →
711∀size'.size ≤ size' →
712block_cost p l_p prog abs_t instr_m (Some ? pc) size' = return k.
713#p #l_p #prog #abs_t #instr_m #pc #size lapply pc elim size
714[ #pc #k whd in ⊢ (??%% → ?); #EQ destruct]
715#n #IH #pc #k whd in ⊢ (??%% → ?); @eqb_elim
716[ #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct
717  #size' * [2: #m #_] whd in ⊢ (??%%); @eqb_elim try( #_ %) * #H @⊥ @H %
718| #Hpc normalize nodelta #H cases(bind_inversion ????? H) -H #i
719  * #EQi #H cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?);
720  #EQ destruct #size' *
721  [ whd in ⊢ (??%?); @eqb_elim
722    [ #EQ @⊥ @(absurd ?? Hpc) assumption ]
723    #_ normalize nodelta >EQi >m_return_bind >EQelem %
724  | #m #Hm whd in ⊢ (??%?); @eqb_elim
725    [ #EQ @⊥ @(absurd ?? Hpc) assumption ]
726    #_ normalize nodelta >EQi >m_return_bind
727    cases (emits_labels ??) in EQelem; normalize nodelta
728    [ whd in ⊢ (??%%→ ??%%); #EQ destruct %]
729    #f #EQelem >(IH … EQelem) [2: /2/ ] %
730  ]
731]
732qed.
733
734lemma step_emit : ∀p,p',l_p,prog,st1,st2,l,i.
735fetch p l_p prog (pc … st1) = return i →
736eval_vmstate p p' … prog st1 = return 〈l,st2〉 → 
737emits_labels … i = None ? → ∃x.
738match l in ActionLabel return λ_: (ActionLabel l_p).(list (CostLabel l_p)) with 
739[call_act f c ⇒ [a_call … c]
740|ret_act x ⇒
741   match x with [None⇒[]|Some c⇒[a_return_post … c]]
742|cost_act x ⇒
743   match x with [None⇒[]|Some c⇒[a_non_functional_label … c]]
744] = [x] ∧
745 (mem … 〈x,pc … st2〉 (labels_pc p l_p (instructions … prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)).
746#p #p' #l_p #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta
747>EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta
748[ #seq * [|#lab]
749| #newpc
750| #cond #newpc #ltrue #lfalse
751| #lin #io #lout
752| #f
753|
754]
755#EQi cases(asm_is_io ???) normalize nodelta
756[1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
757|2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1
758  [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta
759  |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2
760  ]
761]
762whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels;
763normalize nodelta #EQ destruct % [2,4,6,8,10,12,14: % try % |*:]
764[1,2,4,5,7: @(labels_pc_ok … EQi) normalize /3 by or_introl,or_intror/ ]
765/2 by labels_pc_return, labels_pc_call/
766qed.
767
768lemma step_non_emit : ∀p,p',l_p,prog,st1,st2,l,i,f.
769fetch p l_p prog (pc … st1) = return i →
770eval_vmstate p p' … prog st1 = return 〈l,st2〉 → 
771emits_labels … i = Some ? f →
772match l in ActionLabel return λ_: (ActionLabel l_p).(list (CostLabel l_p)) with 
773[call_act f c ⇒ [a_call … c]
774|ret_act x ⇒
775   match x with [None⇒[]|Some c⇒[a_return_post … c]]
776|cost_act x ⇒
777   match x with [None⇒[]|Some c⇒[a_non_functional_label … c]]
778] = [ ] ∧ pc … st2 = f (pc … st1).
779#p #p' #l_p #prog #st1 #st2 #l #i #f #EQi whd in match eval_vmstate; normalize nodelta
780>EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta
781[ #seq * [|#lab]
782| #newpc
783| #cond #newpc #ltrue #lfalse
784| #lin #io #lout
785| #f
786|
787]
788#EQi cases(asm_is_io ???) normalize nodelta
789[1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
790|2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1
791  [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta
792  |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2
793  ]
794]
795whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels;
796normalize nodelta #EQ destruct /2 by refl, conj/
797qed.
798
799lemma labels_of_trace_are_in_code :
800∀p,p',l_p,prog.∀st1,st2 : vm_ass_state p p'.∀t : raw_trace … (asm_operational_semantics p l_p p' prog) … st1 st2.
801∀lbl.
802mem … lbl (get_costlabels_of_trace … t) →
803mem … lbl (map … \fst … (labels_pc … (instructions p … prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)).
804#p #p' #l_p #prog #st1 #st2 #t elim t
805[ #st #lbl *
806| #st1 #st2 #st3 #l whd in ⊢ (% → ?);
807  cases st1 -st1 normalize nodelta [2: * |3: #st1]
808  cases st2 -st2 normalize nodelta [1,4,5: * |2: * #HN1 #HN2 >HN2 -HN2 |6: #st2 * #HN1 #HN2 >HN2 -HN2 |3: #st2 ]
809  [3: * #H1 #H2 #tl #IH #lbl whd in match (get_costlabels_of_trace ????);
810      #H cases(mem_append ???? H) -H [2: #H @IH //]
811      lapply(vm_step_to_eval … H2) whd in match eval_vmstate;
812      normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi #_
813      inversion(emits_labels … i)
814      [ #EQemit cases(step_emit … (vm_step_to_eval … H2)) // #x * #EQ1 #EQ2 whd in match actionlabel_to_costlabel;
815        normalize nodelta >EQ1 *
816        [2: *] #EQ destruct cases(map_mem … \fst … EQ2) #y * #H3 #EQ destruct //
817      | #f #EQemit whd in match actionlabel_to_costlabel; normalize nodelta
818        >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H2) … EQemit))
819        *
820      ]
821  |*: #tl #IH #lbl whd in match (get_costlabels_of_trace ????); * // @IH
822]
823qed.
824
825definition get_pc : ∀p,p'.vm_ass_state p p' → ℕ → option ℕ ≝
826λp,p',st,endmain.match st with
827[ STATE s ⇒ Some ? (pc … s)
828| INITIAL ⇒ None ?
829| FINAL ⇒ Some ? endmain
830].
831
832
833lemma tbase_tind_append : ∀p : label_params.∀S : abstract_status p.∀st1,st2,st3 : S.∀t : raw_trace … st1 st2.
834∀l,prf.∀t'.
835t_base … st1 = t @ t_ind … S st2 st3 st1 l prf t' → False.
836#p #S #st1 #st2 #st3 *
837[ #st #l #prf  #t' normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ]
838#s1 #s2 #s3 #l1 #prf1 #t2 #l2 #prf2 #t3 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
839qed.
840
841let rec chop (A : Type[0]) (l : list A) on l : list A ≝
842match l with
843[ nil ⇒ nil ?
844| cons x xs ⇒ match xs with [ nil ⇒ nil ? | cons _ _ ⇒ x :: chop … xs]
845].
846
847lemma chop_append_singleton : ∀A : Type[0].∀x : A.∀l : list A.chop ? (l@ [x]) = l.
848#A #x #l elim l normalize // #y * normalize //
849qed.
850
851lemma chop_mem : ∀A : Type[0].∀x : A.∀l : list A. mem … x (chop ? l) → mem … x l.
852#A #x #l elim l [*] #y * [ normalize /2/] #z #zs #IH * [/2/] /3/
853qed.
854
855(*
856definition actionlabel_to_costlabel : ActionLabel → list CostLabel ≝
857λa.match a with
858[ call_act f l ⇒ [a_call l]
859| ret_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_return_post l]]
860| cost_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_non_functional_label l]]
861].
862*)
863
864lemma get_cost_label_of_trace_tind : ∀p. ∀S : abstract_status p.
865∀st1,st2,st3 : S.∀l,prf,t.
866get_costlabels_of_trace … (t_ind … st1 st2 st3 l prf t) =
867actionlabel_to_costlabel … l @ get_costlabels_of_trace … t.
868#p #S #st1 #st2 #st3 * // qed.
869
870lemma actionlabel_ok :
871 ∀p.∀l : ActionLabel p.
872  is_costlabelled_act … l → ∃c.actionlabel_to_costlabel … l = [c].
873#p * /2/ * /2/ *
874qed.
875
876lemma i_act_in_map :  ∀p,l_p,prog,iact,l1,l2.
877mem ? 〈a_non_functional_label l_p iact,O〉 (labels_pc p l_p prog l1 l2 iact O).
878#p #l_p #instr #iact #l1 #l2 generalize in match O in ⊢ (???%); elim instr
879[ normalize /2/] #i #xs #IH #m whd in match (labels_pc ???);
880@mem_append_l2 @IH
881qed.
882
883coercion big_op : ∀M:monoid. ∀l: list M. M ≝ big_op on _l: list ? to ?.
884
885lemma static_dynamic_inv :
886(* Given an assembly program *)
887∀p,p',l_p,prog.
888
889(* Given an abstraction interpretation framework for the program *)
890∀R: asm_abstract_interpretation p p' l_p prog.
891
892(* If the static analysis does not fail *)
893∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog = return map1.
894
895(* For every pre_measurable, terminated trace *)
896∀st1,st2. ∀t: raw_trace l_p (asm_operational_semantics … prog) … st1 st2.
897 terminated_trace … t →
898
899(* Let labels be the costlabels observed in the trace (last one excluded) *)
900let labels ≝ chop … (get_costlabels_of_trace …  t) in
901
902(* Let k be the statically computed abstract action of the prefix of the trace
903   up to the first label *)
904∀k.block_cost p … prog … (instr_map … R) (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k →
905
906(* Let abs_actions be the list of statically computed abstract actions
907   associated to each label in labels. *)
908∀abs_actions.
909 abs_actions =
910  dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →
911
912(* Given an abstract state in relation with the first state of the trace *)
913∀a1.R st1 a1 →
914
915(* The final state of the trace is in relation with the one obtained by
916   first applying k to a1, and then applying every semantics in abs_trace. *)
917R st2 (〚abs_actions〛 (〚k〛 a1)).
918
919[2: @hide_prf
920    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
921    #lbl' #pc * #Hmem #EQ destruct   
922    >(proj1 … (static_analisys_ok … EQmap … Hmem))
923    @(proj2 … (static_analisys_ok … EQmap … Hmem))
924]
925#p #p' #l_p #prog #R #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 *
926#l1 * #prf1 ** #EQ destruct #Hlabelled
927>(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1))
928[2: >get_cost_label_append  >get_cost_label_of_trace_tind >append_nil cases(actionlabel_ok … Hlabelled)
929   #c #EQc >EQc // ]
930lapply Hlabelled lapply prf1 -prf1 lapply l1 -l1 elim t1 -st3
931[ * [3: #st] #l #prf #H1 #_ #k whd in ⊢ (??%? → ?);
932  [3: cases prf
933  |2: whd in ⊢ (??%% → ?); #EQ destruct #labels whd in ⊢ (??%% → ?); #EQlabels
934      #a1 #rel_fin
935      lapply(instr_map_ok … R … prf … (refl …) rel_fin) [ %|] cases st2 in prf; -st2 [3: #st2] *
936      #EQpc #EQ destruct #H >act_neutral >act_neutral normalize in H;
937      <(act_neutral … (act_abs …) a1) @H
938  | @eqb_elim normalize nodelta
939    [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #labels whd in ⊢ (??%% → ?);
940      #EQ destruct #a1 #good_st_a1>act_neutral >act_neutral whd in prf; cases st2 in prf; -st2 [3: #st2]
941      normalize nodelta * >EQpc @eqb_elim [2,4: * #ABS @⊥ @ABS %] #_ #EQ destruct
942      #EQ destruct whd in EQc : (??%%); destruct
943      lapply(instr_map_ok … R … (refl …) good_st_a1)
944      [5: @(FINAL …)
945      |2: whd % [2: % | // ]
946      | whd whd in ⊢ (??%%); @eqb_elim [2: * #ABS @⊥ @ABS assumption | #_ % ]
947      |3,4: skip]
948      whd in ⊢ (% → ?); >act_neutral #H @H
949  | #Hpc lapply prf whd in ⊢ (% → ?); cases st2 in prf; -st2 [3: #st2] #prf
950    normalize nodelta [2:* |3: * #ABS @⊥ lapply ABS -ABS @eqb_elim
951    [#EQ #_ @(absurd ? EQ Hpc) | #_ #EQ destruct ] ] * #INUTILE #H4
952    #H cases(bind_inversion ????? H) -H *
953    [ #seq * [|#lbl1]
954    | #newpc
955    | #cond #newpc #ltrue #lfalse
956    | #lin #io #lout
957    | #f
958    |
959    ]
960    * #EQfetch  lapply(vm_step_to_eval … H4) whd in match eval_vmstate in ⊢ (% → ?);
961    normalize nodelta >EQfetch >m_return_bind normalize nodelta
962    cases(asm_is_io ??) normalize nodelta
963    [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
964    |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_
965      [3: cases x normalize nodelta
966      |6: #H cases(bind_inversion ????? H) -H #y * #_
967      ]
968    ]
969    whd in ⊢ (??%% → ?); #EQ destruct [4,8: cases H1 ]
970    >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
971    whd in match (dependent_map ????); #costs #EQ destruct #a1 #good_st_a1
972    >neutral_r >act_neutral
973    lapply(instr_map_ok … l_p … R … (refl …) good_st_a1)
974    [1,7,13,19,25,31,37: whd in ⊢ (??%%); @eqb_elim normalize nodelta
975      [1,3,5,7,9,11,13: #EQ cases(absurd ? EQ Hpc) ] #_ whd in match fetch_state;
976        normalize nodelta
977        [ >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?);
978        | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?);
979        | >EQfetch in ⊢ (??%?); ] %
980      |3,9,15,21,27,33,39: skip |*: try assumption #H @H] ]]
981| -st1 * [3: #st1] #st3 #st4 #l [3: *] cases st3 -st3
982  [1,2,4,5: * #H1 #H2 #tl #_ #l1 #exe @⊥ lapply tl -tl lapply(refl ? (FINAL p p'))
983    generalize in match (FINAL ??) in ⊢ (??%? → %); #st5 #EQst5 #tl lapply EQst5
984    lapply exe lapply st2 -st2 -EQst5 elim tl
985    [ #st #st5 #ABS #EQ destruct cases ABS
986    | #s1 #s2 #s3 #l2 #H3 #tl1 #IH #s4 #_ #EQ destruct cases H3
987    ]
988  ]
989  #st3 #exe_st1_st3 #tl #IH #l1 #exe_st4_st2 #l1_lab #pre_meas #k whd in ⊢ (??%? → ?);
990  >rewrite_in_dependent_map [2,5: @get_cost_label_of_trace_tind |3,6: ]
991  >dependent_map_append
992  [ @eqb_elim [ #ABS @⊥ cases exe_st1_st3 >ABS @eqb_elim [ #_ #EQ destruct | * #ABS1 @⊥ @ABS1 %] ]
993    #Hpc normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi
994    inversion(emits_labels ??)
995    [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct #labels
996      cases(step_emit … EQi … EQemits)
997      [4: cases exe_st1_st3  #EQ #H @(vm_step_to_eval … H) |2,3:] #c * #EQc #Hc
998      whd in match actionlabel_to_costlabel; normalize nodelta
999      >rewrite_in_dependent_map [2: @EQc |3:] whd in match (dependent_map ????);
1000      @opt_safe_elim #k_c #EQk_c whd in match (dependent_map ????); letin ih_labels ≝ (dependent_map ????)
1001      #EQ destruct #a1 #good_a1 >big_op_associative >act_op @IH
1002    | #f #EQemits normalize nodelta #H cases(bind_inversion ????? H) -H #k' * #EQk' whd in ⊢ (??%% → ?);
1003      #EQ destruct(EQ) #labels cases(step_non_emit … EQi… EQemits)
1004      [4: cases exe_st1_st3  #EQ #H @(vm_step_to_eval … H) |2,3:] #EQl #EQpc
1005      >(rewrite_in_dependent_map ??? []) [2: assumption] whd in match (dependent_map ????);
1006      #EQlabels #a1 #good_a1 >act_op @IH
1007  ]
1008  try //
1009  [2: cases(static_analisys_ok … c … (pc … st3) … EQmap) // #EQ #_ <EQ whd in match (big_op ??);
1010      >neutral_l assumption
1011   |3,6: [ >neutral_r] lapply(instr_map_ok … l_p … R … (refl …) good_a1)
1012       [1,7: whd in ⊢ (??%?); @eqb_elim
1013         [1,3: #ABS cases(absurd ? ABS Hpc) ] #_ normalize nodelta whd in match fetch_state;
1014         normalize nodelta [ >EQi in ⊢ (??%?); | >EQi in ⊢ (??%?); ] %
1015       |2,8: assumption
1016       |*:
1017       ]
1018       normalize in ⊢ (% → ?); #H @H
1019  |5: whd in match get_pc; normalize nodelta >EQpc >(monotonicity_of_block_cost … EQk') //
1020  |*:  inversion pre_meas in ⊢ ?;
1021    [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
1022    |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_
1023      #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
1024    |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_
1025      #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
1026    |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct
1027      * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
1028    |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
1029    ] //
1030  ]
1031 | whd in ⊢ (??%% → ?); #EQ destruct cases exe_st1_st3 #EQpc_st3 #EQ destruct
1032   #labels whd in match actionlabel_to_costlabel; normalize nodelta
1033   whd in match (dependent_map ????); @opt_safe_elim #k_c #EQk_c letin ih_labels ≝ (dependent_map ????)
1034   change with ([?]@?) in match ([?]@?); #EQ #a1 #good_a1 destruct
1035   >big_op_associative >act_op @IH try //
1036   [  inversion pre_meas in ⊢ ?;
1037     [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
1038     |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_
1039      #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
1040     |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_
1041      #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
1042     |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct
1043      * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
1044     |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
1045     ] //
1046   |  cases(static_analisys_ok … (in_act … prog) … (pc … st3) … EQmap)
1047      [2: lapply EQpc_st3 @eqb_elim [2: #_ #EQ destruct] #EQ #_ >EQ @i_act_in_map ]
1048      #EQ #_ <EQ whd in match (big_op ??); >neutral_l assumption
1049   |  lapply(instr_map_ok … l_p …  R … (refl …) good_a1)
1050     [1: % | assumption |*:] normalize in ⊢ (% → ?); #H @H
1051   ]
1052]
1053qed.
1054
1055lemma chop_cons : ∀A : Type[0].∀x : A.∀xs: list A. xs ≠ [ ] → chop … (x :: xs) = x :: (chop … xs).
1056#A #x * [ #H cases(absurd ?? H) % ] // qed.
1057 
1058(*
1059lemma measurable_terminated:
1060 ∀S,s1,s2,s4,t. measurable S s1 s2 s4 t → terminated_trace … t.
1061 #S #s1 #s2 #s4 #t * #_ * #s3 * #t' * #l1 * #l2 * #prf1 * #prf2 ** #EQ destruct
1062 /6 width=6 by ex_intro, conj/
1063qed. *)
1064
1065lemma execute_mem_label_pc :∀p,p',l_p,prog.∀st0,st1 :vm_state p p'.∀l1,c1.
1066actionlabel_to_costlabel l_p l1 = [c1] →
1067vmstep p p' l_p prog l1 st0 st1 →
1068 mem … 〈c1,pc p p' st1〉
1069  (labels_pc … (instructions … prog) (call_label_fun … prog)
1070   (return_label_fun … prog) (in_act … prog) O).
1071#p #p' #l_p #prog #st0 #st1 #l1 #c1 #EQc1 #H lapply(vm_step_to_eval … H) -H
1072#H cases(bind_inversion ????? H); #i * #EQi #Hi cases(step_emit … EQi H)
1073[ #c2 whd in match actionlabel_to_costlabel in EQc1; normalize nodelta in EQc1;
1074  >EQc1 * #EQ destruct // ]
1075cases i in Hi;       
1076[ #seq * [|#lbl1]
1077| #newpc
1078| #cond #newpc #ltrue #lfalse
1079| #lin #io #lout
1080| #f
1081|
1082]
1083normalize nodelta cases(asm_is_io ??) normalize nodelta
1084[1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
1085|2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_
1086  [3: cases x normalize nodelta
1087  |6: #H cases(bind_inversion ????? H) -H #y *  #_
1088  ]
1089]
1090whd in ⊢ (??%% → ?); #EQ destruct try % normalize in EQc1; destruct
1091qed.
1092
1093include "Simulation.ma".
1094
1095lemma sub_trace_premeasurable_l1 : ∀p,p',l_p,prog.
1096∀s1,s2,s3. ∀t1: raw_trace l_p (asm_operational_semantics p l_p p' prog) … s1 s2.
1097∀t2 : raw_trace l_p (asm_operational_semantics p l_p p' prog) … s2 s3.
1098pre_measurable_trace … (t1 @ t2) →
1099pre_measurable_trace … t1.
1100#p #p' #l_p #prog #s1 #s2 #s3 #t1 lapply s3 -s3 elim t1
1101[ #st #st3 #t2 whd in ⊢ (?????% → ?); #H %1 @(head_of_premeasurable_is_not_io … H) ]
1102#st1 #st2 #st3 #l #exe #tl #IH #st4 #t2 #H inversion H in ⊢ ?;
1103[ #st #class #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%?%); destruct
1104| #st1' #st2' #st3' #l' #exe' #tl' #H1 #H2 #H3 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
1105  whd in EQ3 : (??%?%); destruct %2 // @IH //
1106| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 destruct
1107  whd in H13 : (??%?%); destruct %3 // @IH //
1108| #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30
1109  destruct whd in H29 : (??%?%); destruct %4 // @IH //
1110| #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46
1111  #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 destruct cases H46
1112]
1113qed.
1114
1115lemma sub_trace_premeasurable_l2 : ∀p,p',l_p,prog.
1116∀s1,s2,s3. ∀t1: raw_trace l_p (asm_operational_semantics p l_p p' prog) … s1 s2.
1117∀t2 : raw_trace l_p (asm_operational_semantics p l_p p' prog) … s2 s3.
1118pre_measurable_trace … (t1 @ t2) →
1119pre_measurable_trace … t2.
1120#p #p' #l_p #prog #s1 #s2 #s3 #t1 lapply s3 -s3 elim t1
1121[ #st #st3 #t2 whd in ⊢ (?????% → ?); #H @H ]
1122#st1 #st2 #st3 #l #exe #tl #IH #st4 #t2 #H inversion H in ⊢ ?;
1123[ #st #class #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%?%); destruct
1124| #st1' #st2' #st3' #l' #exe' #tl' #H1 #H2 #H3 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
1125  whd in EQ3 : (??%?%); destruct @IH //
1126| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 destruct
1127  whd in H13 : (??%?%); destruct @IH //
1128| #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30
1129  destruct whd in H29 : (??%?%); destruct @IH //
1130| #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46
1131  #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 destruct cases H46
1132]
1133qed.
1134
1135
1136
1137theorem static_dynamic :
1138(* Given an assembly program *)
1139∀p,p',l_p,prog.
1140
1141(* Given an abstraction interpretation framework for the program *)
1142∀R: asm_abstract_interpretation p p' l_p prog.
1143
1144(* If the static analysis does not fail *)
1145∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog = return map1.
1146
1147(* For every measurable trace whose second state is st1 or, equivalently,
1148   whose first state after the initial labelled transition is st1 *)
1149∀si,s1,s2,sn. ∀t: raw_trace l_p (asm_operational_semantics … prog) … si sn.
1150 measurable … s1 s2 … t →
1151
1152(* Let labels be the costlabels observed in the trace (last one excluded) *)
1153let labels ≝ chop … (get_costlabels_of_trace …  t) in
1154
1155(* Let abs_actions be the list of statically computed abstract actions
1156   associated to each label in labels. *)
1157∀abs_actions.
1158 abs_actions =
1159  dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →
1160
1161(* Given an abstract state in relation with the first state of the measurable
1162   fragment *)
1163∀a1.R s1 a1 →
1164
1165(* The final state of the measurable fragment is in relation with the one
1166   obtained by applying every semantics in abs_trace. *)
1167R s2 (〚abs_actions〛 a1).
1168[2: @hide_prf
1169    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
1170    #lbl' #pc * #Hmem #EQ destruct   
1171    >(proj1 … (static_analisys_ok … EQmap … Hmem))
1172    @(proj2 … (static_analisys_ok … EQmap … Hmem))
1173]
1174#p #p' #l_p #prog #R #mT #map1 #EQmap #si #s1 #s2 #sn #t #measurable
1175cases measurable #s0 * #s3 * #ti0 * #t13 * #t2n* #l1 * #l2 * #prf1 * #prf2
1176******* #pre_t13 #EQ destruct #Hl1 #Hl2 #Hcall_l2 #sil_ti0 #sil_t2n #Hcall_l1
1177#acts cases(actionlabel_ok … Hl1)
1178#c1 #EQc1 >rewrite_in_dependent_map
1179[2: >get_cost_label_append in ⊢ (??%?); >(get_cost_label_silent_is_empty … sil_ti0) in ⊢ (??%?);
1180     >get_cost_label_of_trace_tind in ⊢ (??%?); >get_cost_label_append in ⊢ (??%?);
1181      >get_cost_label_of_trace_tind in ⊢ (??%?);
1182     >(get_cost_label_silent_is_empty … sil_t2n) in ⊢ (??%?);
1183     >append_nil in ⊢ (??%?); >EQc1 in ⊢ (??%?); whd in ⊢ (??(??%)?);
1184     whd in ⊢ (??(??(???%))?); >chop_cons in ⊢ (??%?);
1185     [2: cases(actionlabel_ok … Hl2) #x #EQx >EQx cases (get_costlabels_of_trace ????)
1186        [2: #z #zs] normalize % #EQ destruct] % |3:
1187 ]
1188 whd in ⊢ (???% → ?); @opt_safe_elim #act #EQact #EQacts2 >EQacts2
1189 >(big_op_associative ? [?]) #a1 >act_op #HR
1190letin actsl ≝ (dependent_map ????);
1191@(static_dynamic_inv … EQmap … (t13 @ (t_ind … prf2 (t_base …))) … HR)
1192  [ /7 width=6 by conj, ex_intro/
1193  (*| lapply(sub_trace_premeasurable_l2 … pre_t13)
1194    change with ((t_base ? s1) @ t12) in match t12 in ⊢ (% → ?);
1195    change with ((t_ind ???????)@(t_ind ???????)) in ⊢ (????% → ?);
1196    change with ((t_ind ???????)@?) in ⊢ (????(?????%?) → ?);
1197    >append_associative #H lapply(sub_trace_premeasurable_l2 … H) -H
1198    change with ((t_base ??)@?) in ⊢ (????(??????(???????%)) → ?);
1199    change with ((t_ind ???????)@?) in ⊢ (????(??????%) → ?);
1200    <append_associative #H @(sub_trace_premeasurable_l1 … H) *)
1201  | cases s1 in prf1 t13; [3: #st1] cases s0 [3,6,9: #st0] *
1202    [2: #H #EQ lapply(refl ? (FINAL p p')) generalize in match (FINAL p p') in ⊢ (??%? → %);
1203        #st' #EQst' #tr lapply prf2 lapply EQst' -EQst' cases tr
1204        [ #st'' #EQ2 >EQ2 *
1205        | #st'' #st''' #st'''' #l3 #ABS #_ #EQ2 >EQ2 in ABS; *
1206        ]
1207    | #H1 #H2 #_ whd in match get_pc; normalize nodelta
1208      <(proj1 ?? (static_analisys_ok … EQmap …))
1209      [ normalize in ⊢ (??%%); >neutral_l @EQact
1210      |
1211      | @execute_mem_label_pc //
1212      ]
1213    | #H #EQ destruct #_ whd in match get_pc; normalize nodelta
1214      <(proj1 ?? (static_analisys_ok … EQmap …))
1215      [ normalize in ⊢ (??%%); >neutral_l @EQact
1216      |
1217      |  whd in EQc1 : (??%%); destruct lapply H @eqb_elim [2: #_ #EQ destruct] #EQ >EQ #_ @i_act_in_map
1218      ]
1219    ]
1220  | >rewrite_in_dependent_map
1221       [2: >get_cost_label_append in ⊢ (??%?); >get_cost_label_of_trace_tind in ⊢ (??%?);
1222       >append_nil in ⊢ (??%?); % |3:]
1223       %
1224   ]
1225qed.
Note: See TracBrowser for help on using the repository browser.