source: LTS/Vm.ma @ 3524

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

rearrangments of lemmas, final statement in place

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