source: LTS/Vm.ma @ 3448

Last change on this file since 3448 was 3448, checked in by piccolo, 6 years ago
File size: 16.0 KB
Line 
1include "Traces.ma".
2include "basics/lists/list.ma".
3include "../src/utilities/option.ma".
4include "basics/jmeq.ma".
5
6record monoid: Type[1] ≝
7 { carrier :> Type[0]
8 ; op: carrier → carrier → carrier
9 ; e: carrier
10 ; neutral: ∀x. op … x e = x
11 ; is_associative: ∀x,y,z. op … (op … x y) z = op … x (op … y z)
12 }.
13
14record assembler_params : Type[1] ≝
15{ seq_instr : Type[0]
16; jump_condition : Type[0]
17; io_instr : Type[0]
18; entry_of_function : FunctionName → ℕ
19; call_label_fun : list (ℕ × CallCostLabel)
20; return_label_fun : list (ℕ × ReturnPostCostLabel)
21}.
22
23inductive AssemblerInstr (p : assembler_params) : Type[0] ≝
24| Seq : seq_instr p → option (NonFunctionalLabel) →  AssemblerInstr p
25| Ijmp: ℕ → AssemblerInstr p
26| CJump : jump_condition p → ℕ → NonFunctionalLabel → NonFunctionalLabel → AssemblerInstr p
27| Iio : NonFunctionalLabel → io_instr p → NonFunctionalLabel → AssemblerInstr p
28| Icall: FunctionName → AssemblerInstr p
29| Iret: AssemblerInstr p.
30
31definition AssemblerProgram ≝λp.list (AssemblerInstr p) × ℕ.
32
33definition fetch: ∀p.AssemblerProgram p → ℕ → option (AssemblerInstr p) ≝
34 λp,l,n. nth_opt ? n (\fst l).
35
36definition stackT: Type[0] ≝ list (nat).
37
38record sem_params (p : assembler_params) : Type[1] ≝
39{ m : monoid
40; asm_store_type : Type[0]
41; eval_asm_seq : seq_instr p → asm_store_type → option asm_store_type
42; eval_asm_cond : jump_condition p → asm_store_type → option bool
43; eval_asm_io : io_instr p → asm_store_type → option asm_store_type
44; cost_of_io : io_instr p → asm_store_type → m
45; cost_of : AssemblerInstr p → m
46}.
47
48record vm_state (p : assembler_params) (p' : sem_params p) : Type[0] ≝
49{ pc : ℕ
50; asm_stack : stackT
51; asm_store : asm_store_type … p'
52; asm_is_io : bool
53; cost : m … p'
54}.
55
56definition label_of_pc ≝ λL.λl.λpc.find …
57   (λp.let 〈x,y〉 ≝ p in if eqb x pc then Some L y else None ? ) l.
58
59
60inductive vmstep (p : assembler_params) (p' : sem_params p)
61   (prog : AssemblerProgram p)  :
62      ActionLabel → relation (vm_state p p') ≝
63| vm_seq : ∀st1,st2 : vm_state p p'.∀i,l.
64           fetch … prog (pc … st1) = return (Seq p i l) →
65           asm_is_io … st1 = false →
66           eval_asm_seq p p' i (asm_store … st1) = return asm_store … st2 → 
67           asm_stack … st1 = asm_stack … st2 →
68           asm_is_io … st1 = asm_is_io … st2 →
69           S (pc … st1) = pc … st2 →
70           op … (cost … st1) (cost_of p p' (Seq p i l)) = cost … st2 →
71           vmstep … (cost_act l) st1 st2
72| vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ.
73           fetch … prog (pc … st1) = return (Ijmp p new_pc) →
74           asm_is_io … st1 = false →
75           asm_store … st1 = asm_store … st2 →
76           asm_stack … st1 = asm_stack … st2 →
77           asm_is_io … st1 = asm_is_io … st2 →
78           new_pc = pc … st2 →
79           op … (cost … st1) (cost_of p p' (Ijmp … new_pc)) = cost … st2 →
80           vmstep … (cost_act (None ?)) st1 st2
81| vm_cjump_true :
82           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
83           eval_asm_cond p p' cond (asm_store … st1) = return true→
84           fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) →
85           asm_is_io … st1 = false →
86           asm_store … st1 = asm_store … st2 →
87           asm_stack … st1 = asm_stack … st2 →
88           asm_is_io … st1 = asm_is_io … st2 →
89           pc … st2 = new_pc →
90           op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse)) = cost … st2 →
91           vmstep … (cost_act (Some ? ltrue)) st1 st2
92| vm_cjump_false :
93           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
94           eval_asm_cond p p' cond (asm_store … st1) = return false→
95           fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) →
96           asm_is_io … st1 = false →
97           asm_store … st1 = asm_store … st2 →
98           asm_stack … st1 = asm_stack … st2 →
99           asm_is_io … st1 = asm_is_io … st2 →
100           S (pc … st1) = pc … st2 →
101           op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse)) = cost … st2 →
102           vmstep … (cost_act (Some ? lfalse)) st1 st2
103| vm_io_in : 
104           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
105           fetch … prog (pc … st1) = return (Iio p lin io lout) →
106           asm_is_io … st1 = false →
107           asm_store … st1 = asm_store … st2 →
108           asm_stack … st1 = asm_stack … st2 →
109           true = asm_is_io … st2 →
110           pc … st1 = pc … st2 →
111           cost … st1 = cost … st2 →
112           vmstep … (cost_act (Some ? lin)) st1 st2
113| vm_io_out :
114           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
115           fetch … prog (pc … st1) = return (Iio p lin io lout) →
116           asm_is_io … st1 = true →
117           eval_asm_io … io (asm_store … st1) = return asm_store … st2 →
118           asm_stack … st1 = asm_stack … st2 →
119           false = asm_is_io … st2 →
120           S (pc … st1) = pc … st2 →
121           op … (cost … st1) (cost_of_io p p' io (asm_store … st1)) = cost … st2 →
122           vmstep … (cost_act (Some ? lout)) st1 st2
123| vm_call :
124           ∀st1,st2 : vm_state p p'.∀f,lbl.
125           fetch … prog (pc … st1) = return (Icall p f) →
126           asm_is_io … st1 = false →
127           asm_store … st1 = asm_store … st2 →
128           S (pc … st1) ::  asm_stack … st1 = asm_stack … st2 →
129           asm_is_io … st1 = asm_is_io … st2 →
130           entry_of_function p  f = pc … st2 →
131           op … (cost … st1) (cost_of p p' (Icall p f)) = cost … st2 →
132           label_of_pc ? (call_label_fun p) (entry_of_function p f) = return lbl →
133           vmstep … (call_act f lbl) st1 st2
134| vm_ret :
135          ∀st1,st2 : vm_state p p'.∀newpc,lbl.
136           fetch … prog (pc … st1) = return (Iret p) →
137           asm_is_io … st1 = false →
138           asm_store … st1 = asm_store … st2 →
139           asm_stack … st1 = newpc ::  asm_stack … st2  →
140           asm_is_io … st1 = asm_is_io … st2 →
141           newpc = pc … st2 →
142           label_of_pc ? (return_label_fun p) newpc = return lbl →
143           op … (cost … st1) (cost_of p p' (Iret p)) = cost … st2 →
144           vmstep … (ret_act (Some ? lbl)) st1 st2.
145           
146include "../src/utilities/hide.ma".
147
148discriminator option.
149
150definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p →  abstract_status ≝
151λp,p',prog.mk_abstract_status
152                (vm_state p p')
153                (λl.λst1,st2 : vm_state p p'.(eqb (pc ?? st1) (\snd prog)) = false ∧
154                               vmstep p p' prog l st1 st2)
155                (λ_.λ_.True)
156                (λs.match fetch … prog (pc … s) with
157                    [ Some i ⇒ match i with
158                               [ Seq _ _ ⇒ cl_other
159                               | Ijmp _ ⇒ cl_other
160                               | CJump _ _ _ _ ⇒ cl_jump
161                               | Iio _ _ _ ⇒ if asm_is_io … s then cl_io else cl_other
162                               | Icall _ ⇒ cl_other
163                               | Iret ⇒ cl_other
164                               ]
165                    | None ⇒ cl_other
166                    ]
167                )
168                (λ_.true)
169                (λs.eqb (pc ?? s) O)
170                (λs.eqb (pc … s) (\snd prog))
171                ???.
172@hide_prf cases daemon (*
173[ #s1 #s2 #l inversion(fetch ???) normalize nodelta
174  [ #_ #EQ destruct] * normalize nodelta
175  [ #seq #lbl #_
176  | #n #_
177  | #cond #newpc #ltrue #lfalse #EQfetch
178  | #lin #io #lout #_ cases (asm_is_io ??) normalize nodelta
179  | #f #_
180  | #_
181  ]
182  #EQ destruct * #_ #H inversion H in ⊢ ?;
183  [ #st1 #st2 #i #lbl #EQ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11
184  | #st1 #st2 #new_pc #EQ #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23
185  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35
186  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47
187  | #st1 #st2 #lin #io #lout #EQ #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59
188  | #st1 #st2 #lin #io #lout #EQ #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71
189  | #st1 #st2 #f #EQ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83
190  | #st1 #st2 #new_pc #EQ #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95
191  ]   
192  destruct >EQfetch in EQ; whd in ⊢ (??%% → ?); #EQ
193  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct % //
194| #s1 #s2 #l inversion(fetch ???) normalize nodelta
195  [ #_ #EQ destruct] * normalize nodelta
196  [ #seq #lbl #_
197  | #n #_
198  | #cond #newpc #ltrue #lfalse #_
199  | #lin #io #lout #EQfetch inversion (asm_is_io ??) #EQio normalize nodelta
200  | #f #_
201  | #_
202  ]
203  #EQ destruct * #_ #H inversion H in ⊢ ?;
204  [ #st1 #st2 #i #lbl #EQf #EQio1 #H2 #H3 #H4 #EQio2 #H6 #H7 #H8 #H9 #H10 #H11
205  | #st1 #st2 #new_pc #EQf #EQio1 #H13 #H14 #H15 #EQio2 #H17 #H18 #H19 #H20 #H21 #H22
206  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQf #EQio1 #H26 #H27 #H28 #EQio2 #H30 #H31 #H32 #H33 #H34 #H35
207  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQf #EQio1 #H38 #H39 #H40 #EQio2 #H42 #H43 #H44 #H45 #H46 #H47
208  | #st1 #st2 #lin #io #lout #EQf #EQio1 #H50 #H51 #H52 #EQio2 #H54 #H55 #H56 #H57 #H58 #H59
209  | #st1 #st2 #lin #io #lout #EQf #EQio1 #H61 #H62 #H63 #EQio2 #H65 #H66 #H67 #H68 #H69 #H70
210  | #st1 #st2 #f #EQf #EQio1 #H74 #H75 #H76 #EQio2 #H78 #H79 #H80 #H81 #H82 #H83
211  | #st1 #st2 #new_pc #EQf #EQio1 #H86 #H87 #H88 #EQio2 #H90 #H91 #H92 #H93 #H94 #H95
212  ]   
213  destruct >EQio in EQio2; >EQio1 #EQ destruct %{lin} //
214|  #s1 #s2 #l inversion(fetch ???) normalize nodelta
215  [ #_ #EQ destruct] * normalize nodelta
216  [ #seq #lbl #_
217  | #n #_
218  | #cond #newpc #ltrue #lfalse #EQfetch
219  | #lin #io #lout #EQfetch cases (asm_is_io ??) normalize nodelta
220  | #f #_
221  | #_
222  ]
223  #EQ destruct * #_ #H inversion H in ⊢ ?;
224  [ #st1 #st2 #i #lbl #EQ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11
225  | #st1 #st2 #new_pc #EQ #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23
226  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35
227  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47
228  | #st1 #st2 #lin1 #io1 #lout1 #EQ #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59
229  | #st1 #st2 #lin1 #io1 #lout1 #EQ #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71
230  | #st1 #st2 #f #EQ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83
231  | #st1 #st2 #new_pc #EQ #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95
232  ]   
233  destruct >EQfetch in EQ; whd in ⊢ (??%% → ?); #EQ
234  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct % //
235]*)
236qed.
237
238definition emits_labels ≝
239λp.λinstr : AssemblerInstr p.match instr with
240        [ Seq _ opt_l ⇒ match opt_l with
241                        [ None ⇒ Some ? (λpc.S pc)
242                        | Some _ ⇒ None ?
243                        ]
244        | Ijmp newpc ⇒ Some ? (λ_.newpc)
245        | _ ⇒ None ?
246        ].
247
248
249let rec block_cost (p : assembler_params) (p' : sem_params p)
250 (prog: AssemblerProgram p) (program_counter: ℕ)
251    (program_size: ℕ)
252        on program_size: option (m … p') ≝
253match program_size with
254  [ O ⇒ None ?
255  | S program_size' ⇒
256    if eqb program_counter (\snd prog) then
257       return e … (m … p')
258    else
259    ! instr ← fetch … prog program_counter;
260    ! n ← (match emits_labels … instr with
261          [ Some f ⇒ block_cost … prog (f program_counter) program_size'
262          | None ⇒ return e …
263          ]);
264    return (op … (m … p') (cost_of p p' instr) n)
265  ].
266 
267axiom initial_act : CostLabel.
268 
269record cost_map_T (dom : DeqSet) (codom : Type[0]) : Type[1] ≝
270{ map_type :> Type[0]
271; empty_map : map_type
272; get_map : map_type → dom → option codom
273; set_map : map_type → dom → codom → map_type
274; get_set_hit : ∀k,v,m.get_map (set_map m k v) k = return v
275; get_set_miss : ∀k1,k2,v,m.(k1 == k2) = false → get_map (set_map m k1 v) k2 = get_map m k2
276}.
277
278let rec labels_pc (p : assembler_params)
279(prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝
280match prog with
281[ nil ⇒ [〈initial_act,O〉] @
282        map … (λx.let〈y,z〉 ≝ x in 〈a_call z,y〉) (call_label_fun … p) @
283        map … (λx.let〈y,z〉 ≝ x in 〈a_return_post z,y〉) (return_label_fun … p)
284| cons i is ⇒
285  match i with
286  [ Seq _ opt_l ⇒ match opt_l with
287                  [ Some lbl ⇒ [〈a_non_functional_label lbl,S program_counter〉]
288                  | None ⇒ [ ]
289                  ]
290  | Ijmp _ ⇒ [ ]
291  | CJump _ newpc ltrue lfalse ⇒ [〈a_non_functional_label ltrue,newpc〉;〈a_non_functional_label lfalse,S program_counter〉]
292  | Iio lin _ lout ⇒ [〈a_non_functional_label lout,S program_counter〉]
293  | Icall f ⇒ [ ]
294  | Iret ⇒ [ ]
295  ] @ labels_pc p is (S program_counter)             
296].
297
298definition static_analisys : ∀p : assembler_params.∀ p' : sem_params p.
299∀mT : cost_map_T DEQCostLabel (m … p').AssemblerProgram p → option mT ≝
300λp,p',mT,prog.
301let 〈instrs,final〉 ≝ prog in
302let prog_size ≝ S (|instrs|) in
303m_fold Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost … prog w prog_size; 
304                               return set_map … m z k) (labels_pc … instrs O)
305      (empty_map ?? mT).
306
307(*falso: necessita di no_duplicates*)
308axiom static_analisys_ok : ∀p,p',mT,prog,lbl,pc,map.
309static_analisys p p' mT prog = return map →
310mem … 〈lbl,pc〉 (labels_pc … (\fst prog) O) →
311get_map … map lbl = block_cost … prog pc (S (|(\fst prog)|)). 
312
313include "Simulation.ma".
314
315record terminated_trace (S : abstract_status) (L_s1,R_s2) (trace: raw_trace S L_s1 R_s2)
316 : Prop ≝
317 { R_label : option ActionLabel
318 ; R_post_state : option S
319 ; R_fin_ok : match R_label with
320               [ None ⇒ bool_to_Prop (as_final … R_s2) ∧ R_post_state = None ?
321               | Some l ⇒ (is_costlabelled_act l ∨ is_unlabelled_ret_act l) ∧
322                          (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧
323                          ∃ s'.R_post_state = Some ? s' ∧ as_execute … l R_s2 s'
324               ]
325 }.
326 
327lemma bind_inversion : ∀A,B : Type[0].∀m : option A.
328∀f : A → option B.∀y : B.
329! x ← m; f x = return y →
330∃ x.(m = return x) ∧ (f x = return y).
331#A #B * [| #a] #f #y normalize #EQ [destruct]
332%{a} %{(refl …)} //
333qed.
334
335lemma static_dynamic : ∀p,p',prog,k,mT,map.
336static_analisys p p' mT prog = return map →
337∀st1,st2 : vm_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
338pre_measurable_trace … t → terminated_trace … t →
339block_cost … prog (pc … st1) (S (|(\fst prog)|)) = return k →
340op … (m … p') (cost … st1)
341 (foldr ?? (λlbl,k1.op … (opt_safe … (get_map … map lbl) ?) k1)
342     k (get_costlabels_of_trace … t)) = cost … st2.
343[2: cases daemon]
344#p #p' #prog #k #mT #map #EQmap #st1 #st2 #t elim t
345[ #st #_ ** [|#r_lab] normalize nodelta #opt_r_state
346  [ * whd in ⊢ (?% → ?); #final_st #_ whd in ⊢ (??%? → ?); >final_st
347    normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
348    >neutral %
349  | ** #H1 #H2 * #post_st * #EQ destruct * #H3 #H4 whd in ⊢ (??%? → ?);
350    >H3 normalize nodelta #H cases(bind_inversion ????? H) -H
351    #i * #EQi #H cases(bind_inversion ????? H) -H #el
352    inversion H4
353    [ #s1 #s2 #i1 * [| #lbl] #EQfetch #no_io #EQstore #EQstack #EQio #EQpc
354      #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct >EQi in EQfetch; whd in ⊢ (??%% → ?);
355      #EQ destruct whd in match emits_labels; normalize nodelta
356      [ cases H1 whd in ⊢ (% → ?); [ * |  #EQ destruct]]
357      * whd in ⊢ (??%% → ?); #EQ destruct >neutral whd in ⊢ (??%% → ?);
358      #EQ destruct whd in match (foldr ?????);
359
360
361
362
Note: See TracBrowser for help on using the repository browser.