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