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