source: LTS/Vm.ma @ 3673

Last change on this file since 3673 was 3591, checked in by piccolo, 4 years ago

stared pass stack to monostack, closed the first three proof obbligations of simulation conditions

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