Context Navigation

source: LTS/Vm.ma @ 3554

Last change on this file since 3554 was 3552, checked in by piccolo, 6 years ago
closed all daemons
File size: 53.2 KB

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

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format