Context Navigation

AssemblyProofSplit.ma @ 1975

Last change on this file since 1975 was 1975, checked in by mulligan, 8 years ago
Work from today on closing main_thm.
File size: 66.4 KB

Line
1	include "ASM/AssemblyProof.ma".
2	include alias "arithmetics/nat.ma".
3	include alias "basics/logic.ma".
4
5	lemma set_arg_16_mk_Status_commutation:
6	∀M: Type[0].
7	∀cm: M.
8	∀s: PreStatus M cm.
9	∀w: Word.
10	∀d: [[dptr]].
11	set_arg_16 M cm s w d =
12	mk_PreStatus M cm
13	(low_internal_ram … s)
14	(high_internal_ram … s)
15	(external_ram … s)
16	(program_counter … s)
17	(special_function_registers_8051 … (set_arg_16 M cm s w d))
18	(special_function_registers_8052 … s)
19	(p1_latch … s)
20	(p3_latch … s)
21	(clock … s).
22	#M #cm #s #w #d
23	whd in match set_arg_16; normalize nodelta
24	whd in match set_arg_16'; normalize nodelta
25	@(subaddressing_mode_elim … [[dptr]] … [[dptr]]) [1: // ]
26	cases (split bool 8 8 w) #bu #bl normalize nodelta
27	whd in match set_8051_sfr; normalize nodelta %
28	qed.
29
30	lemma set_program_counter_mk_Status_commutation:
31	∀M: Type[0].
32	∀cm: M.
33	∀s: PreStatus M cm.
34	∀w: Word.
35	set_program_counter M cm s w =
36	mk_PreStatus M cm
37	(low_internal_ram … s)
38	(high_internal_ram … s)
39	(external_ram … s)
40	w
41	(special_function_registers_8051 … s)
42	(special_function_registers_8052 … s)
43	(p1_latch … s)
44	(p3_latch … s)
45	(clock … s).
46	//
47	qed.
48
49	lemma set_clock_mk_Status_commutation:
50	∀M: Type[0].
51	∀cm: M.
52	∀s: PreStatus M cm.
53	∀c: nat.
54	set_clock M cm s c =
55	mk_PreStatus M cm
56	(low_internal_ram … s)
57	(high_internal_ram … s)
58	(external_ram … s)
59	(program_counter … s)
60	(special_function_registers_8051 … s)
61	(special_function_registers_8052 … s)
62	(p1_latch … s)
63	(p3_latch … s)
64	c.
65	//
66	qed.
67
68	lemma get_8051_sfr_set_clock:
69	∀M: Type[0].
70	∀cm: M.
71	∀s: PreStatus M cm.
72	∀sfr: SFR8051.
73	∀t: Time.
74	get_8051_sfr M cm (set_clock M cm s t) sfr =
75	get_8051_sfr M cm s sfr.
76	#M #cm #s #sfr #t %
77	qed.
78
79	lemma special_function_registers_8051_set_arg_16:
80	∀M, M': Type[0].
81	∀cm: M.
82	∀cm': M'.
83	∀s: PreStatus M cm.
84	∀s': PreStatus M' cm'.
85	∀w, w': Word.
86	∀d, d': [[dptr]].
87	special_function_registers_8051 ?? s = special_function_registers_8051 … s' →
88	w = w' →
89	special_function_registers_8051 ?? (set_arg_16 … s w d) =
90	special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d').
91	#M #M' #cm #cm' #s #s' #w #w'
92	@list_addressing_mode_tags_elim_prop try %
93	@list_addressing_mode_tags_elim_prop try %
94	#EQ1 #EQ2 <EQ2 normalize cases (split bool 8 8 w) #b1 #b2 normalize <EQ1 %
95	qed.
96
97	lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P.
98	#P #A #a #abs destruct
99	qed.
100
101	(*
102	lemma pi1_let_commute:
103	∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c.
104	pi1 … (let 〈x1,y1〉 ≝ c in t) = (let 〈x1,y1〉 ≝ c in pi1 … t).
105	#A #B #C #P * #a #b * //
106	qed.
107
108	lemma pi1_let_as_commute:
109	∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c.
110	pi1 … (let 〈x1,y1〉 as H ≝ c in t) =
111	(let 〈x1,y1〉 as H ≝ c in pi1 … t).
112	#A #B #C #P * #a #b * //
113	qed.
114
115	lemma tech_pi1_let_as_commute:
116	∀A,B,C,P. ∀f. ∀c,c':A × B.
117	∀t: ∀a,b. 〈a,b〉=c → Σc:C.P c.
118	∀t': ∀a,b. 〈a,b〉=c' → Σc:C.P c.
119	c=c' → (∀x,y,H,H'.t x y H = f (pi1 … (t' x y H'))) →
120	pi1 … (let 〈x1,y1〉 as H ≝ c in t x1 y1 H) =
121	f (pi1 … (let 〈x1,y1〉 as H ≝ c' in t' x1 y1 H)).
122	#A #B #C #P #f * #a #b * #a' #b' #t #t' #EQ1 destruct normalize /2/
123	qed.
124	*)
125
126	include alias "arithmetics/nat.ma".
127	include alias "basics/logic.ma".
128	include alias "ASM/BitVectorTrie.ma".
129
130	lemma pair_replace:
131	∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 →
132	P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b').
133	#A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct //
134	qed.
135
136	lemma pair_as_replace:
137	∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. 〈a, b〉 = c' → T. ∀EQc: c'= c.
138	c ≃ 〈a,b〉 →
139	P (let 〈a, b〉 as H ≝ c in t a b ?) → P (let 〈a',b'〉 as H ≝ c' in t a' b' H).
140	[2:
141	>EQc assumption
142	\|1:
143	#A #B #T #P #a #b * #x #y * #x' #y' #t #H1 #H2 destruct //
144	]
145	qed.
146
147	lemma if_then_else_replace:
148	∀T: Type[0].
149	∀P: T → Prop.
150	∀t1, t2: T.
151	∀c, c', c'': bool.
152	c' = c → c ≃ c'' → P (if c'' then t1 else t2) → P (if c' then t1 else t2).
153	#T #P #t1 #t2 #c #c' #c'' #c_refl #c_refl' destruct #assm
154	assumption
155	qed.
156
157	lemma main_lemma_preinstruction:
158	∀M,M': internal_pseudo_address_map.
159	∀preamble : preamble. ∀instr_list : list labelled_instruction.
160	∀cm: pseudo_assembly_program.
161	∀EQcm: cm = 〈preamble,instr_list〉.
162	∀sigma : Word→Word. ∀policy : Word→bool.
163	∀sigma_policy_witness : sigma_policy_specification cm sigma policy.
164	∀ps : PseudoStatus cm.
165	∀ppc : Word.
166	∀EQppc : ppc=program_counter pseudo_assembly_program cm ps.
167	∀labels : label_map.
168	∀costs : BitVectorTrie costlabel 16.
169	∀create_label_cost_refl : create_label_cost_map instr_list=〈labels,costs〉.
170	∀assembled : list Byte.
171	∀costs' : BitVectorTrie costlabel 16.
172	∀assembly_refl : assembly 〈preamble,instr_list〉 sigma policy=〈assembled,costs'〉.
173	∀EQassembled : assembled=\fst (assembly cm sigma policy).
174	∀newppc : Word.
175	∀lookup_labels : Identifier→Word.
176	∀EQlookup_labels : lookup_labels = (λx:Identifier.sigma (address_of_word_labels_code_mem instr_list x)).
177	∀lookup_datalabels : identifier ASMTag→Word.
178	∀ EQlookup_datalabels : lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
179	∀EQnewppc : newppc=add 16 ppc (bitvector_of_nat 16 1).
180	∀instr: preinstruction Identifier.
181	∀ticks.
182	∀EQticks: ticks = ticks_of0 〈preamble,instr_list〉 sigma policy ppc (Instruction instr).
183	∀addr_of.
184	∀EQaddr_of: addr_of = (λx:Identifier
185	.λy:PreStatus pseudo_assembly_program cm
186	.address_of_word_labels cm x).
187	∀s.
188	∀EQs: s = (set_program_counter pseudo_assembly_program cm ps
189	(add 16 ppc (bitvector_of_nat 16 1))).
190	∀P.
191	∀EQP:
192	P = (λs.
193	execute (\|expand_relative_jump lookup_labels sigma ppc instr\|)
194	(code_memory_of_pseudo_assembly_program cm sigma
195	policy)
196	(status_of_pseudo_status M cm ps sigma policy)
197	=status_of_pseudo_status M' cm s sigma policy).
198	sigma (add 16 ppc (bitvector_of_nat 16 1))
199	=add 16 (sigma ppc)
200	(bitvector_of_nat 16
201	(\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
202	lookup_datalabels (Instruction instr))))
203	→next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr)
204	M cm ps
205	=Some internal_pseudo_address_map M'
206	→fetch_many (load_code_memory assembled)
207	(sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma ppc)
208	(expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels
209	(Instruction instr))
210	→P (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm
211	addr_of instr s).
212	#M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels
213	#costs #create_label_cost_refl #assembled #costs' #assembly_refl #EQassembled #newppc
214	#lookup_labels #EQlookup_labels #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr
215	#ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
216	#sigma_increment_commutation #maps_assm #fetch_many_assm
217	letin a ≝ Identifier letin m ≝ pseudo_assembly_program
218	cut (Σxxx:PseudoStatus cm. P (execute_1_preinstruction ticks a m cm addr_of instr s))
219	[2: * // ]
220	@(
221	let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
222	let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
223	match instr in preinstruction return λx. x = instr → Σs'.? with
224	[ ADD addr1 addr2 ⇒ λinstr_refl.
225	let s ≝ add_ticks1 s in
226	let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
227	(get_arg_8 … s false addr2) false in
228	let cy_flag ≝ get_index' ? O ? flags in
229	let ac_flag ≝ get_index' ? 1 ? flags in
230	let ov_flag ≝ get_index' ? 2 ? flags in
231	let s ≝ set_arg_8 … s ACC_A result in
232	set_flags … s cy_flag (Some Bit ac_flag) ov_flag
233	\| ADDC addr1 addr2 ⇒ λinstr_refl.
234	let s ≝ add_ticks1 s in
235	let old_cy_flag ≝ get_cy_flag ?? s in
236	let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
237	(get_arg_8 … s false addr2) old_cy_flag in
238	let cy_flag ≝ get_index' ? O ? flags in
239	let ac_flag ≝ get_index' ? 1 ? flags in
240	let ov_flag ≝ get_index' ? 2 ? flags in
241	let s ≝ set_arg_8 … s ACC_A result in
242	set_flags … s cy_flag (Some Bit ac_flag) ov_flag
243	\| SUBB addr1 addr2 ⇒ λinstr_refl.
244	let s ≝ add_ticks1 s in
245	let old_cy_flag ≝ get_cy_flag ?? s in
246	let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
247	(get_arg_8 … s false addr2) old_cy_flag in
248	let cy_flag ≝ get_index' ? O ? flags in
249	let ac_flag ≝ get_index' ? 1 ? flags in
250	let ov_flag ≝ get_index' ? 2 ? flags in
251	let s ≝ set_arg_8 … s ACC_A result in
252	set_flags … s cy_flag (Some Bit ac_flag) ov_flag
253	\| ANL addr ⇒ λinstr_refl.
254	let s ≝ add_ticks1 s in
255	match addr with
256	[ inl l ⇒
257	match l with
258	[ inl l' ⇒
259	let 〈addr1, addr2〉 ≝ l' in
260	let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
261	set_arg_8 … s addr1 and_val
262	\| inr r ⇒
263	let 〈addr1, addr2〉 ≝ r in
264	let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
265	set_arg_8 … s addr1 and_val
266	]
267	\| inr r ⇒
268	let 〈addr1, addr2〉 ≝ r in
269	let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
270	set_flags … s and_val (None ?) (get_ov_flag ?? s)
271	]
272	\| ORL addr ⇒ λinstr_refl.
273	let s ≝ add_ticks1 s in
274	match addr with
275	[ inl l ⇒
276	match l with
277	[ inl l' ⇒
278	let 〈addr1, addr2〉 ≝ l' in
279	let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
280	set_arg_8 … s addr1 or_val
281	\| inr r ⇒
282	let 〈addr1, addr2〉 ≝ r in
283	let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
284	set_arg_8 … s addr1 or_val
285	]
286	\| inr r ⇒
287	let 〈addr1, addr2〉 ≝ r in
288	let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
289	set_flags … s or_val (None ?) (get_ov_flag … s)
290	]
291	\| XRL addr ⇒ λinstr_refl.
292	let s ≝ add_ticks1 s in
293	match addr with
294	[ inl l' ⇒
295	let 〈addr1, addr2〉 ≝ l' in
296	let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
297	set_arg_8 … s addr1 xor_val
298	\| inr r ⇒
299	let 〈addr1, addr2〉 ≝ r in
300	let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
301	set_arg_8 … s addr1 xor_val
302	]
303	\| INC addr ⇒ λinstr_refl.
304	match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → Σs': PreStatus m cm. ? with
305	[ ACC_A ⇒ λacc_a: True. λEQaddr.
306	let s' ≝ add_ticks1 s in
307	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
308	set_arg_8 … s' ACC_A result
309	\| REGISTER r ⇒ λregister: True. λEQaddr.
310	let s' ≝ add_ticks1 s in
311	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
312	set_arg_8 … s' (REGISTER r) result
313	\| DIRECT d ⇒ λdirect: True. λEQaddr.
314	let s' ≝ add_ticks1 s in
315	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
316	set_arg_8 … s' (DIRECT d) result
317	\| INDIRECT i ⇒ λindirect: True. λEQaddr.
318	let s' ≝ add_ticks1 s in
319	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
320	set_arg_8 … s' (INDIRECT i) result
321	\| DPTR ⇒ λdptr: True. λEQaddr.
322	let s' ≝ add_ticks1 s in
323	let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
324	let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
325	let s ≝ set_8051_sfr … s' SFR_DPL bl in
326	set_8051_sfr … s' SFR_DPH bu
327	\| _ ⇒ λother: False. ⊥
328	] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
329	\| NOP ⇒ λinstr_refl.
330	let s ≝ add_ticks2 s in
331	s
332	\| DEC addr ⇒ λinstr_refl.
333	let s ≝ add_ticks1 s in
334	let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
335	set_arg_8 … s addr result
336	\| MUL addr1 addr2 ⇒ λinstr_refl.
337	let s ≝ add_ticks1 s in
338	let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
339	let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
340	let product ≝ acc_a_nat * acc_b_nat in
341	let ov_flag ≝ product ≥ 256 in
342	let low ≝ bitvector_of_nat 8 (product mod 256) in
343	let high ≝ bitvector_of_nat 8 (product ÷ 256) in
344	let s ≝ set_8051_sfr … s SFR_ACC_A low in
345	set_8051_sfr … s SFR_ACC_B high
346	\| DIV addr1 addr2 ⇒ λinstr_refl.
347	let s ≝ add_ticks1 s in
348	let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
349	let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
350	match acc_b_nat with
351	[ O ⇒ set_flags … s false (None Bit) true
352	\| S o ⇒
353	let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
354	let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
355	let s ≝ set_8051_sfr … s SFR_ACC_A q in
356	let s ≝ set_8051_sfr … s SFR_ACC_B r in
357	set_flags … s false (None Bit) false
358	]
359	\| DA addr ⇒ λinstr_refl.
360	let s ≝ add_ticks1 s in
361	let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
362	if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
363	let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
364	let cy_flag ≝ get_index' ? O ? flags in
365	let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
366	if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
367	let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
368	let new_acc ≝ nu @@ acc_nl' in
369	let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
370	set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
371	else
372	s
373	else
374	s
375	\| CLR addr ⇒ λinstr_refl.
376	match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
377	[ ACC_A ⇒ λacc_a: True. λEQaddr.
378	let s ≝ add_ticks1 s in
379	set_arg_8 … s ACC_A (zero 8)
380	\| CARRY ⇒ λcarry: True. λEQaddr.
381	let s ≝ add_ticks1 s in
382	set_arg_1 … s CARRY false
383	\| BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
384	let s ≝ add_ticks1 s in
385	set_arg_1 … s (BIT_ADDR b) false
386	\| _ ⇒ λother: False. ⊥
387	] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
388	\| CPL addr ⇒ λinstr_refl.
389	match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
390	[ ACC_A ⇒ λacc_a: True. λEQaddr.
391	let s ≝ add_ticks1 s in
392	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
393	let new_acc ≝ negation_bv ? old_acc in
394	set_8051_sfr … s SFR_ACC_A new_acc
395	\| CARRY ⇒ λcarry: True. λEQaddr.
396	let s ≝ add_ticks1 s in
397	let old_cy_flag ≝ get_arg_1 … s CARRY true in
398	let new_cy_flag ≝ ¬old_cy_flag in
399	set_arg_1 … s CARRY new_cy_flag
400	\| BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
401	let s ≝ add_ticks1 s in
402	let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
403	let new_bit ≝ ¬old_bit in
404	set_arg_1 … s (BIT_ADDR b) new_bit
405	\| _ ⇒ λother: False. ?
406	] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
407	\| SETB b ⇒ λinstr_refl.
408	let s ≝ add_ticks1 s in
409	set_arg_1 … s b false
410	\| RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
411	let s ≝ add_ticks1 s in
412	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
413	let new_acc ≝ rotate_left … 1 old_acc in
414	set_8051_sfr … s SFR_ACC_A new_acc
415	\| RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
416	let s ≝ add_ticks1 s in
417	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
418	let new_acc ≝ rotate_right … 1 old_acc in
419	set_8051_sfr … s SFR_ACC_A new_acc
420	\| RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
421	let s ≝ add_ticks1 s in
422	let old_cy_flag ≝ get_cy_flag ?? s in
423	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
424	let new_cy_flag ≝ get_index' ? O ? old_acc in
425	let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
426	let s ≝ set_arg_1 … s CARRY new_cy_flag in
427	set_8051_sfr … s SFR_ACC_A new_acc
428	\| RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
429	let s ≝ add_ticks1 s in
430	let old_cy_flag ≝ get_cy_flag ?? s in
431	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
432	let new_cy_flag ≝ get_index' ? 7 ? old_acc in
433	let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
434	let s ≝ set_arg_1 … s CARRY new_cy_flag in
435	set_8051_sfr … s SFR_ACC_A new_acc
436	\| SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
437	let s ≝ add_ticks1 s in
438	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
439	let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
440	let new_acc ≝ nl @@ nu in
441	set_8051_sfr … s SFR_ACC_A new_acc
442	\| PUSH addr ⇒ λinstr_refl.
443	match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → Σs': PreStatus m cm. ? with
444	[ DIRECT d ⇒ λdirect: True. λEQaddr.
445	let s ≝ add_ticks1 s in
446	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
447	let s ≝ set_8051_sfr … s SFR_SP new_sp in
448	write_at_stack_pointer … s d
449	\| _ ⇒ λother: False. ⊥
450	] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
451	\| POP addr ⇒ λinstr_refl.
452	let s ≝ add_ticks1 s in
453	let contents ≝ read_at_stack_pointer ?? s in
454	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
455	let s ≝ set_8051_sfr … s SFR_SP new_sp in
456	set_arg_8 … s addr contents
457	\| XCH addr1 addr2 ⇒ λinstr_refl.
458	let s ≝ add_ticks1 s in
459	let old_addr ≝ get_arg_8 … s false addr2 in
460	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
461	let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
462	set_arg_8 … s addr2 old_acc
463	\| XCHD addr1 addr2 ⇒ λinstr_refl.
464	let s ≝ add_ticks1 s in
465	let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
466	let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in
467	let new_acc ≝ acc_nu @@ arg_nl in
468	let new_arg ≝ arg_nu @@ acc_nl in
469	let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
470	set_arg_8 … s addr2 new_arg
471	\| RET ⇒ λinstr_refl.
472	let s ≝ add_ticks1 s in
473	let high_bits ≝ read_at_stack_pointer ?? s in
474	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
475	let s ≝ set_8051_sfr … s SFR_SP new_sp in
476	let low_bits ≝ read_at_stack_pointer ?? s in
477	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
478	let s ≝ set_8051_sfr … s SFR_SP new_sp in
479	let new_pc ≝ high_bits @@ low_bits in
480	set_program_counter … s new_pc
481	\| RETI ⇒ λinstr_refl.
482	let s ≝ add_ticks1 s in
483	let high_bits ≝ read_at_stack_pointer ?? s in
484	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
485	let s ≝ set_8051_sfr … s SFR_SP new_sp in
486	let low_bits ≝ read_at_stack_pointer ?? s in
487	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
488	let s ≝ set_8051_sfr … s SFR_SP new_sp in
489	let new_pc ≝ high_bits @@ low_bits in
490	set_program_counter … s new_pc
491	\| MOVX addr ⇒ λinstr_refl.
492	let s ≝ add_ticks1 s in
493	(* DPM: only copies --- doesn't affect I/O *)
494	match addr with
495	[ inl l ⇒
496	let 〈addr1, addr2〉 ≝ l in
497	set_arg_8 … s addr1 (get_arg_8 … s false addr2)
498	\| inr r ⇒
499	let 〈addr1, addr2〉 ≝ r in
500	set_arg_8 … s addr1 (get_arg_8 … s false addr2)
501	]
502	\| MOV addr ⇒ λinstr_refl.
503	let s ≝ add_ticks1 s in
504	match addr with
505	[ inl l ⇒
506	match l with
507	[ inl l' ⇒
508	match l' with
509	[ inl l'' ⇒
510	match l'' with
511	[ inl l''' ⇒
512	match l''' with
513	[ inl l'''' ⇒
514	let 〈addr1, addr2〉 ≝ l'''' in
515	set_arg_8 … s addr1 (get_arg_8 … s false addr2)
516	\| inr r'''' ⇒
517	let 〈addr1, addr2〉 ≝ r'''' in
518	set_arg_8 … s addr1 (get_arg_8 … s false addr2)
519	]
520	\| inr r''' ⇒
521	let 〈addr1, addr2〉 ≝ r''' in
522	set_arg_8 … s addr1 (get_arg_8 … s false addr2)
523	]
524	\| inr r'' ⇒
525	let 〈addr1, addr2〉 ≝ r'' in
526	set_arg_16 … s (get_arg_16 … s addr2) addr1
527	]
528	\| inr r ⇒
529	let 〈addr1, addr2〉 ≝ r in
530	set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
531	]
532	\| inr r ⇒
533	let 〈addr1, addr2〉 ≝ r in
534	set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
535	]
536	\| JC addr ⇒ λinstr_refl.
537	if get_cy_flag ?? s then
538	let s ≝ add_ticks1 s in
539	set_program_counter … s (addr_of addr s)
540	else
541	let s ≝ add_ticks2 s in
542	s
543	\| JNC addr ⇒ λinstr_refl.
544	if ¬(get_cy_flag ?? s) then
545	let s ≝ add_ticks1 s in
546	set_program_counter … s (addr_of addr s)
547	else
548	let s ≝ add_ticks2 s in
549	s
550	\| JB addr1 addr2 ⇒ λinstr_refl.
551	if get_arg_1 … s addr1 false then
552	let s ≝ add_ticks1 s in
553	set_program_counter … s (addr_of addr2 s)
554	else
555	let s ≝ add_ticks2 s in
556	s
557	\| JNB addr1 addr2 ⇒ λinstr_refl.
558	if ¬(get_arg_1 … s addr1 false) then
559	let s ≝ add_ticks1 s in
560	set_program_counter … s (addr_of addr2 s)
561	else
562	let s ≝ add_ticks2 s in
563	s
564	\| JBC addr1 addr2 ⇒ λinstr_refl.
565	let s ≝ set_arg_1 … s addr1 false in
566	if get_arg_1 … s addr1 false then
567	let s ≝ add_ticks1 s in
568	set_program_counter … s (addr_of addr2 s)
569	else
570	let s ≝ add_ticks2 s in
571	s
572	\| JZ addr ⇒ λinstr_refl.
573	if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
574	let s ≝ add_ticks1 s in
575	set_program_counter … s (addr_of addr s)
576	else
577	let s ≝ add_ticks2 s in
578	s
579	\| JNZ addr ⇒ λinstr_refl.
580	if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
581	let s ≝ add_ticks1 s in
582	set_program_counter … s (addr_of addr s)
583	else
584	let s ≝ add_ticks2 s in
585	s
586	\| CJNE addr1 addr2 ⇒ λinstr_refl.
587	match addr1 with
588	[ inl l ⇒
589	let 〈addr1, addr2'〉 ≝ l in
590	let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
591	(nat_of_bitvector ? (get_arg_8 … s false addr2')) in
592	if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
593	let s ≝ add_ticks1 s in
594	let s ≝ set_program_counter … s (addr_of addr2 s) in
595	set_flags … s new_cy (None ?) (get_ov_flag ?? s)
596	else
597	let s ≝ add_ticks2 s in
598	set_flags … s new_cy (None ?) (get_ov_flag ?? s)
599	\| inr r' ⇒
600	let 〈addr1, addr2'〉 ≝ r' in
601	let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
602	(nat_of_bitvector ? (get_arg_8 … s false addr2')) in
603	if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
604	let s ≝ add_ticks1 s in
605	let s ≝ set_program_counter … s (addr_of addr2 s) in
606	set_flags … s new_cy (None ?) (get_ov_flag ?? s)
607	else
608	let s ≝ add_ticks2 s in
609	set_flags … s new_cy (None ?) (get_ov_flag ?? s)
610	]
611	\| DJNZ addr1 addr2 ⇒ λinstr_refl.
612	let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
613	let s ≝ set_arg_8 … s addr1 result in
614	if ¬(eq_bv ? result (zero 8)) then
615	let s ≝ add_ticks1 s in
616	set_program_counter … s (addr_of addr2 s)
617	else
618	let s ≝ add_ticks2 s in
619	s
620	] (refl … instr))
621	try (cases(other))
622	try assumption (20s)
623	try (% @False) (6s) (* Bug exploited here to implement solve :-*)
624	try (
625	@(execute_1_technical … (subaddressing_modein …))
626	@I
627	) (66s)
628	whd in match execute_1_preinstruction; normalize nodelta
629	[4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
630	lapply (subaddressing_modein ???)
631	<EQaddr normalize nodelta #irrelevant
632	try (>p normalize nodelta)
633	try (>p1 normalize nodelta)
634	(* XXX: start work on the left hand side *)
635	>EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
636	(* XXX: work on fetch_many *)
637	<instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
638	whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
639	whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
640	<EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
641	#eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
642	>(eq_bv_eq … fetch_many_assm) -newpc
643	>(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
644	(* XXX: work on sigma commutation *)
645	<instr_refl in sigma_increment_commutation; #sigma_increment_commutation
646	(* XXX: work on ticks (of all kinds) *)
647	>EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
648	(* XXX: work on both sides *)
649	[1,2,3,4,5:
650	generalize in ⊢ (??(???(?%))?);
651	\|6,7,8,9,10,11:
652	generalize in ⊢ (??(???(?%))?);
653	\|12:
654	generalize in ⊢ (??(???(?%))?);
655	]
656	<EQaddr normalize nodelta #irrelevant
657	[1:
658	@(pair_as_replace ??? (λx. pi1 ?? x = ?) ???? (λx. λy. λ_. half_add ???) ? p)
659
660	(* XXX: removes status 's' *)
661	normalize nodelta >EQs -s -ticks
662	whd in ⊢ (??%%);
663	(* XXX: simplify the left hand side *)
664
665	(* XXX: work on both sides *)
666	\|1,2,3,9,51,53,54,55: (* ADD, ADDC, SUBB, DEC, POP, XCHD, RET, RETI *)
667	(* XXX: simplify the right hand side *)
668	>p normalize nodelta
669	try (>p1 normalize nodelta)
670	(* XXX: start work on the left hand side *)
671	>EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
672	(* XXX: work on fetch_many *)
673	<instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
674	whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
675	whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
676	<EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
677	#eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
678	>(eq_bv_eq … fetch_many_assm) -newpc
679	>(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
680	(* XXX: work on sigma commutation *)
681	<instr_refl in sigma_increment_commutation; #sigma_increment_commutation
682	(* XXX: work on ticks (of all kinds) *)
683	>EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
684	(* XXX: simplify the left hand side *)
685	@(pair_replace ?????????? p)
686	[1,3,5,7,9,11,13,15:
687	cases daemon
688	\|12,14,16:
689	normalize nodelta
690	@(pair_replace ?????????? p1)
691	[1,3,5:
692	cases daemon
693	]
694	]
695	(* XXX: removes status 's' *)
696	normalize nodelta >EQs -s -ticks
697	whd in ⊢ (??%%);
698	(* XXX: work on both sides *)
699	cases daemon (*
700	@split_eq_status try %
701	[*: whd in ⊢ (??%%); >set_clock_mk_Status_commutation
702	whd in match (set_flags ??????);
703	(* CSC: TO BE COMPLETED *)
704	] *)
705	\|10,42,43,44,45,49,52,56: (* MUL *)
706	(* XXX: simplify the right hand side *)
707	(* XXX: start work on the left hand side *)
708	>EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
709	(* XXX: work on fetch_many *)
710	<instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
711	whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
712	whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
713	<EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
714	#eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
715	>(eq_bv_eq … fetch_many_assm) -newpc
716	>(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
717	(* XXX: work on sigma commutation *)
718	<instr_refl in sigma_increment_commutation; #sigma_increment_commutation
719	(* XXX: work on ticks (of all kinds) *)
720	>EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
721	(* XXX: removes status 's' *)
722	normalize nodelta >EQs -s -ticks
723	whd in ⊢ (??%%);
724	(* XXX: work on both sides *)
725	(* @split_eq_status try % *)
726	cases daemon
727	\|11,12: (* DIV *)
728	normalize nodelta in p;
729	>p normalize nodelta
730	>EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
731	(* XXX: work on fetch_many *)
732	<instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
733	whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
734	whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
735	<EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
736	#eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
737	>(eq_bv_eq … fetch_many_assm) -newpc
738	>(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
739	(* XXX: work on sigma commutation *)
740	<instr_refl in sigma_increment_commutation; #sigma_increment_commutation
741	(* XXX: work on ticks (of all kinds) *)
742	>EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
743	(* XXX: work on both sides *)
744	@(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
745	>(?: pose_assm = 0)
746	[2,4:
747	<p >pose_refl
748	cases daemon
749	\|1,3:
750	(* XXX: removes status 's' *)
751	normalize nodelta >EQs -s -ticks
752	whd in ⊢ (??%%);
753	(* XXX: work on both sides *)
754	@split_eq_status try %
755	cases daemon
756	]
757	\|13,14,15: (* DA *)
758	>p normalize nodelta
759	>p1 normalize nodelta
760	try (>p2 normalize nodelta
761	try (>p3 normalize nodelta
762	try (>p4 normalize nodelta
763	try (>p5 normalize nodelta))))
764	>EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
765	(* XXX: work on fetch_many *)
766	<instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
767	whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
768	whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
769	<EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
770	#eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
771	>(eq_bv_eq … fetch_many_assm) -newpc
772	>(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
773	(* XXX: work on sigma commutation *)
774	<instr_refl in sigma_increment_commutation; #sigma_increment_commutation
775	(* XXX: work on ticks (of all kinds) *)
776	>EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
777	(* XXX: work on both sides *)
778	@(pair_replace ?????????? p)
779	[1,3,5:
780	cases daemon
781	\|2,4,6:
782	@(if_then_else_replace ???????? p1)
783	[1,3,5:
784	cases daemon
785	\|2,4:
786	normalize nodelta
787	@(pair_replace ?????????? p2)
788	[1,3:
789	cases daemon
790	\|2,4:
791	normalize nodelta >p3 normalize nodelta
792	>p4 normalize nodelta try >p5
793	]
794	]
795	(* XXX: removes status 's' *)
796	normalize nodelta >EQs -s -ticks
797	whd in ⊢ (??%%);
798	(* XXX: work on both sides *)
799	@split_eq_status try %
800	cases daemon
801	]
802	\|33,34,35: (* ANL, ORL, XRL *)
803	(* XXX: simplify the right hand side *)
804	[1,2,3:
805	inversion addr #addr' #EQaddr normalize nodelta
806	[1,3:
807	inversion addr' #addr'' #EQaddr' normalize nodelta
808	]
809	]
810	@pair_elim #lft #rgt #lft_rgt_refl normalize nodelta
811	(* XXX: start work on the left hand side *)
812	>EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
813	(* XXX: work on fetch_many *)
814	<instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
815	whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
816	whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
817	<EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
818	#eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
819	>(eq_bv_eq … fetch_many_assm) -newpc
820	>(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
821	(* XXX: work on sigma commutation *)
822	<instr_refl in sigma_increment_commutation; #sigma_increment_commutation
823	(* XXX: work on ticks (of all kinds) *)
824	>EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
825	(* XXX: simplify the left hand side *)
826	>EQaddr normalize nodelta try (>EQaddr' normalize nodelta)
827	>lft_rgt_refl normalize nodelta
828	(* XXX: removes status 's' *)
829	normalize nodelta >EQs -s -ticks
830	whd in ⊢ (??%%);
831	(* XXX: work on both sides *)
832	cases daemon
833	\|
834	qed.
835	(*
836
837
838	@list_addressing_mode_tags_elim_prop try % whd
839	@list_addressing_mode_tags_elim_prop try % whd #arg
840	(* XXX: we first work on sigma_increment_commutation *)
841	#sigma_increment_commutation
842	normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
843	(* XXX: we work on the maps *)
844	whd in ⊢ (??%? → ?);
845	try (change with (if ? then ? else ? = ? → ?)
846	cases (addressing_mode_ok ????? ∧ addressing_mode_ok ?????) normalize nodelta)
847	#H try @(None_Some_elim ??? H) @(Some_Some_elim ????? H) #map_refl_assm <map_refl_assm
848	(* XXX: we assume the fetch_many hypothesis *)
849	#fetch_many_assm
850	(* XXX: we give the existential *)
851	%{1}
852	whd in match (execute_1_pseudo_instruction0 ?????);
853	(* XXX: work on the left hand side of the equality *)
854	whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
855	(* XXX: execute fetches some more *)
856	whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
857	whd in fetch_many_assm;
858	>EQassembled in fetch_many_assm;
859	cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
860	#eq_instr #EQticks whd in EQticks:(???%); >EQticks
861	#fetch_many_assm whd in fetch_many_assm;
862	lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
863	>(eq_instruction_to_eq … eq_instr) -instr
864	[ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs
865	@(pose …
866	(λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy))
867	#Pl #EQPl
868	cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq
869	lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) -XX >EQlhs -lhs
870	whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%)));
871	@pair_elim
872	>tech_pi1_let_as_commute
873
874	*)
875
876
877	theorem main_thm:
878	∀M.
879	∀M'.
880	∀program: pseudo_assembly_program.
881	∀sigma: Word → Word.
882	∀policy: Word → bool.
883	∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
884	∀ps: PseudoStatus program.
885	next_internal_pseudo_address_map M program ps = Some … M' →
886	∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
887	status_of_pseudo_status M' …
888	(execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy.
889	#M #M' * #preamble #instr_list #sigma #policy #sigma_policy_witness #ps
890	change with (next_internal_pseudo_address_map0 ????? = ? → ?)
891	@(pose … (program_counter ?? ps)) #ppc #EQppc
892	generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?;
893	@pair_elim #labels #costs #create_label_cost_refl normalize nodelta
894	@pair_elim #assembled #costs' #assembly_refl normalize nodelta
895	lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
896	@pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
897	@(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
898	@(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
899	whd in match execute_1_pseudo_instruction; normalize nodelta
900	whd in match ticks_of; normalize nodelta <EQppc >fetch_pseudo_refl normalize nodelta
901	lapply (snd_fetch_pseudo_instruction instr_list ppc) >fetch_pseudo_refl #EQnewppc >EQnewppc
902	lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc pi … EQlookup_labels EQlookup_datalabels ?)
903	[1: >fetch_pseudo_refl % ]
904	#assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
905	generalize in match assm1; -assm1 -assm2 -assm3
906	normalize nodelta
907	cases pi
908	[2,3:
909	#arg
910	(* XXX: we first work on sigma_increment_commutation *)
911	#sigma_increment_commutation
912	normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
913	(* XXX: we work on the maps *)
914	whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
915	(* XXX: we assume the fetch_many hypothesis *)
916	#fetch_many_assm
917	(* XXX: we give the existential *)
918	%{0}
919	whd in match (execute_1_pseudo_instruction0 ?????);
920	(* XXX: work on the left hand side of the equality *)
921	whd in ⊢ (??%?);
922	@split_eq_status //
923	[1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (CSC: auto not working, why? ) ]
924	\|6: (* Mov *)
925	#arg1 #arg2
926	(* XXX: we first work on sigma_increment_commutation *)
927	#sigma_increment_commutation
928	normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
929	(* XXX: we work on the maps *)
930	whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
931	(* XXX: we assume the fetch_many hypothesis *)
932	#fetch_many_assm
933	(* XXX: we give the existential *)
934	%{1}
935	whd in match (execute_1_pseudo_instruction0 ?????);
936	(* XXX: work on the left hand side of the equality *)
937	whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
938	(* XXX: execute fetches some more *)
939	whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
940	whd in fetch_many_assm;
941	>EQassembled in fetch_many_assm;
942	cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
943	#eq_instr #EQticks whd in EQticks:(???%); >EQticks
944	#fetch_many_assm whd in fetch_many_assm;
945	lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
946	>(eq_instruction_to_eq … eq_instr) -instr whd in ⊢ (??%?);
947	(* XXX: now we start to work on the mk_PreStatus equality *)
948	(* XXX: lhs *)
949	change with (set_arg_16 ????? = ?)
950	>set_program_counter_mk_Status_commutation
951	>set_clock_mk_Status_commutation
952	>set_arg_16_mk_Status_commutation
953	(* XXX: rhs *)
954	change with (? = status_of_pseudo_status ?? (set_arg_16 ?????) ??)
955	>set_program_counter_mk_Status_commutation
956	>set_clock_mk_Status_commutation
957	>set_arg_16_mk_Status_commutation in ⊢ (???%);
958	(* here we are *)
959	@split_eq_status //
960	[1:
961	assumption
962	\|2:
963	@special_function_registers_8051_set_arg_16
964	[2: >EQlookup_datalabels %
965	\|1: //
966	]
967	]
968	\|1: (* Instruction *) -pi; #instr
969	@(main_lemma_preinstruction M M' preamble instr_list … (refl …) … sigma_policy_witness
970	… EQppc … create_label_cost_refl … assembly_refl EQassembled … EQlookup_labels …
971	EQlookup_datalabels EQnewppc instr … (refl …) … (refl …) … (refl …) … (refl …))
972	\|4,5: cases daemon
973	]
974	qed.
975	(*
976	*
977	[1,2,3: (* ADD, ADDC, SUBB *)
978	@list_addressing_mode_tags_elim_prop try % whd
979	@list_addressing_mode_tags_elim_prop try % whd #arg
980	(* XXX: we first work on sigma_increment_commutation *)
981	#sigma_increment_commutation
982	normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
983	(* XXX: we work on the maps *)
984	whd in ⊢ (??%? → ?);
985	try (change with (if ? then ? else ? = ? → ?)
986	cases (addressing_mode_ok ????? ∧ addressing_mode_ok ?????) normalize nodelta)
987	#H try @(None_Some_elim ??? H) @(Some_Some_elim ????? H) #map_refl_assm <map_refl_assm
988	(* XXX: we assume the fetch_many hypothesis *)
989	#fetch_many_assm
990	(* XXX: we give the existential *)
991	%{1}
992	whd in match (execute_1_pseudo_instruction0 ?????);
993	(* XXX: work on the left hand side of the equality *)
994	whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
995	(* XXX: execute fetches some more *)
996	whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
997	whd in fetch_many_assm;
998	>EQassembled in fetch_many_assm;
999	cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
1000	#eq_instr #EQticks whd in EQticks:(???%); >EQticks
1001	#fetch_many_assm whd in fetch_many_assm;
1002	lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
1003	>(eq_instruction_to_eq … eq_instr) -instr
1004	[ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs
1005	@(pose …
1006	(λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy))
1007	#Pl #EQPl
1008	cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq
1009	lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) -XX >EQlhs -lhs
1010	whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%)));
1011	@pair_elim
1012	>tech_pi1_let_as_commute
1013
1014
1015	whd in ⊢ (??%?);
1016	[ @(pose … (execute_1_preinstruction' ???????))
1017	#lhs whd in ⊢ (???% → ?); #EQlhs
1018	@(pose … (execute_1_preinstruction' ???????))
1019	#rhs whd in ⊢ (???% → ?); #EQrhs
1020
1021
1022	CSC: delirium
1023
1024	>EQlhs -EQlhs >EQrhs -EQrhs
1025	cases (add_8_with_carry ???) #bits1 #bits2 whd in ⊢ (??%%);
1026
1027	lapply (refl ? (execute_1_preinstruction' ???????));
1028	[ whd in match (execute_1_preinstruction' ???????);
1029
1030	whd in ⊢ (??%?);
1031	[ whd in ⊢ (??(???%)%);
1032	whd in match (execute_1_preinstruction' ???????);
1033	cases (add_8_with_carry ???) #bits1 #bits2 whd in ⊢ (??%?);
1034	@pair_elim #result #flags #Heq1
1035	whd in match execute_1_preinstruction'; normalize nodelta
1036	(* XXX: now we start to work on the mk_PreStatus equality *)
1037	whd in ⊢ (??%?);
1038
1039
1040
1041	[1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2
1042	(* XXX: we take up the hypotheses *)
1043	#sigma_increment_commutation #next_map_assm #fetch_many_assm
1044	(* XXX: we give the existential *)
1045	%{1}
1046	whd in match (execute_1_pseudo_instruction0 ?????);
1047	whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
1048	whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
1049	(* XXX: fetching of the instruction *)
1050	whd in fetch_many_assm;
1051	>EQassembled in fetch_many_assm;
1052	cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
1053	#eq_instr #EQticks whd in EQticks:(???%); >EQticks
1054	#fetch_many_assm whd in fetch_many_assm;
1055	lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
1056	>(eq_instruction_to_eq … eq_instr) -instr
1057	(* XXX: now we start to work on the mk_PreStatus equality *)
1058	whd in ⊢ (??%?);
1059	check execute_1_preinstruction
1060
1061
1062	#MAP #H1 #H2 #EQ %[1,3,5:@1]
1063	normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1064	change in ⊢ (? → ??%?) with (execute_1_0 ??)
1065	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1066	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
1067	>H2b >(eq_instruction_to_eq … H2a)
1068	generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
1069	@(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
1070	@(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
1071	normalize nodelta; #MAP;
1072	[1: change in ⊢ (? → %) with
1073	((let 〈result,flags〉 ≝
1074	add_8_with_carry
1075	(get_arg_8 ? ps false ACC_A)
1076	(get_arg_8 ?
1077	(set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
1078	false (DIRECT ARG2))
1079	? in ?) = ?)
1080	[2,3: %]
1081	change in ⊢ (???% → ?) with
1082	(let 〈result,flags〉 ≝ add_8_with_carry ?((get_arg_8 ? ps false ACC_A)) ?? in ?)
1083	>get_arg_8_set_clock
1084	[1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
1085	[2,4: #abs @⊥ normalize in abs; destruct (abs)
1086	\|*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
1087	[ change in ⊢ (? → %) with
1088	((let 〈result,flags〉 ≝
1089	add_8_with_carry
1090	(get_arg_8 ? ps false ACC_A)
1091	(get_arg_8 ?
1092	(set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
1093	false (DIRECT ARG2))
1094	? in ?) = ?)
1095	>get_arg_8_set_low_internal_ram
1096
1097	cases (add_8_with_carry ???)
1098
1099	[1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) \|*: cases (sub_8_with_carry ???)]
1100	#result #flags
1101	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
1102
1103
1104	\|4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?);
1105	@Some_Some_elim #MAP cases (pol ?) normalize nodelta
1106	[3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
1107	whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
1108	@pair_elim' * #instr #newppc' #ticks #EQ4
1109	* * #H2a #H2b whd in ⊢ (% → ?) #H2
1110	>H2b >(eq_instruction_to_eq … H2a)
1111	#EQ %[@1]
1112	<MAP >(eq_bv_eq … H2) >EQ
1113	whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?)
1114	cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX %
1115	whd in ⊢ (??%?)
1116	whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)
1117	cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
1118	\|5: (* Call *) #label #MAP
1119	generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
1120	whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
1121	[ (* short *) #abs @⊥ destruct (abs)
1122	\|3: (* long *) #H1 #H2 #EQ %[@1]
1123	(* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1124	change in ⊢ (? → ??%?) with (execute_1_0 ??)
1125	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1126	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
1127	>H2b >(eq_instruction_to_eq … H2a)
1128	generalize in match EQ; -EQ;
1129	whd in ⊢ (???% → ??%?);
1130	generalize in match (refl … (half_add 8 (get_8051_sfr ? ps SFR_SP) (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry #new_sp #EQ1 normalize nodelta;
1131	>(eq_bv_eq … H2c)
1132	change with
1133	((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
1134	(let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
1135	generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
1136	generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 pol newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
1137	>get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
1138	>get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
1139	generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
1140	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
1141	@split_eq_status;
1142	[ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
1143	>code_memory_write_at_stack_pointer %
1144	\| >set_program_counter_set_low_internal_ram
1145	>set_clock_set_low_internal_ram
1146	@low_internal_ram_write_at_stack_pointer
1147	[ >EQ0 @pol \| % \| %
1148	\| @( … EQ1)
1149	\| @(pair_destruct_2 … EQ2)
1150	\| >(pair_destruct_1 ????? EQpc)
1151	>(pair_destruct_2 ????? EQpc)
1152	@split_elim #x #y #H <H -x y H;
1153	>(pair_destruct_1 ????? EQppc)
1154	>(pair_destruct_2 ????? EQppc)
1155	@split_elim #x #y #H <H -x y H;
1156	>EQ0 % ]
1157	\| >set_low_internal_ram_set_high_internal_ram
1158	>set_program_counter_set_high_internal_ram
1159	>set_clock_set_high_internal_ram
1160	@high_internal_ram_write_at_stack_pointer
1161	[ >EQ0 @pol \| % \| %
1162	\| @(pair_destruct_2 … EQ1)
1163	\| @(pair_destruct_2 … EQ2)
1164	\| >(pair_destruct_1 ????? EQpc)
1165	>(pair_destruct_2 ????? EQpc)
1166	@split_elim #x #y #H <H -x y H;
1167	>(pair_destruct_1 ????? EQppc)
1168	>(pair_destruct_2 ????? EQppc)
1169	@split_elim #x #y #H <H -x y H;
1170	>EQ0 % ]
1171	\| >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
1172	>external_ram_write_at_stack_pointer whd in ⊢ (???%)
1173	>external_ram_write_at_stack_pointer whd in ⊢ (???%)
1174	>external_ram_write_at_stack_pointer %
1175	\| change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
1176	>EQ0 %
1177	\| >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
1178	>special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
1179	>special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
1180	>special_function_registers_8051_write_at_stack_pointer %
1181	\| >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
1182	>special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
1183	>special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
1184	>special_function_registers_8052_write_at_stack_pointer %
1185	\| >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
1186	>p1_latch_write_at_stack_pointer whd in ⊢ (???%)
1187	>p1_latch_write_at_stack_pointer whd in ⊢ (???%)
1188	>p1_latch_write_at_stack_pointer %
1189	\| >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
1190	>p3_latch_write_at_stack_pointer whd in ⊢ (???%)
1191	>p3_latch_write_at_stack_pointer whd in ⊢ (???%)
1192	>p3_latch_write_at_stack_pointer %
1193	\| >clock_write_at_stack_pointer whd in ⊢ (??%?)
1194	>clock_write_at_stack_pointer whd in ⊢ (???%)
1195	>clock_write_at_stack_pointer whd in ⊢ (???%)
1196	>clock_write_at_stack_pointer %]
1197	(\| ( medium *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
1198	@pair_elim' #fst_5_addr #rest_addr #EQ1
1199	@pair_elim' #fst_5_pc #rest_pc #EQ2
1200	generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
1201	cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
1202	generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
1203	change in ⊢ (? →??%?) with (execute_1_0 ??)
1204	@pair_elim' * #instr #newppc' #ticks #EQn
1205	* * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
1206	generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
1207	@pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
1208	@split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
1209	@pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
1210	change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
1211	@split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
1212	>get_8051_sfr_set_8051_sfr
1213
1214	whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
1215	change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
1216	generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
1217	cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
1218	generalize in match (refl … (split bool 4 4 pc_bu))
1219	cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
1220	generalize in match (refl … (split bool 3 8 rest_addr))
1221	cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
1222	change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
1223	generalize in match
1224	(refl …
1225	(half_add 16 (sigma 〈preamble,instr_list〉 newppc)
1226	((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
1227	cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
1228	@split_eq_status try %
1229	[ change with (? = sigma ? (address_of_word_labels ps label))
1230	(* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
1231	\| whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
1232	@(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
1233	\|4: (* Jmp *) #label #MAP
1234	generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
1235	whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
1236	[3: (* long *) #H1 #H2 #EQ %[@1]
1237	(* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1238	change in ⊢ (? → ??%?) with (execute_1_0 ??)
1239	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1240	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
1241	>H2b >(eq_instruction_to_eq … H2a)
1242	generalize in match EQ; -EQ;
1243	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
1244	cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
1245	\|1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
1246	generalize in match
1247	(refl ?
1248	(sub_16_with_carry
1249	(sigma 〈preamble,instr_list〉 pol (program_counter … ps))
1250	(sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))
1251	false))
1252	cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
1253	generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
1254	generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
1255	#EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
1256	generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1257	change in ⊢ (? → ??%?) with (execute_1_0 ??)
1258	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1259	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
1260	>H2b >(eq_instruction_to_eq … H2a)
1261	generalize in match EQ; -EQ;
1262	whd in ⊢ (???% → ?);
1263	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
1264	change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)
1265	generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))
1266	cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
1267	@split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))
1268	(* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
1269	\| (* medium *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
1270	generalize in match
1271	(refl …
1272	(split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
1273	cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
1274	generalize in match
1275	(refl …
1276	(split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
1277	cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
1278	generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
1279	cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
1280	generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
1281	change in ⊢ (? →??%?) with (execute_1_0 ??)
1282	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1283	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
1284	>H2b >(eq_instruction_to_eq … H2a)
1285	generalize in match EQ; -EQ;
1286	whd in ⊢ (???% → ?);
1287	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
1288	change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
1289	generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
1290	cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
1291	generalize in match (refl … (split bool 4 4 pc_bu))
1292	cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
1293	generalize in match (refl … (split bool 3 8 rest_addr))
1294	cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
1295	change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
1296	generalize in match
1297	(refl …
1298	(half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)
1299	((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
1300	cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
1301	@split_eq_status try %
1302	[ change with (? = sigma ?? (address_of_word_labels ps label))
1303	(* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
1304	\| whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
1305	@(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
1306	\| (* Instruction ) -pi; whd in ⊢ (? → ??%? → ?) ; normalize nodelta;
1307	[1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
1308	normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1309	change in ⊢ (? → ??%?) with (execute_1_0 ??)
1310	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1311	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
1312	>H2b >(eq_instruction_to_eq … H2a)
1313	generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
1314	@(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
1315	@(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
1316	normalize nodelta; #MAP;
1317	[1: change in ⊢ (? → %) with
1318	((let 〈result,flags〉 ≝
1319	add_8_with_carry
1320	(get_arg_8 ? ps false ACC_A)
1321	(get_arg_8 ?
1322	(set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
1323	false (DIRECT ARG2))
1324	? in ?) = ?)
1325	[2,3: %]
1326	change in ⊢ (???% → ?) with
1327	(let 〈result,flags〉 ≝ add_8_with_carry ?((get_arg_8 ? ps false ACC_A)) ?? in ?)
1328	>get_arg_8_set_clock
1329	[1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
1330	[2,4: #abs @⊥ normalize in abs; destruct (abs)
1331	\|*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
1332	[ change in ⊢ (? → %) with
1333	((let 〈result,flags〉 ≝
1334	add_8_with_carry
1335	(get_arg_8 ? ps false ACC_A)
1336	(get_arg_8 ?
1337	(set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
1338	false (DIRECT ARG2))
1339	? in ?) = ?)
1340	>get_arg_8_set_low_internal_ram
1341
1342	cases (add_8_with_carry ???)
1343
1344	[1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) \|*: cases (sub_8_with_carry ???)]
1345	#result #flags
1346	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
1347	\| (* INC *) #arg1 #H1 #H2 #EQ %[@1]
1348	normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1349	change in ⊢ (? → ??%?) with (execute_1_0 ??)
1350	cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1351	* * #H2a #H2b whd in ⊢ (% → ?) #H2c
1352	>H2b >(eq_instruction_to_eq … H2a)
1353	generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
1354	@(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
1355	[1,2,3,4: cases (half_add ???) #carry #result
1356	\| cases (half_add ???) #carry #bl normalize nodelta;
1357	cases (full_add ????) #carry' #bu normalize nodelta ]
1358	#EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';
1359	[5: %
1360	\|1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
1361	(set_program_counter pseudo_assembly_program ps newppc)
1362	(\fst (ticks_of0 〈preamble,instr_list〉
1363	(program_counter pseudo_assembly_program ps)
1364	(Instruction (INC Identifier (DIRECT ARG))))
1365	+clock pseudo_assembly_program
1366	(set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
1367	[2,3: // ]
1368	<(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
1369	whd in ⊢ (??%%)
1370	cases (split bool 4 4 ARG)
1371	#nu' #nl'
1372	normalize nodelta
1373	cases (split bool 1 3 nu')
1374	#bit_1' #ignore'
1375	normalize nodelta
1376	cases (get_index_v bool 4 nu' ? ?)
1377	[ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
1378	\|
1379	]
1380	cases daemon (* EASY CASES TO BE COMPLETED *)
1381	qed.
1382	*)

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

Download in other formats:

Original Format