source: src/ASM/AssemblyProofSplit.ma @ 2143

Last change on this file since 2143 was 2143, checked in by mulligan, 8 years ago

Changes to the subaddressing mode elim functions moved into their correct place in ASM.ma. ticks_of0 completed, with all daemons removed. Another commutation lemma added in AssemblyProofSplit?.ma.

File size: 59.8 KB
Line 
1include "ASM/AssemblyProof.ma".
2include alias "arithmetics/nat.ma".
3include alias "basics/logic.ma".
4
5lemma 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 … d)
26  cases (vsplit bool 8 8 w) #bu #bl normalize nodelta
27  whd in match set_8051_sfr; normalize nodelta %
28qed.
29
30lemma 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  //
47qed.
48
49lemma 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  //
66qed.
67
68lemma 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 %
77qed.
78
79lemma get_8051_sfr_set_program_counter:
80  ∀M: Type[0].
81  ∀cm: M.
82  ∀s: PreStatus M cm.
83  ∀sfr: SFR8051.
84  ∀pc: Word.
85    get_8051_sfr M cm (set_program_counter M cm s pc) =
86      get_8051_sfr M cm s.
87  #M #cm #s #sfr #pc %
88qed.
89
90lemma special_function_registers_8051_set_arg_16:
91  ∀M, M': Type[0].
92  ∀cm: M.
93  ∀cm': M'.
94  ∀s: PreStatus M cm.
95  ∀s': PreStatus M' cm'.
96  ∀w, w': Word.
97  ∀d, d': [[dptr]].
98   special_function_registers_8051 ?? s = special_function_registers_8051 … s' →
99    w = w' →
100      special_function_registers_8051 ?? (set_arg_16 … s w d) =
101        special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d').
102  #M #M' #cm #cm' #s #s' #w #w'
103  #d @(subaddressing_mode_elim … d)
104  #d' @(subaddressing_mode_elim … d')
105  #EQ1 #EQ2 <EQ2 normalize cases (vsplit bool 8 8 w) #b1 #b2 normalize <EQ1 %
106qed.
107
108lemma program_counter_set_arg_1:
109  ∀M: Type[0].
110  ∀cm: M.
111  ∀s: PreStatus M cm.
112  ∀addr: [[bit_addr; carry]].
113  ∀b: Bit.
114    program_counter M cm (set_arg_1 M cm s addr b) = program_counter M cm s.
115  #M #cm #s whd in match set_arg_1; whd in match set_arg_1'; normalize nodelta
116  #addr #b
117  @(subaddressing_mode_elim … addr)
118  [1:
119    #byte cases (vsplit ????) #nu #nl normalize nodelta
120    cases (vsplit ????) #ignore #three_bits normalize nodelta
121    cases (get_index_v bool ????) normalize nodelta
122    [1:
123      @program_counter_set_bit_addressable_sfr
124    |2:
125      @program_counter_set_low_internal_ram
126    ]
127  |2:
128    cases (vsplit ????) //
129  ]
130qed.
131
132lemma get_ov_flag_set_program_counter:
133  ∀M: Type[0].
134  ∀cm: M.
135  ∀s: PreStatus M cm.
136  ∀pc: Word.
137    get_ov_flag M cm (set_program_counter M cm s pc) =
138      get_ov_flag M cm s.
139  #M #cm #s #pc %
140qed.
141
142lemma external_ram_set_program_counter:
143  ∀M: Type[0].
144  ∀cm: M.
145  ∀s: PreStatus M cm.
146  ∀pc: Word.
147    external_ram M cm (set_program_counter M cm s pc) =
148      external_ram M cm s.
149  #M #cm #s #pc %
150qed.
151
152lemma low_internal_ram_set_program_counter:
153  ∀M: Type[0].
154  ∀cm: M.
155  ∀s: PreStatus M cm.
156  ∀pc: Word.
157    low_internal_ram M cm (set_program_counter M cm s pc) =
158      low_internal_ram M cm s.
159  #M #cm #s #pc %
160qed.
161
162lemma high_internal_ram_set_program_counter:
163  ∀M: Type[0].
164  ∀cm: M.
165  ∀s: PreStatus M cm.
166  ∀pc: Word.
167    high_internal_ram M cm (set_program_counter M cm s pc) =
168      high_internal_ram M cm s.
169  #M #cm #s #pc %
170qed.
171
172lemma get_arg_8_set_program_counter:
173  ∀M: Type[0].
174  ∀cm: M.
175  ∀s: PreStatus M cm.
176  ∀flag: bool.
177  ∀addr: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; ext_indirect; ext_indirect_dptr]].
178  ∀pc: Word.
179    get_arg_8 M cm (set_program_counter M cm s pc) flag addr =
180      get_arg_8 M cm s flag addr.
181  [2,3:
182    cases addr #subaddressing_mode
183    cases subaddressing_mode
184    try (#addr1 whd in ⊢ (% → %);)
185    whd in ⊢ (% → %); //
186  ]
187  #M #cm #s #flag #addr #pc
188  whd in match get_arg_8; normalize nodelta
189  cases addr *
190  try (#addr1 #absurd normalize in absurd; cases absurd @I)
191  try (#absurd normalize in absurd; cases absurd @I)
192  try (#addr1 #addr2) try #addr1
193  normalize nodelta %
194qed.
195
196lemma external_ram_set_flags:
197  ∀M: Type[0].
198  ∀cm: M.
199  ∀s: PreStatus M cm.
200  ∀opt: option Bit.
201  ∀bit1, bit2: Bit.
202    external_ram M cm (set_flags M cm s bit1 opt bit2) =
203      external_ram M cm s.
204  #M #cm #s #opt #bit1 #bit2 %
205qed.
206
207lemma low_internal_ram_set_flags:
208  ∀M: Type[0].
209  ∀cm: M.
210  ∀s: PreStatus M cm.
211  ∀opt: option Bit.
212  ∀bit1, bit2: Bit.
213    low_internal_ram M cm (set_flags M cm s bit1 opt bit2) =
214      low_internal_ram M cm s.
215  #M #cm #s #opt #bit1 #bit2 %
216qed.
217
218lemma high_internal_ram_set_flags:
219  ∀M: Type[0].
220  ∀cm: M.
221  ∀s: PreStatus M cm.
222  ∀opt: option Bit.
223  ∀bit1, bit2: Bit.
224    high_internal_ram M cm (set_flags M cm s bit1 opt bit2) =
225      high_internal_ram M cm s.
226  #M #cm #s #opt #bit1 #bit2 %
227qed.
228
229lemma low_internal_ram_set_clock:
230  ∀M: Type[0].
231  ∀cm: M.
232  ∀s: PreStatus M cm.
233  ∀t: Time.
234    low_internal_ram M cm (set_clock M cm s t) =
235      low_internal_ram M cm s.
236  #M #cm #s #t %
237qed.
238
239lemma high_internal_ram_set_clock:
240  ∀M: Type[0].
241  ∀cm: M.
242  ∀s: PreStatus M cm.
243  ∀t: Time.
244    high_internal_ram M cm (set_clock M cm s t) =
245      high_internal_ram M cm s.
246  #M #cm #s #t %
247qed.
248
249lemma external_ram_set_clock:
250  ∀M: Type[0].
251  ∀cm: M.
252  ∀s: PreStatus M cm.
253  ∀t: Time.
254    external_ram M cm (set_clock M cm s t) =
255      external_ram M cm s.
256  #M #cm #s #t %
257qed.
258
259lemma set_8051_sfr_set_program_counter:
260  ∀M: Type[0].
261  ∀cm: M.
262  ∀s: PreStatus M cm.
263  ∀pc: Word.
264  ∀sfr: SFR8051.
265  ∀v: Byte.
266    set_8051_sfr M cm (set_program_counter M cm s pc) sfr v =
267      set_program_counter M cm (set_8051_sfr M cm s sfr v) pc.
268  #M #cm #s #pc #sfr #v %
269qed.
270
271lemma low_internal_ram_set_8051_sfr:
272  ∀M: Type[0].
273  ∀cm: M.
274  ∀s: PreStatus M cm.
275  ∀sfr: SFR8051.
276  ∀v: Byte.
277    low_internal_ram M cm (set_8051_sfr M cm s sfr v) =
278      low_internal_ram M cm s.
279  #M #cm #s #sfr #v %
280qed.
281
282lemma high_internal_ram_set_8051_sfr:
283  ∀M: Type[0].
284  ∀cm: M.
285  ∀s: PreStatus M cm.
286  ∀sfr: SFR8051.
287  ∀v: Byte.
288    high_internal_ram M cm (set_8051_sfr M cm s sfr v) =
289      high_internal_ram M cm s.
290  #M #cm #s #sfr #v %
291qed.
292
293lemma external_ram_set_8051_sfr:
294  ∀M: Type[0].
295  ∀cm: M.
296  ∀s: PreStatus M cm.
297  ∀sfr: SFR8051.
298  ∀v: Byte.
299    external_ram M cm (set_8051_sfr M cm s sfr v) =
300      external_ram M cm s.
301  #M #cm #s #sfr #v %
302qed.
303
304lemma get_arg_8_set_clock:
305  ∀M: Type[0].
306  ∀cm: M.
307  ∀s: PreStatus M cm.
308  ∀addr.
309  ∀t: Time.
310    get_arg_8 M cm (set_clock M cm s t) addr =
311      get_arg_8 M cm s addr.
312  #M #cm #s #addr #t %
313qed.
314
315lemma set_program_counter_set_program_counter:
316  ∀M: Type[0].
317  ∀cm: M.
318  ∀s: PreStatus M cm.
319  ∀pc: Word.
320  ∀pc': Word.
321    set_program_counter M cm (set_program_counter M cm s pc) pc' =
322      set_program_counter M cm s pc'.
323  #M #cm #s #pc #pc' %
324qed.
325
326(* XXX: move elsewhere *)
327lemma bitvector_8_cases:
328  ∀w: BitVector 8.
329    ∃b0,b1,b2,b3,b4,b5,b6,b7: bool.
330      w ≃ [[b0;b1;b2;b3;b4;b5;b6;b7]].
331 #w repeat (cases (BitVector_Sn … w)  #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w)
332 >(BitVector_O … w) %
333qed.
334
335(* XXX: not true
336lemma p3_latch_set_arg_8:
337  ∀M: Type[0].
338  ∀cm: M.
339  ∀s: PreStatus M cm.
340  ∀args.
341  ∀v: Byte.
342    p3_latch M cm (set_arg_8 M cm s args v) =
343      p3_latch M cm s.
344  #M #cm #s #args #v
345  @(subaddressing_mode_elim … args)
346  try #w try %
347  whd in match set_arg_8; normalize nodelta
348  whd in match set_arg_8'; normalize nodelta
349  inversion (vsplit bool ???) #nu #nl #nu_nl_refl normalize nodelta
350  inversion (vsplit bool ???) #ignore #three_bits #ignore_three_bits_refl normalize nodelta
351  inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta try %
352  whd in match set_bit_addressable_sfr; normalize nodelta
353  @(bitvector_8_elim_prop … w)
354*)
355
356lemma status_of_pseudo_status_does_not_change_8051_sfrs:
357  ∀M: internal_pseudo_address_map.
358  ∀cm: pseudo_assembly_program.
359  ∀s: PreStatus pseudo_assembly_program cm.
360  ∀sigma: Word → Word.
361  ∀policy: Word → bool.
362    \snd M = (None …) →
363      special_function_registers_8051 pseudo_assembly_program cm s =
364        special_function_registers_8051 (BitVectorTrie Byte 16)
365          (code_memory_of_pseudo_assembly_program cm sigma policy)
366          (status_of_pseudo_status M cm s sigma policy).
367  #M #cm #s #sigma #policy #None_proof cases s
368  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
369  whd in match status_of_pseudo_status; normalize nodelta
370  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
371  >None_proof %
372qed.
373
374lemma special_function_registers_8051_set_program_counter:
375  ∀cm: pseudo_assembly_program.
376  ∀ps: PreStatus pseudo_assembly_program cm.
377  ∀v: Word.
378  special_function_registers_8051 pseudo_assembly_program cm
379   (set_program_counter pseudo_assembly_program cm ps v) =
380     special_function_registers_8051 pseudo_assembly_program cm ps.
381  #cm #ps #v %
382qed.
383
384(*
385lemma get_arg_8_status_of_pseudo_status:
386  ∀M: internal_pseudo_address_map.
387  ∀cm: pseudo_assembly_program.
388  ∀ps.
389  ∀sigma: Word → Word.
390  ∀policy: Word → bool.
391  ∀b: bool.
392  ∀addr1: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; ext_indirect_dptr]].
393    get_arg_8 (BitVectorTrie Byte 16)
394     (code_memory_of_pseudo_assembly_program cm sigma policy)
395     (status_of_pseudo_status M cm ps sigma policy) b addr1 =
396    get_arg_8 pseudo_assembly_program cm ps b addr1.
397  [2,3:
398    @(subaddressing_mode_elim … addr1) try #w @I
399  ]
400  #M #cm #ps #sigma #policy #b #addr1
401  @(subaddressing_mode_elim … addr1)
402  try #w
403  [1:
404    whd in ⊢ (??%%);
405    @pair_elim #nu #nl #nu_nl_refl normalize nodelta
406    @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
407    cases (get_index_v bool ????) normalize nodelta try %
408    cases daemon (* XXX: require axioms from Assembly.ma *)
409  |2:
410    whd in ⊢ (??%%);
411    @pair_elim #nu #nl #nu_nl_refl normalize nodelta
412    lapply (refl_to_jmrefl ??? nu_nl_refl) -nu_nl_refl #nu_nl_refl
413    @(pair_replace ?????????? nu_nl_refl) [1: cases daemon (* XXX: !! *) ]
414    @pair_elim #bit_one_v #three_bits #bit_one_v_three_bits_refl normalize nodelta
415    cases (get_index_v bool ????) normalize nodelta
416    cases daemon (* XXX: same as above *)
417  |3:
418    whd in ⊢ (??%%); @(bitvector_3_elim_prop … w)
419    whd in match bit_address_of_register; normalize nodelta
420    @pair_elim #un #ln #un_ln_refl
421    cases (¬get_index_v bool ???? ∧ ¬get_index_v bool ????) normalize nodelta
422    [1,3,5,7,9,11,13,15:
423      cases daemon (* XXX: same as above *)
424    |*:
425      cases (¬get_index_v bool ???? ∧ get_index_v bool ????) normalize nodelta
426      [1,3,5,7,9,11,13,15:
427        cases daemon (* XXX: same as above *)
428      |*:
429        cases (get_index_v bool ???? ∧ get_index_v bool ????) normalize nodelta
430        cases daemon (* XXX: same as above *)
431      ]
432    ]
433  |4,5:
434    whd in ⊢ (??%%); <status_of_pseudo_status_does_not_change_8051_sfrs %
435  |6,7,8:
436    %
437  ]
438qed.
439*)
440
441(*
442lemma pi1_let_commute:
443 ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c.
444 pi1 … (let 〈x1,y1〉 ≝ c in t) = (let 〈x1,y1〉 ≝ c in pi1 … t).
445 #A #B #C #P * #a #b * //
446qed.
447
448lemma pi1_let_as_commute:
449 ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c.
450 pi1 … (let 〈x1,y1〉 as H ≝ c in t) =
451  (let 〈x1,y1〉 as H ≝ c in pi1 … t).
452 #A #B #C #P * #a #b * //
453qed.
454
455lemma tech_pi1_let_as_commute:
456 ∀A,B,C,P. ∀f. ∀c,c':A × B.
457 ∀t: ∀a,b. 〈a,b〉=c → Σc:C.P c.
458 ∀t': ∀a,b. 〈a,b〉=c' → Σc:C.P c.
459  c=c' → (∀x,y,H,H'.t x y H = f (pi1 … (t' x y H'))) →
460  pi1 … (let 〈x1,y1〉 as H ≝ c in t x1 y1 H) =
461   f (pi1 … (let 〈x1,y1〉 as H ≝ c' in t' x1 y1 H)).
462 #A #B #C #P #f * #a #b * #a' #b' #t #t' #EQ1 destruct normalize /2/
463qed.
464*)
465
466include alias "arithmetics/nat.ma".
467include alias "basics/logic.ma".
468include alias "ASM/BitVectorTrie.ma".
469
470lemma fetch_many_singleton:
471  ∀code_memory: BitVectorTrie Byte 16.
472  ∀final_pc, start_pc: Word.
473  ∀i: instruction.
474    fetch_many code_memory final_pc start_pc [i] →
475      〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory start_pc.
476  #code_memory #final_pc #start_pc #i * #new_pc
477  #fetch_many_assm whd in fetch_many_assm;
478  cases (eq_bv_eq … fetch_many_assm) assumption
479qed.
480
481include alias "ASM/Vector.ma".
482
483lemma main_lemma_preinstruction:
484  ∀M, M': internal_pseudo_address_map.
485  ∀preamble: preamble.
486  ∀instr_list: list labelled_instruction.
487  ∀cm: pseudo_assembly_program.
488  ∀EQcm: cm = 〈preamble, instr_list〉.
489  ∀is_well_labelled_witness: is_well_labelled_p instr_list.
490  ∀sigma: Word → Word.
491  ∀policy: Word → bool.
492  ∀sigma_policy_witness: sigma_policy_specification cm sigma policy.
493  ∀ps: PseudoStatus cm.
494  ∀ppc: Word.
495  ∀program_counter_in_bounds_witness: nat_of_bitvector … ppc < |instr_list|.
496  ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps.
497  ∀labels: label_map.
498  ∀costs: BitVectorTrie costlabel 16.
499  ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉.
500  ∀newppc: Word.
501  ∀lookup_labels: Identifier → Word.
502  ∀EQlookup_labels: lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)).
503  ∀lookup_datalabels: Identifier → Word.
504  ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
505  ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1).
506  ∀instr: preinstruction Identifier.
507  ∀fetch_pseudo_refl: \fst  (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr.
508  ∀ticks: nat × nat.
509  ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr).
510  ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
511  ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x).
512  ∀s: PreStatus pseudo_assembly_program cm.
513  ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))).
514  ∀P: preinstruction Identifier → PseudoStatus cm → Prop.
515  ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc)
516              (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
517                  lookup_datalabels (Instruction instr)))) →
518              next_internal_pseudo_address_map0 ? cm addr_of (Instruction instr) M ps = Some internal_pseudo_address_map M' →
519                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))
520                  (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) →
521                    ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) =
522                      status_of_pseudo_status M' cm s sigma policy).
523    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
524  (* XXX: takes about 45 minutes to type check! *)
525  #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
526  #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
527  #costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels
528  #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr #fetch_pseudo_refl
529  #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
530  (*#sigma_increment_commutation #maps_assm #fetch_many_assm *)
531  letin a ≝ Identifier letin m ≝ pseudo_assembly_program
532  cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s))
533  [2: * // ]
534  @(
535  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
536  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
537  match instr in preinstruction return λx. x = instr → Σs'.? with
538        [ ADD addr1 addr2 ⇒ λinstr_refl.
539            let s ≝ add_ticks1 s in
540            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
541                                                   (get_arg_8 … s false addr2) false in
542            let cy_flag ≝ get_index' ? O  ? flags in
543            let ac_flag ≝ get_index' ? 1 ? flags in
544            let ov_flag ≝ get_index' ? 2 ? flags in
545            let s ≝ set_arg_8 … s ACC_A result in
546              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
547        | ADDC addr1 addr2 ⇒ λinstr_refl.
548            let s ≝ add_ticks1 s in
549            let old_cy_flag ≝ get_cy_flag ?? s in
550            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
551                                                   (get_arg_8 … s false addr2) old_cy_flag in
552            let cy_flag ≝ get_index' ? O ? flags in
553            let ac_flag ≝ get_index' ? 1 ? flags in
554            let ov_flag ≝ get_index' ? 2 ? flags in
555            let s ≝ set_arg_8 … s ACC_A result in
556              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
557        | SUBB addr1 addr2 ⇒ λinstr_refl.
558            let s ≝ add_ticks1 s in
559            let old_cy_flag ≝ get_cy_flag ?? s in
560            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
561                                                   (get_arg_8 … s false addr2) old_cy_flag in
562            let cy_flag ≝ get_index' ? O ? flags in
563            let ac_flag ≝ get_index' ? 1 ? flags in
564            let ov_flag ≝ get_index' ? 2 ? flags in
565            let s ≝ set_arg_8 … s ACC_A result in
566              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
567        | ANL addr ⇒ λinstr_refl.
568          let s ≝ add_ticks1 s in
569          match addr with
570            [ inl l ⇒
571              match l with
572                [ inl l' ⇒
573                  let 〈addr1, addr2〉 ≝ l' in
574                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
575                    set_arg_8 … s addr1 and_val
576                | inr r ⇒
577                  let 〈addr1, addr2〉 ≝ r in
578                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
579                    set_arg_8 … s addr1 and_val
580                ]
581            | inr r ⇒
582              let 〈addr1, addr2〉 ≝ r in
583              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
584               set_flags … s and_val (None ?) (get_ov_flag ?? s)
585            ]
586        | ORL addr ⇒ λinstr_refl.
587          let s ≝ add_ticks1 s in
588          match addr with
589            [ inl l ⇒
590              match l with
591                [ inl l' ⇒
592                  let 〈addr1, addr2〉 ≝ l' in
593                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
594                    set_arg_8 … s addr1 or_val
595                | inr r ⇒
596                  let 〈addr1, addr2〉 ≝ r in
597                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
598                    set_arg_8 … s addr1 or_val
599                ]
600            | inr r ⇒
601              let 〈addr1, addr2〉 ≝ r in
602              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
603               set_flags … s or_val (None ?) (get_ov_flag … s)
604            ]
605        | XRL addr ⇒ λinstr_refl.
606          let s ≝ add_ticks1 s in
607          match addr with
608            [ inl l' ⇒
609              let 〈addr1, addr2〉 ≝ l' in
610              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
611                set_arg_8 … s addr1 xor_val
612            | inr r ⇒
613              let 〈addr1, addr2〉 ≝ r in
614              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
615                set_arg_8 … s addr1 xor_val
616            ]
617        | INC addr ⇒ λinstr_refl.
618            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → Σs': PreStatus m cm. ? with
619              [ ACC_A ⇒ λacc_a: True. λEQaddr.
620                let s' ≝ add_ticks1 s in
621                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
622                 set_arg_8 … s' ACC_A result
623              | REGISTER r ⇒ λregister: True. λEQaddr.
624                let s' ≝ add_ticks1 s in
625                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
626                 set_arg_8 … s' (REGISTER r) result
627              | DIRECT d ⇒ λdirect: True. λEQaddr.
628                let s' ≝ add_ticks1 s in
629                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
630                 set_arg_8 … s' (DIRECT d) result
631              | INDIRECT i ⇒ λindirect: True. λEQaddr.
632                let s' ≝ add_ticks1 s in
633                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
634                 set_arg_8 … s' (INDIRECT i) result
635              | DPTR ⇒ λdptr: True. λEQaddr.
636                let s' ≝ add_ticks1 s in
637                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
638                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
639                let s ≝ set_8051_sfr … s' SFR_DPL bl in
640                 set_8051_sfr … s' SFR_DPH bu
641              | _ ⇒ λother: False. ⊥
642              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
643        | NOP ⇒ λinstr_refl.
644           let s ≝ add_ticks2 s in
645            s
646        | DEC addr ⇒ λinstr_refl.
647           let s ≝ add_ticks1 s in
648           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
649             set_arg_8 … s addr result
650        | MUL addr1 addr2 ⇒ λinstr_refl.
651           let s ≝ add_ticks1 s in
652           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
653           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
654           let product ≝ acc_a_nat * acc_b_nat in
655           let ov_flag ≝ product ≥ 256 in
656           let low ≝ bitvector_of_nat 8 (product mod 256) in
657           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
658           let s ≝ set_8051_sfr … s SFR_ACC_A low in
659             set_8051_sfr … s SFR_ACC_B high
660        | DIV addr1 addr2 ⇒ λinstr_refl.
661           let s ≝ add_ticks1 s in
662           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
663           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
664             match acc_b_nat with
665               [ O ⇒ set_flags … s false (None Bit) true
666               | S o ⇒
667                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
668                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
669                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
670                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
671                   set_flags … s false (None Bit) false
672               ]
673        | DA addr ⇒ λinstr_refl.
674            let s ≝ add_ticks1 s in
675            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
676              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
677                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
678                let cy_flag ≝ get_index' ? O ? flags in
679                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
680                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
681                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
682                    let new_acc ≝ nu @@ acc_nl' in
683                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
684                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
685                  else
686                    s
687              else
688                s
689        | CLR addr ⇒ λinstr_refl.
690          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
691            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
692              let s ≝ add_ticks1 s in
693               set_arg_8 … s ACC_A (zero 8)
694            | CARRY ⇒ λcarry: True.  λEQaddr.
695              let s ≝ add_ticks1 s in
696               set_arg_1 … s CARRY false
697            | BIT_ADDR b ⇒ λbit_addr: True.  λEQaddr.
698              let s ≝ add_ticks1 s in
699               set_arg_1 … s (BIT_ADDR b) false
700            | _ ⇒ λother: False. ⊥
701            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
702        | CPL addr ⇒ λinstr_refl.
703          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
704            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
705                let s ≝ add_ticks1 s in
706                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
707                let new_acc ≝ negation_bv ? old_acc in
708                 set_8051_sfr … s SFR_ACC_A new_acc
709            | CARRY ⇒ λcarry: True. λEQaddr.
710                let s ≝ add_ticks1 s in
711                let old_cy_flag ≝ get_arg_1 … s CARRY true in
712                let new_cy_flag ≝ ¬old_cy_flag in
713                 set_arg_1 … s CARRY new_cy_flag
714            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
715                let s ≝ add_ticks1 s in
716                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
717                let new_bit ≝ ¬old_bit in
718                 set_arg_1 … s (BIT_ADDR b) new_bit
719            | _ ⇒ λother: False. ?
720            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
721        | SETB b ⇒ λinstr_refl.
722            let s ≝ add_ticks1 s in
723            set_arg_1 … s b false
724        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
725            let s ≝ add_ticks1 s in
726            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
727            let new_acc ≝ rotate_left … 1 old_acc in
728              set_8051_sfr … s SFR_ACC_A new_acc
729        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
730            let s ≝ add_ticks1 s in
731            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
732            let new_acc ≝ rotate_right … 1 old_acc in
733              set_8051_sfr … s SFR_ACC_A new_acc
734        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
735            let s ≝ add_ticks1 s in
736            let old_cy_flag ≝ get_cy_flag ?? s in
737            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
738            let new_cy_flag ≝ get_index' ? O ? old_acc in
739            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
740            let s ≝ set_arg_1 … s CARRY new_cy_flag in
741              set_8051_sfr … s SFR_ACC_A new_acc
742        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
743            let s ≝ add_ticks1 s in
744            let old_cy_flag ≝ get_cy_flag ?? s in
745            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
746            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
747            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
748            let s ≝ set_arg_1 … s CARRY new_cy_flag in
749              set_8051_sfr … s SFR_ACC_A new_acc
750        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
751            let s ≝ add_ticks1 s in
752            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
753            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
754            let new_acc ≝ nl @@ nu in
755              set_8051_sfr … s SFR_ACC_A new_acc
756        | PUSH addr ⇒ λinstr_refl.
757            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → Σs': PreStatus m cm. ? with
758              [ DIRECT d ⇒ λdirect: True. λEQaddr.
759                let s ≝ add_ticks1 s in
760                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
761                let s ≝ set_8051_sfr … s SFR_SP new_sp in
762                  write_at_stack_pointer … s d
763              | _ ⇒ λother: False. ⊥
764              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
765        | POP addr ⇒ λinstr_refl.
766            let s ≝ add_ticks1 s in
767            let contents ≝ read_at_stack_pointer ?? s in
768            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
769            let s ≝ set_8051_sfr … s SFR_SP new_sp in
770              set_arg_8 … s addr contents
771        | XCH addr1 addr2 ⇒ λinstr_refl.
772            let s ≝ add_ticks1 s in
773            let old_addr ≝ get_arg_8 … s false addr2 in
774            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
775            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
776              set_arg_8 … s addr2 old_acc
777        | XCHD addr1 addr2 ⇒ λinstr_refl.
778            let s ≝ add_ticks1 s in
779            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
780            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
781            let new_acc ≝ acc_nu @@ arg_nl in
782            let new_arg ≝ arg_nu @@ acc_nl in
783            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
784              set_arg_8 … s addr2 new_arg
785        | RET ⇒ λinstr_refl.
786            let s ≝ add_ticks1 s in
787            let high_bits ≝ read_at_stack_pointer ?? s in
788            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
789            let s ≝ set_8051_sfr … s SFR_SP new_sp in
790            let low_bits ≝ read_at_stack_pointer ?? s in
791            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
792            let s ≝ set_8051_sfr … s SFR_SP new_sp in
793            let new_pc ≝ high_bits @@ low_bits in
794              set_program_counter … s new_pc
795        | RETI ⇒ λinstr_refl.
796            let s ≝ add_ticks1 s in
797            let high_bits ≝ read_at_stack_pointer ?? s in
798            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
799            let s ≝ set_8051_sfr … s SFR_SP new_sp in
800            let low_bits ≝ read_at_stack_pointer ?? s in
801            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
802            let s ≝ set_8051_sfr … s SFR_SP new_sp in
803            let new_pc ≝ high_bits @@ low_bits in
804              set_program_counter … s new_pc
805        | MOVX addr ⇒ λinstr_refl.
806          let s ≝ add_ticks1 s in
807          (* DPM: only copies --- doesn't affect I/O *)
808          match addr with
809            [ inl l ⇒
810              let 〈addr1, addr2〉 ≝ l in
811                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
812            | inr r ⇒
813              let 〈addr1, addr2〉 ≝ r in
814                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
815            ]
816        | MOV addr ⇒ λinstr_refl.
817          let s ≝ add_ticks1 s in
818          match addr with
819            [ inl l ⇒
820              match l with
821                [ inl l' ⇒
822                  match l' with
823                    [ inl l'' ⇒
824                      match l'' with
825                        [ inl l''' ⇒
826                          match l''' with
827                            [ inl l'''' ⇒
828                              let 〈addr1, addr2〉 ≝ l'''' in
829                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
830                            | inr r'''' ⇒
831                              let 〈addr1, addr2〉 ≝ r'''' in
832                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
833                            ]
834                        | inr r''' ⇒
835                          let 〈addr1, addr2〉 ≝ r''' in
836                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
837                        ]
838                    | inr r'' ⇒
839                      let 〈addr1, addr2〉 ≝ r'' in
840                       set_arg_16 … s (get_arg_16 … s addr2) addr1
841                    ]
842                | inr r ⇒
843                  let 〈addr1, addr2〉 ≝ r in
844                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
845                ]
846            | inr r ⇒
847              let 〈addr1, addr2〉 ≝ r in
848               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
849            ]
850          | JC addr ⇒ λinstr_refl.
851                  if get_cy_flag ?? s then
852                    let s ≝ add_ticks1 s in
853                      set_program_counter … s (addr_of addr s)
854                  else
855                    let s ≝ add_ticks2 s in
856                      s
857            | JNC addr ⇒ λinstr_refl.
858                  if ¬(get_cy_flag ?? s) then
859                   let s ≝ add_ticks1 s in
860                     set_program_counter … s (addr_of addr s)
861                  else
862                   let s ≝ add_ticks2 s in
863                    s
864            | JB addr1 addr2 ⇒ λinstr_refl.
865                  if get_arg_1 … s addr1 false then
866                   let s ≝ add_ticks1 s in
867                    set_program_counter … s (addr_of addr2 s)
868                  else
869                   let s ≝ add_ticks2 s in
870                    s
871            | JNB addr1 addr2 ⇒ λinstr_refl.
872                  if ¬(get_arg_1 … s addr1 false) then
873                   let s ≝ add_ticks1 s in
874                    set_program_counter … s (addr_of addr2 s)
875                  else
876                   let s ≝ add_ticks2 s in
877                    s
878            | JBC addr1 addr2 ⇒ λinstr_refl.
879                  let s ≝ set_arg_1 … s addr1 false in
880                    if get_arg_1 … s addr1 false then
881                     let s ≝ add_ticks1 s in
882                      set_program_counter … s (addr_of addr2 s)
883                    else
884                     let s ≝ add_ticks2 s in
885                      s
886            | JZ addr ⇒ λinstr_refl.
887                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
888                     let s ≝ add_ticks1 s in
889                      set_program_counter … s (addr_of addr s)
890                    else
891                     let s ≝ add_ticks2 s in
892                      s
893            | JNZ addr ⇒ λinstr_refl.
894                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
895                     let s ≝ add_ticks1 s in
896                      set_program_counter … s (addr_of addr s)
897                    else
898                     let s ≝ add_ticks2 s in
899                      s
900            | CJNE addr1 addr2 ⇒ λinstr_refl.
901                  match addr1 with
902                    [ inl l ⇒
903                        let 〈addr1, addr2'〉 ≝ l in
904                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
905                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
906                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
907                            let s ≝ add_ticks1 s in
908                            let s ≝ set_program_counter … s (addr_of addr2 s) in
909                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
910                          else
911                            let s ≝ add_ticks2 s in
912                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
913                    | inr r' ⇒
914                        let 〈addr1, addr2'〉 ≝ r' in
915                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
916                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
917                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
918                            let s ≝ add_ticks1 s in
919                            let s ≝ set_program_counter … s (addr_of addr2 s) in
920                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
921                          else
922                            let s ≝ add_ticks2 s in
923                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
924                    ]
925            | DJNZ addr1 addr2 ⇒ λinstr_refl.
926              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
927              let s ≝ set_arg_8 … s addr1 result in
928                if ¬(eq_bv ? result (zero 8)) then
929                 let s ≝ add_ticks1 s in
930                  set_program_counter … s (addr_of addr2 s)
931                else
932                 let s ≝ add_ticks2 s in
933                  s
934           ] (refl … instr))
935  try (cases(other))
936  try assumption (*20s*)
937  try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
938  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
939  whd in match execute_1_preinstruction; normalize nodelta
940  [31,32: (* DJNZ *)
941  (* XXX: work on the right hand side *)
942  >p normalize nodelta >p1 normalize nodelta
943  (* XXX: switch to the left hand side *)
944  >EQP -P normalize nodelta
945  #sigma_increment_commutation #maps_assm #fetch_many_assm
946  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
947  <EQppc in fetch_many_assm;
948  whd in match (short_jump_cond ??);
949  @pair_elim #sj_possible #disp
950  @pair_elim #result #flags #sub16_refl
951  @pair_elim #upper #lower #vsplit_refl
952  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
953  #sj_possible_pair destruct(sj_possible_pair)
954  >p1 normalize nodelta
955  [1,3:
956    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
957    whd in ⊢ (??%?);
958    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
959    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
960    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
961    (* XXX: work on the left hand side *)
962    @(pair_replace ?????????? p) normalize nodelta
963    [1,3:
964      >(get_arg_8_set_program_counter … true addr1) in ⊢ (??%?);
965      [2,4: (* /2 by _/ *) cases daemon ] @eq_f3 [2,3,5,6: % ]
966      whd in ⊢ (??%?); @(subaddressing_mode_elim … addr1)
967      #arg normalize nodelta whd in ⊢ (???%);
968      [1,3:
969        whd in match get_register; normalize nodelta
970        @(bitvector_3_elim_prop … arg)
971        whd in match bit_address_of_register; normalize nodelta
972        @pair_elim #un #ln #un_ln_refl
973        lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
974        @(pair_replace ?????????? un_ln_refl)
975        [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31:
976          whd in match get_8051_sfr; normalize nodelta
977          whd in match sfr_8051_index; normalize nodelta
978          @eq_f <status_of_pseudo_status_does_not_change_8051_sfrs
979          >EQs
980          [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31:
981            /demod nohyps/ %
982          |*:
983            cases daemon
984          ]
985        |*:
986          >low_internal_ram_of_pseudo_internal_ram_miss
987          cases daemon
988          (* XXX: require axioms about low_internal_ram_of_pseudo_low_internal_ram *)         
989        ]
990      |2,4:
991        @pair_elim #nu #nl #nu_nl_refl
992        lapply (refl_to_jmrefl ??? nu_nl_refl) -nu_nl_refl #nu_nl_refl
993        @pair_elim #ignore #three_bits #ignore_three_bits_refl
994        lapply (refl_to_jmrefl ??? ignore_three_bits_refl) -ignore_three_bits_refl #ignore_three_bits_refl
995        inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
996        [1,3:
997          @(pair_replace ?????????? ignore_three_bits_refl) try %
998          >get_index_v_refl normalize nodelta >EQs %
999        |2,4:
1000          @(pair_replace ?????????? ignore_three_bits_refl) try %
1001          >get_index_v_refl normalize nodelta >EQs
1002          cases daemon
1003          (* XXX: require axioms about low_internal_ram as above *)
1004        ]
1005      ]
1006    ]
1007    (* XXX: switch to the right hand side *)
1008    normalize nodelta >EQs -s >EQticks -ticks
1009    cases (¬ eq_bv ???) normalize nodelta
1010    whd in ⊢ (??%%);
1011    (* XXX: finally, prove the equality using sigma commutation *)
1012    @split_eq_status try %
1013    [1,2,3,19,20,21,28,29,30:
1014      cases daemon (* XXX: axioms as above *)
1015    |4,13,22,31:
1016    |5,14,23,32:
1017    |6,15,24,33:
1018    |7,16,25,34:
1019    |8,17,26,35:
1020      whd in ⊢ (??%%);
1021     
1022    |9,18,27,36:
1023      whd in ⊢ (??%%);
1024      whd in match (ticks_of_instruction ?); <instr_refl
1025      cases daemon (* XXX: daemon in ticks_of0 stopping progression *)
1026    ]
1027  |2,4:
1028    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
1029    [2, 4:
1030      cases daemon (* XXX: !!! *)
1031    ]
1032    normalize nodelta >EQppc
1033    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
1034    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
1035    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
1036    #fetch_many_assm whd in fetch_many_assm; %{2}
1037    change with (execute_1 ?? = ?)
1038    @(pose … (execute_1 ? (status_of_pseudo_status …)))
1039    #status_after_1 #EQstatus_after_1
1040    <(?: ? = status_after_1)
1041    [3,6:
1042      >EQstatus_after_1 in ⊢ (???%);
1043      whd in ⊢ (???%);
1044      [1:
1045        <fetch_refl in ⊢ (???%);
1046      |2:
1047        <fetch_refl in ⊢ (???%);
1048      ]
1049      whd in ⊢ (???%);
1050      @(pair_replace ?????????? p)
1051      [1,3:
1052        cases daemon
1053      |2,4:
1054        normalize nodelta
1055        whd in match (addr_of_relative ????);
1056        cases (¬ eq_bv ???) normalize nodelta
1057        >set_clock_mk_Status_commutation
1058        whd in ⊢ (???%);
1059        change with (add ???) in match (\snd (half_add ???));
1060        >set_arg_8_set_program_counter in ⊢ (???%);
1061        [2,4,6,8: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1062        >program_counter_set_program_counter in ⊢ (???%);
1063        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
1064        [2,4,6,8:
1065          >bitvector_of_nat_sign_extension_equivalence
1066          [1,3,5,7:
1067            >EQintermediate_pc' %
1068          |*:
1069            repeat @le_S_S @le_O_n
1070          ]
1071        ]
1072        [1,3: % ]
1073      ]
1074    |1,4:
1075      skip
1076    ]
1077    [3,4:
1078      -status_after_1
1079      @(pose … (execute_1 ? (mk_PreStatus …)))
1080      #status_after_1 #EQstatus_after_1
1081      <(?: ? = status_after_1)
1082      [3,6:
1083        >EQstatus_after_1 in ⊢ (???%);
1084        whd in ⊢ (???%);
1085        (* XXX: matita bug with patterns across multiple goals *)
1086        [1:
1087          <fetch_refl'' in ⊢ (???%);
1088        |2:
1089          <fetch_refl'' in ⊢ (???%);
1090        ]
1091        [2: % |1: whd in ⊢ (???%); % ]
1092      |1,4:
1093        skip
1094      ]
1095      -status_after_1 whd in ⊢ (??%?);
1096      (* XXX: switch to the right hand side *)
1097      normalize nodelta >EQs -s >EQticks -ticks
1098      normalize nodelta whd in ⊢ (??%%);
1099    ]
1100    (* XXX: finally, prove the equality using sigma commutation *)
1101    @split_eq_status try %
1102    whd in ⊢ (??%%);
1103    cases daemon
1104  ]
1105  |30: (* CJNE *)
1106  (* XXX: work on the right hand side *)
1107  cases addr1 -addr1 #addr1 normalize nodelta
1108  cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
1109  (* XXX: switch to the left hand side *)
1110  >EQP -P normalize nodelta
1111  #sigma_increment_commutation #maps_assm #fetch_many_assm
1112
1113  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1114  <EQppc in fetch_many_assm;
1115  whd in match (short_jump_cond ??);
1116  @pair_elim #sj_possible #disp
1117  @pair_elim #result #flags #sub16_refl
1118  @pair_elim #upper #lower #vsplit_refl
1119  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
1120  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
1121  [1,3:
1122    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
1123    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
1124    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
1125    whd in ⊢ (??%?);
1126    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1127    inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
1128    lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
1129    @(if_then_else_replace ???????? eq_bv_refl)
1130    [1,3,5,7:
1131      cases daemon
1132    |2,4,6,8:
1133      (* XXX: switch to the right hand side *)
1134      normalize nodelta >EQs -s >EQticks -ticks
1135      whd in ⊢ (??%%);
1136      (* XXX: finally, prove the equality using sigma commutation *)
1137      @split_eq_status try %
1138      [3,7,11,15:
1139        whd in ⊢ (??%?);
1140        [1,3:
1141          cases daemon
1142        |2,4:
1143          cases daemon
1144        ]
1145      ]
1146      cases daemon (* XXX *)
1147    ]
1148  |2,4:
1149    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
1150    [2, 4:
1151      cases daemon (* XXX: !!! *)
1152    ]
1153    normalize nodelta >EQppc
1154    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
1155    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
1156    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
1157    #fetch_many_assm whd in fetch_many_assm; %{2}
1158    change with (execute_1 ?? = ?)
1159    @(pose … (execute_1 ? (status_of_pseudo_status …)))
1160    #status_after_1 #EQstatus_after_1
1161    <(?: ? = status_after_1)
1162    [2,5:
1163      inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
1164    |3,6:
1165      >EQstatus_after_1 in ⊢ (???%);
1166      whd in ⊢ (???%);
1167      [1: <fetch_refl in ⊢ (???%);
1168      |2: <fetch_refl in ⊢ (???%);
1169      ]
1170      whd in ⊢ (???%);
1171      inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
1172      whd in ⊢ (???%);
1173      whd in match (addr_of_relative ????);
1174      change with (add ???) in match (\snd (half_add ???));
1175      >set_clock_set_program_counter in ⊢ (???%);
1176      >program_counter_set_program_counter in ⊢ (???%);
1177      >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
1178      [2,4,6,8:
1179        >bitvector_of_nat_sign_extension_equivalence
1180        [1,3,5,7:
1181          >EQintermediate_pc' %
1182        |*:
1183          repeat @le_S_S @le_O_n
1184        ]
1185      |1,5:
1186        %
1187      ]
1188    |1,4: skip
1189    ]
1190    [1,2,3,4:
1191      -status_after_1
1192      @(pose … (execute_1 ? (mk_PreStatus …)))
1193      #status_after_1 #EQstatus_after_1
1194      <(?: ? = status_after_1)
1195      [3,6,9,12:
1196        >EQstatus_after_1 in ⊢ (???%);
1197        whd in ⊢ (???%);
1198        (* XXX: matita bug with patterns across multiple goals *)
1199        [1: <fetch_refl'' in ⊢ (???%);
1200        |2: <fetch_refl'' in ⊢ (???%);
1201        |3: <fetch_refl'' in ⊢ (???%);
1202        |4: <fetch_refl'' in ⊢ (???%);
1203        ] %
1204      |1,4,7,10:
1205        skip
1206      ]
1207      -status_after_1 whd in ⊢ (??%?);
1208      (* XXX: switch to the right hand side *)
1209      normalize nodelta >EQs -s >EQticks -ticks
1210      whd in ⊢ (??%%);
1211    ]
1212    (* XXX: finally, prove the equality using sigma commutation *)
1213    @split_eq_status try %
1214    cases daemon
1215  ]
1216  |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
1217  (* XXX: work on the right hand side *)
1218  >p normalize nodelta
1219  (* XXX: switch to the left hand side *)
1220  >EQP -P normalize nodelta
1221  #sigma_increment_commutation #maps_assm #fetch_many_assm
1222 
1223  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1224  <EQppc in fetch_many_assm;
1225  whd in match (short_jump_cond ??);
1226  @pair_elim #sj_possible #disp
1227  @pair_elim #result #flags #sub16_refl
1228  @pair_elim #upper #lower #vsplit_refl
1229  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
1230  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
1231  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1232    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
1233    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
1234    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
1235    whd in ⊢ (??%?);
1236    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1237    (* XXX: work on the left hand side *)
1238    @(if_then_else_replace ???????? p) normalize nodelta
1239    [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1240      cases daemon
1241    ]
1242    (* XXX: switch to the right hand side *)
1243    normalize nodelta >EQs -s >EQticks -ticks
1244    whd in ⊢ (??%%);
1245    (* XXX: finally, prove the equality using sigma commutation *)
1246    @split_eq_status try %
1247    cases daemon
1248  |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1249    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
1250    [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1251      cases daemon (* XXX: !!! *)
1252    ]
1253    normalize nodelta >EQppc
1254    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
1255    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
1256    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
1257    #fetch_many_assm whd in fetch_many_assm; %{2}
1258    change with (execute_1 ?? = ?)
1259    @(pose … (execute_1 ? (status_of_pseudo_status …)))
1260    #status_after_1 #EQstatus_after_1
1261    <(?: ? = status_after_1)
1262    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
1263      >EQstatus_after_1 in ⊢ (???%);
1264      whd in ⊢ (???%);
1265      [1: <fetch_refl in ⊢ (???%);
1266      |2: <fetch_refl in ⊢ (???%);
1267      |3: <fetch_refl in ⊢ (???%);
1268      |4: <fetch_refl in ⊢ (???%);
1269      |5: <fetch_refl in ⊢ (???%);
1270      |6: <fetch_refl in ⊢ (???%);
1271      |7: <fetch_refl in ⊢ (???%);
1272      |8: <fetch_refl in ⊢ (???%);
1273      |9: <fetch_refl in ⊢ (???%);
1274      |10: <fetch_refl in ⊢ (???%);
1275      |11: <fetch_refl in ⊢ (???%);
1276      |12: <fetch_refl in ⊢ (???%);
1277      |13: <fetch_refl in ⊢ (???%);
1278      |14: <fetch_refl in ⊢ (???%);
1279      ]
1280      whd in ⊢ (???%);
1281      @(if_then_else_replace ???????? p)
1282      [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1283        cases daemon
1284      |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1285        normalize nodelta
1286        whd in match (addr_of_relative ????);
1287        >set_clock_mk_Status_commutation
1288        [9,10:
1289          (* XXX: demodulation not working in this case *)
1290          >program_counter_set_arg_1 in ⊢ (???%);
1291          >program_counter_set_program_counter in ⊢ (???%);
1292        |*:
1293          /demod/
1294        ]
1295        whd in ⊢ (???%);
1296        change with (add ???) in match (\snd (half_add ???));
1297        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
1298        [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1299          >bitvector_of_nat_sign_extension_equivalence
1300          [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1301            >EQintermediate_pc' %
1302          |*:
1303            repeat @le_S_S @le_O_n
1304          ]
1305        ]
1306        %
1307      ]
1308    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
1309      skip
1310    ]
1311    -status_after_1
1312    @(pose … (execute_1 ? (mk_PreStatus …)))
1313    #status_after_1 #EQstatus_after_1
1314    <(?: ? = status_after_1)
1315    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
1316      >EQstatus_after_1 in ⊢ (???%);
1317      whd in ⊢ (???%);
1318      (* XXX: matita bug with patterns across multiple goals *)
1319      [1: <fetch_refl'' in ⊢ (???%);
1320      |2: <fetch_refl' in ⊢ (???%);
1321      |3: <fetch_refl'' in ⊢ (???%);
1322      |4: <fetch_refl' in ⊢ (???%);
1323      |5: <fetch_refl'' in ⊢ (???%);
1324      |6: <fetch_refl' in ⊢ (???%);
1325      |7: <fetch_refl'' in ⊢ (???%);
1326      |8: <fetch_refl' in ⊢ (???%);
1327      |9: <fetch_refl'' in ⊢ (???%);
1328      |10: <fetch_refl' in ⊢ (???%);
1329      |11: <fetch_refl'' in ⊢ (???%);
1330      |12: <fetch_refl' in ⊢ (???%);
1331      |13: <fetch_refl'' in ⊢ (???%);
1332      |14: <fetch_refl' in ⊢ (???%);
1333      ]
1334      whd in ⊢ (???%);
1335      [9,10:
1336      |*:
1337        /demod/
1338      ] %
1339    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
1340      skip
1341    ]
1342    -status_after_1 whd in ⊢ (??%?);
1343    (* XXX: switch to the right hand side *)
1344    normalize nodelta >EQs -s >EQticks -ticks
1345    whd in ⊢ (??%%);
1346    (* XXX: finally, prove the equality using sigma commutation *)
1347    @split_eq_status try %
1348    [3,11,19,27,36,53,61:
1349      >program_counter_set_program_counter >set_clock_mk_Status_commutation
1350      [5: >program_counter_set_program_counter ]
1351      >EQaddr_of normalize nodelta
1352      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
1353      >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
1354      @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉)
1355      >create_label_cost_refl normalize nodelta #relevant @relevant
1356      whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr))
1357      try assumption whd in match instruction_has_label; normalize nodelta
1358      <instr_refl normalize nodelta %
1359    |7,15,23,31,45,57,65:
1360      >set_clock_mk_Status_commutation >program_counter_set_program_counter
1361      whd in ⊢ (??%?); normalize nodelta
1362      >EQppc in fetch_many_assm; #fetch_many_assm
1363      [5:
1364        >program_counter_set_arg_1 >program_counter_set_program_counter
1365      ]
1366      <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
1367      <bitvector_of_nat_sign_extension_equivalence
1368      [1,3,5,7,9,11,13:
1369        whd in ⊢ (???%); cases (half_add ???) normalize //
1370      |2,4,6,8,10,12,14:
1371        @assembly1_lt_128
1372        @le_S_S @le_O_n
1373      ]
1374    |*:
1375      cases daemon
1376    ]
1377  ]
1378  |4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
1379  (* XXX: work on the right hand side *)
1380  lapply (subaddressing_modein ???)
1381  <EQaddr normalize nodelta #irrelevant
1382  try (>p normalize nodelta)
1383  try (>p1 normalize nodelta)
1384  (* XXX: switch to the left hand side *)
1385  >EQP -P normalize nodelta
1386  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1387  whd in ⊢ (??%?);
1388  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1389  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1390  (* XXX: work on the left hand side *)
1391  [1,2,3,4,5:
1392    generalize in ⊢ (??(???(?%))?);
1393  |6,7,8,9,10,11:
1394    generalize in ⊢ (??(???(?%))?);
1395  |12:
1396    generalize in ⊢ (??(???(?%))?);
1397  ]
1398  <EQaddr normalize nodelta #irrelevant
1399  try @(jmpair_as_replace ?????????? p)
1400  [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
1401  (* XXX: switch to the right hand side *)
1402  normalize nodelta >EQs -s >EQticks -ticks
1403  whd in ⊢ (??%%);
1404  (* XXX: finally, prove the equality using sigma commutation *)
1405  try @split_eq_status try % whd in ⊢ (??%%);
1406  cases daemon
1407  |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
1408  (* XXX: work on the right hand side *)
1409  >p normalize nodelta
1410  try (>p1 normalize nodelta)
1411  (* XXX: switch to the left hand side *)
1412  -instr_refl >EQP -P normalize nodelta
1413  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1414  whd in ⊢ (??%?);
1415  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1416  (* XXX: work on the left hand side *)
1417  @(pair_replace ?????????? p)
1418  [1,3,5,7,9,11,13,15,17:
1419    >set_clock_set_program_counter >set_clock_mk_Status_commutation
1420    >set_program_counter_mk_Status_commutation >clock_set_program_counter
1421    cases daemon
1422  |14,16,18:
1423    normalize nodelta
1424    @(pair_replace ?????????? p1)
1425    [1,3,5:
1426      >set_clock_mk_Status_commutation
1427      cases daemon
1428    ]
1429  ]
1430  (* XXX: switch to the right hand side *)
1431  normalize nodelta >EQs -s >EQticks -ticks
1432  whd in ⊢ (??%%);
1433  (* XXX: finally, prove the equality using sigma commutation *)
1434  try @split_eq_status try %
1435  cases daemon
1436  |10,42,43,44,45,49,52,56: (* MUL *)
1437  (* XXX: work on the right hand side *)
1438  (* XXX: switch to the left hand side *)
1439  -instr_refl >EQP -P normalize nodelta
1440  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1441  whd in ⊢ (??%?);
1442  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1443  (* XXX: work on the left hand side *)
1444  (* XXX: switch to the right hand side *)
1445  normalize nodelta >EQs -s >EQticks -ticks
1446  whd in ⊢ (??%%);
1447  (* XXX: finally, prove the equality using sigma commutation *)
1448  cases daemon
1449  |11,12: (* DIV *)
1450  (* XXX: work on the right hand side *)
1451  normalize nodelta in p;
1452  >p normalize nodelta
1453  (* XXX: switch to the left hand side *)
1454  -instr_refl >EQP -P normalize nodelta
1455  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1456  whd in ⊢ (??%?);
1457  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1458  @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
1459  >(?: pose_assm = 0) normalize nodelta
1460  [2,4:
1461    <p >pose_refl
1462    cases daemon
1463  |1,3:
1464    (* XXX: switch to the right hand side *)
1465    >EQs -s >EQticks -ticks
1466    whd in ⊢ (??%%);
1467    (* XXX: finally, prove the equality using sigma commutation *)
1468    @split_eq_status try %
1469    cases daemon
1470  ]
1471  |13,14,15: (* DA *)
1472  (* XXX: work on the right hand side *)
1473  >p normalize nodelta
1474  >p1 normalize nodelta
1475  try (>p2 normalize nodelta
1476  try (>p3 normalize nodelta
1477  try (>p4 normalize nodelta
1478  try (>p5 normalize nodelta))))
1479  (* XXX: switch to the left hand side *)
1480  -instr_refl >EQP -P normalize nodelta
1481  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1482  whd in ⊢ (??%?);
1483  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1484  (* XXX: work on the left hand side *)
1485  @(pair_replace ?????????? p)
1486  [1,3,5:
1487    /demod/
1488    cases daemon
1489  |2,4,6:
1490    @(if_then_else_replace ???????? p1)
1491    [1,3,5:
1492      cases daemon
1493    |2,4:
1494      normalize nodelta
1495      @(pair_replace ?????????? p2)
1496      [1,3:
1497        cases daemon
1498      |2,4:
1499        normalize nodelta >p3 normalize nodelta
1500        >p4 normalize nodelta try >p5
1501      ]
1502    ]
1503  (* XXX: switch to the right hand side *)
1504  normalize nodelta >EQs -s >EQticks -ticks
1505  whd in ⊢ (??%%);
1506  (* XXX: finally, prove the equality using sigma commutation *)
1507  @split_eq_status try %
1508  cases daemon
1509  ]
1510  |33,34,35,48: (* ANL, ORL, XRL, MOVX *)
1511  (* XXX: work on the right hand side *)
1512  cases addr #addr' normalize nodelta
1513  [1,3:
1514    cases addr' #addr'' normalize nodelta
1515  ]
1516  @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta
1517  (* XXX: switch to the left hand side *)
1518  -instr_refl >EQP -P normalize nodelta
1519  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1520  whd in ⊢ (??%?);
1521  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1522  (* XXX: work on the left hand side *)
1523  (* XXX: switch to the right hand side *)
1524  normalize nodelta >EQs -s >EQticks -ticks
1525  whd in ⊢ (??%%);
1526  (* XXX: finally, prove the equality using sigma commutation *)
1527  cases daemon
1528  |47: (* MOV *)
1529  (* XXX: work on the right hand side *)
1530  cases addr -addr #addr normalize nodelta
1531  [1:
1532    cases addr #addr normalize nodelta
1533    [1:
1534      cases addr #addr normalize nodelta
1535      [1:
1536        cases addr #addr normalize nodelta
1537        [1:
1538          cases addr #addr normalize nodelta
1539        ]
1540      ]
1541    ]
1542  ]
1543  cases addr #lft #rgt normalize nodelta
1544  (* XXX: switch to the left hand side *)
1545  >EQP -P normalize nodelta
1546  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1547  whd in ⊢ (??%?);
1548  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1549  (* XXX: work on the left hand side *)
1550  (* XXX: switch to the right hand side *)
1551  normalize nodelta >EQs -s >EQticks -ticks
1552  whd in ⊢ (??%%);
1553  (* XXX: finally, prove the equality using sigma commutation *)
1554  cases daemon
1555  ]
1556qed.
Note: See TracBrowser for help on using the repository browser.