Context Navigation

AssemblyProofSplit.ma @ 2173

Last change on this file since 2173 was 2173, checked in by mulligan, 7 years ago
MUL case of main lemma nearly complete (subject to two small holes that require a lemma) using new proof strategy.
File size: 52.6 KB

Line
1	include "ASM/StatusProofsSplit.ma".
2
3	include alias "arithmetics/nat.ma".
4	include alias "basics/logic.ma".
5	include alias "ASM/BitVectorTrie.ma".
6
7	lemma fetch_many_singleton:
8	∀code_memory: BitVectorTrie Byte 16.
9	∀final_pc, start_pc: Word.
10	∀i: instruction.
11	fetch_many code_memory final_pc start_pc [i] →
12	〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory
13	start_pc.
14	#code_memory #final_pc #start_pc #i * #new_pc
15	#fetch_many_assm whd in fetch_many_assm;
16	cases (eq_bv_eq … fetch_many_assm) assumption
17	qed.
18
19	include alias "ASM/Vector.ma".
20	include "ASM/Test.ma".
21
22	lemma addressing_mode_ok_to_map_address_using_internal_pseudo_address_map:
23	∀M, cm, ps, sigma, x.
24	∀addr1: [[acc_a]].
25	addressing_mode_ok pseudo_assembly_program M cm ps addr1=true →
26	map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A x = x.
27	#M #cm #ps #sigma #x #addr1
28	@(subaddressing_mode_elim … addr1)
29	whd in ⊢ (??%? → ??%?);
30	cases (\snd M)
31	[1:
32	//
33	\|2:
34	#upper_lower #address normalize nodelta #absurd
35	destruct(absurd)
36	]
37	qed.
38
39	lemma main_lemma_preinstruction:
40	∀M, M': internal_pseudo_address_map.
41	∀preamble: preamble.
42	∀instr_list: list labelled_instruction.
43	∀cm: pseudo_assembly_program.
44	∀EQcm: cm = 〈preamble, instr_list〉.
45	∀is_well_labelled_witness: is_well_labelled_p instr_list.
46	∀sigma: Word → Word.
47	∀policy: Word → bool.
48	∀sigma_policy_witness: sigma_policy_specification cm sigma policy.
49	∀ps: PseudoStatus cm.
50	∀ppc: Word.
51	∀program_counter_in_bounds_witness: nat_of_bitvector … ppc < \|instr_list\|.
52	∀EQppc: ppc = program_counter pseudo_assembly_program cm ps.
53	∀labels: label_map.
54	∀costs: BitVectorTrie costlabel 16.
55	∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉.
56	∀newppc: Word.
57	∀lookup_labels: Identifier → Word.
58	∀EQlookup_labels: lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)).
59	∀lookup_datalabels: Identifier → Word.
60	∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
61	∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1).
62	∀instr: preinstruction Identifier.
63	∀fetch_pseudo_refl: \fst (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr.
64	∀ticks: nat × nat.
65	∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_datalabels sigma policy ppc (Instruction instr).
66	∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
67	∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x).
68	∀s: PreStatus pseudo_assembly_program cm.
69	∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))).
70	∀P: preinstruction Identifier → PseudoStatus cm → Prop.
71	∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc)
72	(bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
73	lookup_datalabels (Instruction instr)))) →
74	next_internal_pseudo_address_map0 ? cm addr_of (Instruction instr) M ps = Some internal_pseudo_address_map M' →
75	fetch_many (load_code_memory (\fst (pi1 … (assembly cm sigma policy)))) (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps))
76	(expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) →
77	∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) =
78	status_of_pseudo_status M' cm s sigma policy).
79	P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
80	(* XXX: takes about 45 minutes to type check! *)
81	#M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
82	#sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
83	#costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels
84	#lookup_datalabels #EQlookup_datalabels #EQnewppc #instr #fetch_pseudo_refl
85	#ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
86	(#sigma_increment_commutation #maps_assm #fetch_many_assm )
87	letin a ≝ Identifier letin m ≝ pseudo_assembly_program
88	cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s))
89	[2: * // ]
90	@(
91	let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
92	let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
93	match instr in preinstruction return λx. x = instr → Σs'.? with
94	[ ADD addr1 addr2 ⇒ λinstr_refl.
95	let s ≝ add_ticks1 s in
96	let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
97	(get_arg_8 … s false addr2) false in
98	let cy_flag ≝ get_index' ? O ? flags in
99	let ac_flag ≝ get_index' ? 1 ? flags in
100	let ov_flag ≝ get_index' ? 2 ? flags in
101	let s ≝ set_arg_8 … s ACC_A result in
102	set_flags … s cy_flag (Some Bit ac_flag) ov_flag
103	\| ADDC addr1 addr2 ⇒ λinstr_refl.
104	let s ≝ add_ticks1 s in
105	let old_cy_flag ≝ get_cy_flag ?? s in
106	let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
107	(get_arg_8 … s false addr2) old_cy_flag in
108	let cy_flag ≝ get_index' ? O ? flags in
109	let ac_flag ≝ get_index' ? 1 ? flags in
110	let ov_flag ≝ get_index' ? 2 ? flags in
111	let s ≝ set_arg_8 … s ACC_A result in
112	set_flags … s cy_flag (Some Bit ac_flag) ov_flag
113	\| SUBB addr1 addr2 ⇒ λinstr_refl.
114	let s ≝ add_ticks1 s in
115	let old_cy_flag ≝ get_cy_flag ?? s in
116	let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
117	(get_arg_8 … s false addr2) old_cy_flag in
118	let cy_flag ≝ get_index' ? O ? flags in
119	let ac_flag ≝ get_index' ? 1 ? flags in
120	let ov_flag ≝ get_index' ? 2 ? flags in
121	let s ≝ set_arg_8 … s ACC_A result in
122	set_flags … s cy_flag (Some Bit ac_flag) ov_flag
123	\| ANL addr ⇒ λinstr_refl.
124	let s ≝ add_ticks1 s in
125	match addr with
126	[ inl l ⇒
127	match l with
128	[ inl l' ⇒
129	let 〈addr1, addr2〉 ≝ l' in
130	let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
131	set_arg_8 … s addr1 and_val
132	\| inr r ⇒
133	let 〈addr1, addr2〉 ≝ r in
134	let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
135	set_arg_8 … s addr1 and_val
136	]
137	\| inr r ⇒
138	let 〈addr1, addr2〉 ≝ r in
139	let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
140	set_flags … s and_val (None ?) (get_ov_flag ?? s)
141	]
142	\| ORL addr ⇒ λinstr_refl.
143	let s ≝ add_ticks1 s in
144	match addr with
145	[ inl l ⇒
146	match l with
147	[ inl l' ⇒
148	let 〈addr1, addr2〉 ≝ l' in
149	let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
150	set_arg_8 … s addr1 or_val
151	\| inr r ⇒
152	let 〈addr1, addr2〉 ≝ r in
153	let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
154	set_arg_8 … s addr1 or_val
155	]
156	\| inr r ⇒
157	let 〈addr1, addr2〉 ≝ r in
158	let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
159	set_flags … s or_val (None ?) (get_ov_flag … s)
160	]
161	\| XRL addr ⇒ λinstr_refl.
162	let s ≝ add_ticks1 s in
163	match addr with
164	[ inl l' ⇒
165	let 〈addr1, addr2〉 ≝ l' in
166	let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
167	set_arg_8 … s addr1 xor_val
168	\| inr r ⇒
169	let 〈addr1, addr2〉 ≝ r in
170	let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
171	set_arg_8 … s addr1 xor_val
172	]
173	\| INC addr ⇒ λinstr_refl.
174	match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → Σs': PreStatus m cm. ? with
175	[ ACC_A ⇒ λacc_a: True. λEQaddr.
176	let s' ≝ add_ticks1 s in
177	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
178	set_arg_8 … s' ACC_A result
179	\| REGISTER r ⇒ λregister: True. λEQaddr.
180	let s' ≝ add_ticks1 s in
181	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
182	set_arg_8 … s' (REGISTER r) result
183	\| DIRECT d ⇒ λdirect: True. λEQaddr.
184	let s' ≝ add_ticks1 s in
185	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
186	set_arg_8 … s' (DIRECT d) result
187	\| INDIRECT i ⇒ λindirect: True. λEQaddr.
188	let s' ≝ add_ticks1 s in
189	let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
190	set_arg_8 … s' (INDIRECT i) result
191	\| DPTR ⇒ λdptr: True. λEQaddr.
192	let s' ≝ add_ticks1 s in
193	let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
194	let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
195	let s ≝ set_8051_sfr … s' SFR_DPL bl in
196	set_8051_sfr … s' SFR_DPH bu
197	\| _ ⇒ λother: False. ⊥
198	] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
199	\| NOP ⇒ λinstr_refl.
200	let s ≝ add_ticks2 s in
201	s
202	\| DEC addr ⇒ λinstr_refl.
203	let s ≝ add_ticks1 s in
204	let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
205	set_arg_8 … s addr result
206	\| MUL addr1 addr2 ⇒ λinstr_refl.
207	let s ≝ add_ticks1 s in
208	let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
209	let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
210	let product ≝ acc_a_nat * acc_b_nat in
211	let ov_flag ≝ product ≥ 256 in
212	let low ≝ bitvector_of_nat 8 (product mod 256) in
213	let high ≝ bitvector_of_nat 8 (product ÷ 256) in
214	let s ≝ set_8051_sfr … s SFR_ACC_A low in
215	set_8051_sfr … s SFR_ACC_B high
216	\| DIV addr1 addr2 ⇒ λinstr_refl.
217	let s ≝ add_ticks1 s in
218	let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
219	let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
220	match acc_b_nat with
221	[ O ⇒ set_flags … s false (None Bit) true
222	\| S o ⇒
223	let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
224	let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
225	let s ≝ set_8051_sfr … s SFR_ACC_A q in
226	let s ≝ set_8051_sfr … s SFR_ACC_B r in
227	set_flags … s false (None Bit) false
228	]
229	\| DA addr ⇒ λinstr_refl.
230	let s ≝ add_ticks1 s in
231	let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
232	if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
233	let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
234	let cy_flag ≝ get_index' ? O ? flags in
235	let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
236	if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
237	let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
238	let new_acc ≝ nu @@ acc_nl' in
239	let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
240	set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
241	else
242	s
243	else
244	s
245	\| CLR addr ⇒ λinstr_refl.
246	match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
247	[ ACC_A ⇒ λacc_a: True. λEQaddr.
248	let s ≝ add_ticks1 s in
249	set_arg_8 … s ACC_A (zero 8)
250	\| CARRY ⇒ λcarry: True. λEQaddr.
251	let s ≝ add_ticks1 s in
252	set_arg_1 … s CARRY false
253	\| BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
254	let s ≝ add_ticks1 s in
255	set_arg_1 … s (BIT_ADDR b) false
256	\| _ ⇒ λother: False. ⊥
257	] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
258	\| CPL addr ⇒ λinstr_refl.
259	match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
260	[ ACC_A ⇒ λacc_a: True. λEQaddr.
261	let s ≝ add_ticks1 s in
262	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
263	let new_acc ≝ negation_bv ? old_acc in
264	set_8051_sfr … s SFR_ACC_A new_acc
265	\| CARRY ⇒ λcarry: True. λEQaddr.
266	let s ≝ add_ticks1 s in
267	let old_cy_flag ≝ get_arg_1 … s CARRY true in
268	let new_cy_flag ≝ ¬old_cy_flag in
269	set_arg_1 … s CARRY new_cy_flag
270	\| BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
271	let s ≝ add_ticks1 s in
272	let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
273	let new_bit ≝ ¬old_bit in
274	set_arg_1 … s (BIT_ADDR b) new_bit
275	\| _ ⇒ λother: False. ?
276	] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
277	\| SETB b ⇒ λinstr_refl.
278	let s ≝ add_ticks1 s in
279	set_arg_1 … s b false
280	\| RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
281	let s ≝ add_ticks1 s in
282	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
283	let new_acc ≝ rotate_left … 1 old_acc in
284	set_8051_sfr … s SFR_ACC_A new_acc
285	\| RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
286	let s ≝ add_ticks1 s in
287	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
288	let new_acc ≝ rotate_right … 1 old_acc in
289	set_8051_sfr … s SFR_ACC_A new_acc
290	\| RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
291	let s ≝ add_ticks1 s in
292	let old_cy_flag ≝ get_cy_flag ?? s in
293	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
294	let new_cy_flag ≝ get_index' ? O ? old_acc in
295	let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
296	let s ≝ set_arg_1 … s CARRY new_cy_flag in
297	set_8051_sfr … s SFR_ACC_A new_acc
298	\| RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
299	let s ≝ add_ticks1 s in
300	let old_cy_flag ≝ get_cy_flag ?? s in
301	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
302	let new_cy_flag ≝ get_index' ? 7 ? old_acc in
303	let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
304	let s ≝ set_arg_1 … s CARRY new_cy_flag in
305	set_8051_sfr … s SFR_ACC_A new_acc
306	\| SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
307	let s ≝ add_ticks1 s in
308	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
309	let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
310	let new_acc ≝ nl @@ nu in
311	set_8051_sfr … s SFR_ACC_A new_acc
312	\| PUSH addr ⇒ λinstr_refl.
313	match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → Σs': PreStatus m cm. ? with
314	[ DIRECT d ⇒ λdirect: True. λEQaddr.
315	let s ≝ add_ticks1 s in
316	let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
317	let s ≝ set_8051_sfr … s SFR_SP new_sp in
318	write_at_stack_pointer … s d
319	\| _ ⇒ λother: False. ⊥
320	] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
321	\| POP addr ⇒ λinstr_refl.
322	let s ≝ add_ticks1 s in
323	let contents ≝ read_at_stack_pointer ?? s in
324	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
325	let s ≝ set_8051_sfr … s SFR_SP new_sp in
326	set_arg_8 … s addr contents
327	\| XCH addr1 addr2 ⇒ λinstr_refl.
328	let s ≝ add_ticks1 s in
329	let old_addr ≝ get_arg_8 … s false addr2 in
330	let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
331	let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
332	set_arg_8 … s addr2 old_acc
333	\| XCHD addr1 addr2 ⇒ λinstr_refl.
334	let s ≝ add_ticks1 s in
335	let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
336	let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
337	let new_acc ≝ acc_nu @@ arg_nl in
338	let new_arg ≝ arg_nu @@ acc_nl in
339	let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
340	set_arg_8 … s addr2 new_arg
341	\| RET ⇒ λinstr_refl.
342	let s ≝ add_ticks1 s in
343	let high_bits ≝ read_at_stack_pointer ?? s in
344	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
345	let s ≝ set_8051_sfr … s SFR_SP new_sp in
346	let low_bits ≝ read_at_stack_pointer ?? s in
347	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
348	let s ≝ set_8051_sfr … s SFR_SP new_sp in
349	let new_pc ≝ high_bits @@ low_bits in
350	set_program_counter … s new_pc
351	\| RETI ⇒ λinstr_refl.
352	let s ≝ add_ticks1 s in
353	let high_bits ≝ read_at_stack_pointer ?? s in
354	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
355	let s ≝ set_8051_sfr … s SFR_SP new_sp in
356	let low_bits ≝ read_at_stack_pointer ?? s in
357	let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
358	let s ≝ set_8051_sfr … s SFR_SP new_sp in
359	let new_pc ≝ high_bits @@ low_bits in
360	set_program_counter … s new_pc
361	\| MOVX addr ⇒ λinstr_refl.
362	let s ≝ add_ticks1 s in
363	(* DPM: only copies --- doesn't affect I/O *)
364	match addr with
365	[ inl l ⇒
366	let 〈addr1, addr2〉 ≝ l in
367	set_arg_8 … s addr1 (get_arg_8 … s false addr2)
368	\| inr r ⇒
369	let 〈addr1, addr2〉 ≝ r in
370	set_arg_8 … s addr1 (get_arg_8 … s false addr2)
371	]
372	\| MOV addr ⇒ λinstr_refl.
373	let s ≝ add_ticks1 s in
374	match addr with
375	[ inl l ⇒
376	match l with
377	[ inl l' ⇒
378	match l' with
379	[ inl l'' ⇒
380	match l'' with
381	[ inl l''' ⇒
382	match l''' with
383	[ inl l'''' ⇒
384	let 〈addr1, addr2〉 ≝ l'''' in
385	set_arg_8 … s addr1 (get_arg_8 … s false addr2)
386	\| inr r'''' ⇒
387	let 〈addr1, addr2〉 ≝ r'''' in
388	set_arg_8 … s addr1 (get_arg_8 … s false addr2)
389	]
390	\| inr r''' ⇒
391	let 〈addr1, addr2〉 ≝ r''' in
392	set_arg_8 … s addr1 (get_arg_8 … s false addr2)
393	]
394	\| inr r'' ⇒
395	let 〈addr1, addr2〉 ≝ r'' in
396	set_arg_16 … s (get_arg_16 … s addr2) addr1
397	]
398	\| inr r ⇒
399	let 〈addr1, addr2〉 ≝ r in
400	set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
401	]
402	\| inr r ⇒
403	let 〈addr1, addr2〉 ≝ r in
404	set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
405	]
406	\| JC addr ⇒ λinstr_refl.
407	if get_cy_flag ?? s then
408	let s ≝ add_ticks1 s in
409	set_program_counter … s (addr_of addr s)
410	else
411	let s ≝ add_ticks2 s in
412	s
413	\| JNC addr ⇒ λinstr_refl.
414	if ¬(get_cy_flag ?? s) then
415	let s ≝ add_ticks1 s in
416	set_program_counter … s (addr_of addr s)
417	else
418	let s ≝ add_ticks2 s in
419	s
420	\| JB addr1 addr2 ⇒ λinstr_refl.
421	if get_arg_1 … s addr1 false then
422	let s ≝ add_ticks1 s in
423	set_program_counter … s (addr_of addr2 s)
424	else
425	let s ≝ add_ticks2 s in
426	s
427	\| JNB addr1 addr2 ⇒ λinstr_refl.
428	if ¬(get_arg_1 … s addr1 false) then
429	let s ≝ add_ticks1 s in
430	set_program_counter … s (addr_of addr2 s)
431	else
432	let s ≝ add_ticks2 s in
433	s
434	\| JBC addr1 addr2 ⇒ λinstr_refl.
435	let s ≝ set_arg_1 … s addr1 false in
436	if get_arg_1 … s addr1 false then
437	let s ≝ add_ticks1 s in
438	set_program_counter … s (addr_of addr2 s)
439	else
440	let s ≝ add_ticks2 s in
441	s
442	\| JZ addr ⇒ λinstr_refl.
443	if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
444	let s ≝ add_ticks1 s in
445	set_program_counter … s (addr_of addr s)
446	else
447	let s ≝ add_ticks2 s in
448	s
449	\| JNZ addr ⇒ λinstr_refl.
450	if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
451	let s ≝ add_ticks1 s in
452	set_program_counter … s (addr_of addr s)
453	else
454	let s ≝ add_ticks2 s in
455	s
456	\| CJNE addr1 addr2 ⇒ λinstr_refl.
457	match addr1 with
458	[ inl l ⇒
459	let 〈addr1, addr2'〉 ≝ l in
460	let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
461	(nat_of_bitvector ? (get_arg_8 … s false addr2')) in
462	if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
463	let s ≝ add_ticks1 s in
464	let s ≝ set_program_counter … s (addr_of addr2 s) in
465	set_flags … s new_cy (None ?) (get_ov_flag ?? s)
466	else
467	let s ≝ add_ticks2 s in
468	set_flags … s new_cy (None ?) (get_ov_flag ?? s)
469	\| inr r' ⇒
470	let 〈addr1, addr2'〉 ≝ r' in
471	let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
472	(nat_of_bitvector ? (get_arg_8 … s false addr2')) in
473	if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
474	let s ≝ add_ticks1 s in
475	let s ≝ set_program_counter … s (addr_of addr2 s) in
476	set_flags … s new_cy (None ?) (get_ov_flag ?? s)
477	else
478	let s ≝ add_ticks2 s in
479	set_flags … s new_cy (None ?) (get_ov_flag ?? s)
480	]
481	\| DJNZ addr1 addr2 ⇒ λinstr_refl.
482	let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
483	let s ≝ set_arg_8 … s addr1 result in
484	if ¬(eq_bv ? result (zero 8)) then
485	let s ≝ add_ticks1 s in
486	set_program_counter … s (addr_of addr2 s)
487	else
488	let s ≝ add_ticks2 s in
489	s
490	] (refl … instr))
491	try cases other
492	try assumption (20s)
493	try (% @False) (6s) (* Bug exploited here to implement solve :-*)
494	try (@(execute_1_technical … (subaddressing_modein …)) @I) (66s)
495	whd in match execute_1_preinstruction; normalize nodelta
496
497	(* [31,32: (* DJNZ *)
498	(* XXX: work on the right hand side *)
499	>p normalize nodelta >p1 normalize nodelta
500	(* XXX: switch to the left hand side *)
501	>EQP -P normalize nodelta
502	#sigma_increment_commutation #maps_assm #fetch_many_assm
503	whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
504	<EQppc in fetch_many_assm;
505	whd in match (short_jump_cond ??);
506	@pair_elim #sj_possible #disp
507	@pair_elim #result #flags #sub16_refl
508	@pair_elim #upper #lower #vsplit_refl
509	inversion (get_index' bool ???) #get_index_refl' normalize nodelta
510	#sj_possible_pair destruct(sj_possible_pair)
511	>p1 normalize nodelta
512	[1,3:
513	>EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
514	>(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
515	normalize nodelta in ⊢ (% → ?); #fetch_many_assm
516	whd in ⊢ (??%?);
517	<(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
518	lapply maps_assm whd in ⊢ (??%? → ?);
519	inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta
520	[2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl -M'
521	(* XXX: work on the left hand side *)
522	@(pair_replace ?????????? p) normalize nodelta
523	[1,3:
524	>EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1)
525	[2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
526	>(get_arg_8_set_program_counter … true addr1)
527	[2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
528	@get_arg_8_pseudo_addressing_mode_ok assumption
529	\|2,4:
530	>p1 normalize nodelta >EQs
531	alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)".
532	>set_program_counter_status_of_pseudo_status
533	whd in ⊢ (??%%);
534	@split_eq_status
535	[1,10:
536	whd in ⊢ (??%%); >set_arg_8_set_program_counter
537	[2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
538	>low_internal_ram_set_program_counter
539	[1:
540	>low_internal_ram_set_program_counter
541	(* XXX: ??? *)
542	\|2:
543	>low_internal_ram_set_clock
544	(* XXX: ??? *)
545	]
546	\|2,11:
547	whd in ⊢ (??%%); >set_arg_8_set_program_counter
548	[2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
549	>high_internal_ram_set_program_counter
550	[1:
551	>high_internal_ram_set_program_counter
552	(* XXX: ??? *)
553	\|2:
554	>high_internal_ram_set_clock
555	(* XXX: ??? *)
556	]
557	\|3,12:
558	whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%);
559	[2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
560	>(external_ram_set_arg_8 ??? addr1)
561	[2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
562	\|4,13:
563	whd in ⊢ (??%%); >EQaddr_of normalize nodelta
564	[1:
565	>program_counter_set_program_counter
566	>set_arg_8_set_program_counter
567	[2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
568	>set_clock_set_program_counter >program_counter_set_program_counter
569	change with (add ??? = ?)
570	(* XXX: ??? *)
571	\|2:
572	>set_arg_8_set_program_counter
573	[2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
574	>program_counter_set_program_counter
575	>set_arg_8_set_program_counter
576	[2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
577	>set_clock_set_program_counter >program_counter_set_program_counter
578	>sigma_increment_commutation <EQppc
579	whd in match (assembly_1_pseudoinstruction ??????);
580	whd in match (expand_pseudo_instruction ??????);
581	(* XXX: ??? *)
582	]
583	\|5,14:
584	whd in match (special_function_registers_8051 ???);
585	[1:
586	>special_function_registers_8051_set_program_counter
587	>special_function_registers_8051_set_clock
588	>set_arg_8_set_program_counter in ⊢ (???%);
589	[2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
590	>special_function_registers_8051_set_program_counter
591	>set_arg_8_set_program_counter
592	[2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
593	>special_function_registers_8051_set_program_counter
594	@special_function_registers_8051_set_arg_8 assumption
595	\|2:
596	>special_function_registers_8051_set_clock
597	>set_arg_8_set_program_counter
598	[2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
599	>set_arg_8_set_program_counter
600	[2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
601	>special_function_registers_8051_set_program_counter
602	>special_function_registers_8051_set_program_counter
603	@special_function_registers_8051_set_arg_8 assumption
604	]
605	\|6,15:
606	whd in match (special_function_registers_8052 ???);
607	whd in match (special_function_registers_8052 ???) in ⊢ (???%);
608	[1:
609	>set_arg_8_set_program_counter
610	[2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
611	>set_arg_8_set_program_counter
612	[2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
613	>special_function_registers_8052_set_program_counter
614	>special_function_registers_8052_set_program_counter
615	@special_function_registers_8052_set_arg_8 assumption
616	\|2:
617	whd in ⊢ (??%%);
618	>special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption
619	]
620	(* XXX: we need special_function_registers_8052_set_arg_8 *)
621	\|7,16:
622	whd in match (p1_latch ???);
623	whd in match (p1_latch ???) in ⊢ (???%);
624	(* XXX: we need p1_latch_8052_set_arg_8 *)
625	\|8,17:
626	whd in match (p3_latch ???);
627	whd in match (p3_latch ???) in ⊢ (???%);
628	(* XXX: we need p3_latch_8052_set_arg_8 *)
629	\|9:
630	>clock_set_clock
631	>clock_set_program_counter in ⊢ (???%); >clock_set_clock
632	>EQticks <instr_refl @eq_f2
633	[1:
634	whd in ⊢ (??%%); whd in match (ticks_of0 ??????);
635	\|2:
636	(* XXX: we need clock_set_arg_8 *)
637	]
638	\|18:
639	]
640	]
641	(* XXX: switch to the right hand side *)
642	normalize nodelta >EQs -s >EQticks -ticks
643	cases (¬ eq_bv ???) normalize nodelta
644	whd in ⊢ (??%%);
645	(* XXX: finally, prove the equality using sigma commutation *)
646	@split_eq_status try %
647	[1,2,3,19,20,21,28,29,30:
648	cases daemon (* XXX: axioms as above *)
649	\|4,13,22,31:
650	\|5,14,23,32:
651	\|6,15,24,33:
652	\|7,16,25,34:
653	\|8,17,26,35:
654	whd in ⊢ (??%%);maps_assm
655
656	\|9,18,27,36:
657	whd in ⊢ (??%%);
658	whd in match (ticks_of_instruction ?); <instr_refl
659	cases daemon (* XXX: daemon in ticks_of0 stopping progression *)
660	]
661	\|2,4:
662	>(? : eq_v bool 9 eq_b upper (zero 9) = false)
663	[2, 4:
664	cases daemon (* XXX: !!! *)
665	]
666	normalize nodelta >EQppc
667	* @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
668	* @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
669	* @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
670	#fetch_many_assm whd in fetch_many_assm; %{2}
671	change with (execute_1 ?? = ?)
672	@(pose … (execute_1 ? (status_of_pseudo_status …)))
673	#status_after_1 #EQstatus_after_1
674	<(?: ? = status_after_1)
675	[3,6:
676	>EQstatus_after_1 in ⊢ (???%);
677	whd in ⊢ (???%);
678	[1:
679	<fetch_refl in ⊢ (???%);
680	\|2:
681	<fetch_refl in ⊢ (???%);
682	]
683	whd in ⊢ (???%);
684	@(pair_replace ?????????? p)
685	[1,3:
686	cases daemon
687	\|2,4:
688	normalize nodelta
689	whd in match (addr_of_relative ????);
690	cases (¬ eq_bv ???) normalize nodelta
691	>set_clock_mk_Status_commutation
692	whd in ⊢ (???%);
693	change with (add ???) in match (\snd (half_add ???));
694	>set_arg_8_set_program_counter in ⊢ (???%);
695	[2,4,6,8: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
696	>program_counter_set_program_counter in ⊢ (???%);
697	>(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
698	[2,4,6,8:
699	>bitvector_of_nat_sign_extension_equivalence
700	[1,3,5,7:
701	>EQintermediate_pc' %
702	\|*:
703	repeat @le_S_S @le_O_n
704	]
705	]
706	[1,3: % ]
707	]
708	\|1,4:
709	skip
710	]
711	[3,4:
712	-status_after_1
713	@(pose … (execute_1 ? (mk_PreStatus …)))
714	#status_after_1 #EQstatus_after_1
715	<(?: ? = status_after_1)
716	[3,6:
717	>EQstatus_after_1 in ⊢ (???%);
718	whd in ⊢ (???%);
719	(* XXX: matita bug with patterns across multiple goals *)
720	[1:
721	<fetch_refl'' in ⊢ (???%);
722	\|2:
723	<fetch_refl'' in ⊢ (???%);
724	]
725	[2: % \|1: whd in ⊢ (???%); % ]
726	\|1,4:
727	skip
728	]
729	-status_after_1 whd in ⊢ (??%?);
730	(* XXX: switch to the right hand side *)
731	normalize nodelta >EQs -s >EQticks -ticks
732	normalize nodelta whd in ⊢ (??%%);
733	]
734	(* XXX: finally, prove the equality using sigma commutation *)
735	@split_eq_status try %
736	whd in ⊢ (??%%);
737	cases daemon
738	]
739	\|30: (* CJNE *)
740	(* XXX: work on the right hand side *)
741	cases addr1 -addr1 #addr1 normalize nodelta
742	cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
743	(* XXX: switch to the left hand side *)
744	>EQP -P normalize nodelta
745	#sigma_increment_commutation #maps_assm #fetch_many_assm
746
747	whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
748	<EQppc in fetch_many_assm;
749	whd in match (short_jump_cond ??);
750	@pair_elim #sj_possible #disp
751	@pair_elim #result #flags #sub16_refl
752	@pair_elim #upper #lower #vsplit_refl
753	inversion (get_index' bool ???) #get_index_refl' normalize nodelta
754	#sj_possible_pair destruct(sj_possible_pair) normalize nodelta
755	[1,3:
756	>EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
757	>(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
758	normalize nodelta in ⊢ (% → ?); #fetch_many_assm
759	whd in ⊢ (??%?);
760	<(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
761	inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
762	lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
763	@(if_then_else_replace ???????? eq_bv_refl)
764	[1,3,5,7:
765	cases daemon
766	\|2,4,6,8:
767	(* XXX: switch to the right hand side *)
768	normalize nodelta >EQs -s >EQticks -ticks
769	whd in ⊢ (??%%);
770	(* XXX: finally, prove the equality using sigma commutation *)
771	@split_eq_status try %
772	[3,7,11,15:
773	whd in ⊢ (??%?);
774	[1,3:
775	cases daemon
776	\|2,4:
777	cases daemon
778	]
779	]
780	cases daemon (* XXX *)
781	]
782	\|2,4:
783	>(? : eq_v bool 9 eq_b upper (zero 9) = false)
784	[2, 4:
785	cases daemon (* XXX: !!! *)
786	]
787	normalize nodelta >EQppc
788	* @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
789	* @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
790	* @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
791	#fetch_many_assm whd in fetch_many_assm; %{2}
792	change with (execute_1 ?? = ?)
793	@(pose … (execute_1 ? (status_of_pseudo_status …)))
794	#status_after_1 #EQstatus_after_1
795	<(?: ? = status_after_1)
796	[2,5:
797	inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
798	\|3,6:
799	>EQstatus_after_1 in ⊢ (???%);
800	whd in ⊢ (???%);
801	[1: <fetch_refl in ⊢ (???%);
802	\|2: <fetch_refl in ⊢ (???%);
803	]
804	whd in ⊢ (???%);
805	inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
806	whd in ⊢ (???%);
807	whd in match (addr_of_relative ????);
808	change with (add ???) in match (\snd (half_add ???));
809	>set_clock_set_program_counter in ⊢ (???%);
810	>program_counter_set_program_counter in ⊢ (???%);
811	>(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
812	[2,4,6,8:
813	>bitvector_of_nat_sign_extension_equivalence
814	[1,3,5,7:
815	>EQintermediate_pc' %
816	\|*:
817	repeat @le_S_S @le_O_n
818	]
819	\|1,5:
820	%
821	]
822	\|1,4: skip
823	]
824	[1,2,3,4:
825	-status_after_1
826	@(pose … (execute_1 ? (mk_PreStatus …)))
827	#status_after_1 #EQstatus_after_1
828	<(?: ? = status_after_1)
829	[3,6,9,12:
830	>EQstatus_after_1 in ⊢ (???%);
831	whd in ⊢ (???%);
832	(* XXX: matita bug with patterns across multiple goals *)
833	[1: <fetch_refl'' in ⊢ (???%);
834	\|2: <fetch_refl'' in ⊢ (???%);
835	\|3: <fetch_refl'' in ⊢ (???%);
836	\|4: <fetch_refl'' in ⊢ (???%);
837	] %
838	\|1,4,7,10:
839	skip
840	]
841	-status_after_1 whd in ⊢ (??%?);
842	(* XXX: switch to the right hand side *)
843	normalize nodelta >EQs -s >EQticks -ticks
844	whd in ⊢ (??%%);
845	]
846	(* XXX: finally, prove the equality using sigma commutation *)
847	@split_eq_status try %
848	cases daemon
849	]
850	\|17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
851	(* XXX: work on the right hand side *)
852	>p normalize nodelta
853	(* XXX: switch to the left hand side *)
854	>EQP -P normalize nodelta
855	#sigma_increment_commutation #maps_assm #fetch_many_assm
856
857	whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
858	<EQppc in fetch_many_assm;
859	whd in match (short_jump_cond ??);
860	@pair_elim #sj_possible #disp
861	@pair_elim #result #flags #sub16_refl
862	@pair_elim #upper #lower #vsplit_refl
863	inversion (get_index' bool ???) #get_index_refl' normalize nodelta
864	#sj_possible_pair destruct(sj_possible_pair) normalize nodelta
865	[1,3,5,7,9,11,13,15,17,19,21,23,25,27:
866	>EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
867	>(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
868	normalize nodelta in ⊢ (% → ?); #fetch_many_assm
869	whd in ⊢ (??%?);
870	<(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
871	(* XXX: work on the left hand side *)
872	@(if_then_else_replace ???????? p) normalize nodelta
873	[1,3,5,7,9,11,13,15,17,19,21,23,25,27:
874	cases daemon
875	]
876	(* XXX: switch to the right hand side *)
877	normalize nodelta >EQs -s >EQticks -ticks
878	whd in ⊢ (??%%);
879	(* XXX: finally, prove the equality using sigma commutation *)
880	@split_eq_status try %
881	cases daemon
882	\|2,4,6,8,10,12,14,16,18,20,22,24,26,28:
883	>(? : eq_v bool 9 eq_b upper (zero 9) = false)
884	[2,4,6,8,10,12,14,16,18,20,22,24,26,28:
885	cases daemon (* XXX: !!! *)
886	]
887	normalize nodelta >EQppc
888	* @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
889	* @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
890	* @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
891	#fetch_many_assm whd in fetch_many_assm; %{2}
892	change with (execute_1 ?? = ?)
893	@(pose … (execute_1 ? (status_of_pseudo_status …)))
894	#status_after_1 #EQstatus_after_1
895	<(?: ? = status_after_1)
896	[3,6,9,12,15,18,21,24,27,30,33,36,39,42:
897	>EQstatus_after_1 in ⊢ (???%);
898	whd in ⊢ (???%);
899	[1: <fetch_refl in ⊢ (???%);
900	\|2: <fetch_refl in ⊢ (???%);
901	\|3: <fetch_refl in ⊢ (???%);
902	\|4: <fetch_refl in ⊢ (???%);
903	\|5: <fetch_refl in ⊢ (???%);
904	\|6: <fetch_refl in ⊢ (???%);
905	\|7: <fetch_refl in ⊢ (???%);
906	\|8: <fetch_refl in ⊢ (???%);
907	\|9: <fetch_refl in ⊢ (???%);
908	\|10: <fetch_refl in ⊢ (???%);
909	\|11: <fetch_refl in ⊢ (???%);
910	\|12: <fetch_refl in ⊢ (???%);
911	\|13: <fetch_refl in ⊢ (???%);
912	\|14: <fetch_refl in ⊢ (???%);
913	]
914	whd in ⊢ (???%);
915	@(if_then_else_replace ???????? p)
916	[1,3,5,7,9,11,13,15,17,19,21,23,25,27:
917	cases daemon
918	\|2,4,6,8,10,12,14,16,18,20,22,24,26,28:
919	normalize nodelta
920	whd in match (addr_of_relative ????);
921	>set_clock_mk_Status_commutation
922	[9,10:
923	(* XXX: demodulation not working in this case *)
924	>program_counter_set_arg_1 in ⊢ (???%);
925	>program_counter_set_program_counter in ⊢ (???%);
926	\|*:
927	/demod/
928	]
929	whd in ⊢ (???%);
930	change with (add ???) in match (\snd (half_add ???));
931	>(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
932	[2,4,6,8,10,12,14,16,18,20,22,24,26,28:
933	>bitvector_of_nat_sign_extension_equivalence
934	[1,3,5,7,9,11,13,15,17,19,21,23,25,27:
935	>EQintermediate_pc' %
936	\|*:
937	repeat @le_S_S @le_O_n
938	]
939	]
940	%
941	]
942	\|1,4,7,10,13,16,19,22,25,28,31,34,37,40:
943	skip
944	]
945	-status_after_1
946	@(pose … (execute_1 ? (mk_PreStatus …)))
947	#status_after_1 #EQstatus_after_1
948	<(?: ? = status_after_1)
949	[3,6,9,12,15,18,21,24,27,30,33,36,39,42:
950	>EQstatus_after_1 in ⊢ (???%);
951	whd in ⊢ (???%);
952	(* XXX: matita bug with patterns across multiple goals *)
953	[1: <fetch_refl'' in ⊢ (???%);
954	\|2: <fetch_refl' in ⊢ (???%);
955	\|3: <fetch_refl'' in ⊢ (???%);
956	\|4: <fetch_refl' in ⊢ (???%);
957	\|5: <fetch_refl'' in ⊢ (???%);
958	\|6: <fetch_refl' in ⊢ (???%);
959	\|7: <fetch_refl'' in ⊢ (???%);
960	\|8: <fetch_refl' in ⊢ (???%);
961	\|9: <fetch_refl'' in ⊢ (???%);
962	\|10: <fetch_refl' in ⊢ (???%);
963	\|11: <fetch_refl'' in ⊢ (???%);
964	\|12: <fetch_refl' in ⊢ (???%);
965	\|13: <fetch_refl'' in ⊢ (???%);
966	\|14: <fetch_refl' in ⊢ (???%);
967	]
968	whd in ⊢ (???%);
969	[9,10:
970	\|*:
971	/demod/
972	] %
973	\|1,4,7,10,13,16,19,22,25,28,31,34,37,40:
974	skip
975	]
976	-status_after_1 whd in ⊢ (??%?);
977	(* XXX: switch to the right hand side *)
978	normalize nodelta >EQs -s >EQticks -ticks
979	whd in ⊢ (??%%);
980	(* XXX: finally, prove the equality using sigma commutation *)
981	@split_eq_status try %
982	[3,11,19,27,36,53,61:
983	>program_counter_set_program_counter >set_clock_mk_Status_commutation
984	[5: >program_counter_set_program_counter ]
985	>EQaddr_of normalize nodelta
986	whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
987	>EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
988	@eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉)
989	>create_label_cost_refl normalize nodelta #relevant @relevant
990	whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr))
991	try assumption whd in match instruction_has_label; normalize nodelta
992	<instr_refl normalize nodelta %
993	\|7,15,23,31,45,57,65:
994	>set_clock_mk_Status_commutation >program_counter_set_program_counter
995	whd in ⊢ (??%?); normalize nodelta
996	>EQppc in fetch_many_assm; #fetch_many_assm
997	[5:
998	>program_counter_set_arg_1 >program_counter_set_program_counter
999	]
1000	<(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
1001	<bitvector_of_nat_sign_extension_equivalence
1002	[1,3,5,7,9,11,13:
1003	whd in ⊢ (???%); cases (half_add ???) normalize //
1004	\|2,4,6,8,10,12,14:
1005	@assembly1_lt_128
1006	@le_S_S @le_O_n
1007	]
1008	\|*:
1009	cases daemon
1010	]
1011	]
1012	\|4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
1013	(* XXX: work on the right hand side *)
1014	lapply (subaddressing_modein ???)
1015	<EQaddr normalize nodelta #irrelevant
1016	try (>p normalize nodelta)
1017	try (>p1 normalize nodelta)
1018	(* XXX: switch to the left hand side *)
1019	>EQP -P normalize nodelta
1020	#sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1021	whd in ⊢ (??%?);
1022	whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1023	<(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1024	(* XXX: work on the left hand side *)
1025	[1,2,3,4,5:
1026	generalize in ⊢ (??(???(?%))?);
1027	\|6,7,8,9,10,11:
1028	generalize in ⊢ (??(???(?%))?);
1029	\|12:
1030	generalize in ⊢ (??(???(?%))?);
1031	]
1032	<EQaddr normalize nodelta #irrelevant
1033	try @(jmpair_as_replace ?????????? p)
1034	[10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
1035	(* XXX: switch to the right hand side *)
1036	normalize nodelta >EQs -s >EQticks -ticks
1037	whd in ⊢ (??%%);
1038	(* XXX: finally, prove the equality using sigma commutation *)
1039	try @split_eq_status try % whd in ⊢ (??%%);
1040	cases daemon
1041	\|1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI *)
1042	(* XXX: work on the right hand side *)
1043	>p normalize nodelta
1044	try (>p1 normalize nodelta)
1045	(* XXX: switch to the left hand side *)
1046	-instr_refl >EQP -P normalize nodelta
1047	#sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1048	whd in ⊢ (??%?);
1049	<(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1050	(* XXX: work on the left hand side *)
1051	@(pair_replace ?????????? p)
1052	[1,3,5,7,9,11,13,15,17:
1053	>set_clock_set_program_counter >set_clock_mk_Status_commutation
1054	>set_program_counter_mk_Status_commutation >clock_set_program_counter
1055	cases daemon
1056	\|14,16,18:
1057	normalize nodelta
1058	@(pair_replace ?????????? p1)
1059	[1,3,5:
1060	>set_clock_mk_Status_commutation
1061	cases daemon
1062	]
1063	]
1064	(* XXX: switch to the right hand side *)
1065	normalize nodelta >EQs -s >EQticks -ticks
1066	whd in ⊢ (??%%);
1067	(* XXX: finally, prove the equality using sigma commutation *)
1068	try @split_eq_status try %
1069	cases daemon *)
1070	[42,43,44,45,49,52,56:
1071	\|10: (* MUL *)
1072	(* XXX: work on the right hand side *)
1073	(* XXX: switch to the left hand side *)
1074	>EQP -P normalize nodelta
1075	#sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1076	whd in maps_assm:(??%%);
1077	inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1078	[2: normalize nodelta #absurd destruct(absurd) ]
1079	inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1080	[2: normalize nodelta #absurd destruct(absurd) ]
1081	normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1082	whd in ⊢ (??%?);
1083	<(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1084	change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
1085	[2:
1086	whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f
1087	@sym_eq
1088	[1:
1089	@(get_8051_sfr_status_of_pseudo_status … policy)
1090	cases daemon (* XXX: need a lemma *)
1091	\|2:
1092	@(get_8051_sfr_status_of_pseudo_status M' … policy)
1093	@sym_eq @set_clock_status_of_pseudo_status [2: % ]
1094	@sym_eq @set_program_counter_status_of_pseudo_status %
1095	]
1096	]
1097	@sym_eq @set_8051_sfr_status_of_pseudo_status
1098	[2:
1099	>(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
1100	@eq_f @eq_f2 try % @eq_f2 @eq_f
1101	@sym_eq
1102	[1:
1103	@(get_8051_sfr_status_of_pseudo_status … policy)
1104	cases daemon (* XXX: needs a lemma *)
1105	\|2:
1106	@(get_8051_sfr_status_of_pseudo_status M' … policy)
1107	@sym_eq @set_clock_status_of_pseudo_status [2: % ]
1108	@sym_eq @set_program_counter_status_of_pseudo_status %
1109	]
1110	]
1111	@sym_eq @set_clock_status_of_pseudo_status
1112	[2:
1113	@eq_f %
1114	]
1115	@sym_eq @set_program_counter_status_of_pseudo_status %
1116
1117	(* XXX: work on the left hand side *)
1118	(* XXX: switch to the right hand side *)
1119	normalize nodelta >EQs -s >EQticks -ticks
1120	whd in ⊢ (??%%);
1121	(* XXX: finally, prove the equality using sigma commutation *)
1122	cases daemon
1123	\|11,12: (* DIV *)
1124	(* XXX: work on the right hand side *)
1125	normalize nodelta in p;
1126	>p normalize nodelta
1127	(* XXX: switch to the left hand side *)
1128	-instr_refl >EQP -P normalize nodelta
1129	#sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1130	whd in ⊢ (??%?);
1131	<(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1132	@(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
1133	>(?: pose_assm = 0) normalize nodelta
1134	[2,4:
1135	<p >pose_refl
1136	cases daemon
1137	\|1,3:
1138	(* XXX: switch to the right hand side *)
1139	>EQs -s >EQticks -ticks
1140	whd in ⊢ (??%%);
1141	(* XXX: finally, prove the equality using sigma commutation *)
1142	@split_eq_status try %
1143	cases daemon
1144	]
1145	\|13,14,15: (* DA *)
1146	(* XXX: work on the right hand side *)
1147	>p normalize nodelta
1148	>p1 normalize nodelta
1149	try (>p2 normalize nodelta
1150	try (>p3 normalize nodelta
1151	try (>p4 normalize nodelta
1152	try (>p5 normalize nodelta))))
1153	(* XXX: switch to the left hand side *)
1154	-instr_refl >EQP -P normalize nodelta
1155	#sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1156	whd in ⊢ (??%?);
1157	<(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1158	(* XXX: work on the left hand side *)
1159	@(pair_replace ?????????? p)
1160	[1,3,5:
1161	/demod/
1162	cases daemon
1163	\|2,4,6:
1164	@(if_then_else_replace ???????? p1)
1165	[1,3,5:
1166	cases daemon
1167	\|2,4:
1168	normalize nodelta
1169	@(pair_replace ?????????? p2)
1170	[1,3:
1171	cases daemon
1172	\|2,4:
1173	normalize nodelta >p3 normalize nodelta
1174	>p4 normalize nodelta try >p5
1175	]
1176	]
1177	(* XXX: switch to the right hand side *)
1178	normalize nodelta >EQs -s >EQticks -ticks
1179	whd in ⊢ (??%%);
1180	(* XXX: finally, prove the equality using sigma commutation *)
1181	@split_eq_status try %
1182	cases daemon
1183	]
1184	\|33,34,35,48: (* ANL, ORL, XRL, MOVX *)
1185	(* XXX: work on the right hand side *)
1186	cases addr #addr' normalize nodelta
1187	[1,3:
1188	cases addr' #addr'' normalize nodelta
1189	]
1190	@pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta
1191	(* XXX: switch to the left hand side *)
1192	-instr_refl >EQP -P normalize nodelta
1193	#sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1194	whd in ⊢ (??%?);
1195	<(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1196	(* XXX: work on the left hand side *)
1197	(* XXX: switch to the right hand side *)
1198	normalize nodelta >EQs -s >EQticks -ticks
1199	whd in ⊢ (??%%);
1200	(* XXX: finally, prove the equality using sigma commutation *)
1201	cases daemon
1202	\|47: (* MOV *)
1203	(* XXX: work on the right hand side *)
1204	cases addr -addr #addr normalize nodelta
1205	[1:
1206	cases addr #addr normalize nodelta
1207	[1:
1208	cases addr #addr normalize nodelta
1209	[1:
1210	cases addr #addr normalize nodelta
1211	[1:
1212	cases addr #addr normalize nodelta
1213	]
1214	]
1215	]
1216	]
1217	cases addr #lft #rgt normalize nodelta
1218	(* XXX: switch to the left hand side *)
1219	>EQP -P normalize nodelta
1220	#sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1221	whd in ⊢ (??%?);
1222	<(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1223	(* XXX: work on the left hand side *)
1224	(* XXX: switch to the right hand side *)
1225	normalize nodelta >EQs -s >EQticks -ticks
1226	whd in ⊢ (??%%);
1227	(* XXX: finally, prove the equality using sigma commutation *)
1228	cases daemon
1229	]
1230	qed.

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

Download in other formats:

Original Format