source: src/ASM/AssemblyProofSplit.ma @ 2168

Last change on this file since 2168 was 2160, checked in by mulligan, 7 years ago

Added a new scratch file Test.ma for working on lemmas that are needed in the massive proof to avoid having to retypecheck everything. Lots of work from the last week on the AssemblyProofSplit?.ma file, as well as an attempt to use Russell-style types on set_arg_8.

File size: 79.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 = data →
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 n_lt_19_elim_prop:
375  ∀P: nat → Prop.
376    P 0 → P 1 → P 2 → P 3 → P 4 → P 5 → P 6 → P 7 → P 8 → P 9 →
377    P 10 → P 11 → P 12 → P 13 → P 14 → P 15 → P 16 → P 17 → P 18 →
378      (∀n. n < 19 → P n).
379  #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14
380  #H15 #H16 #H17 #H18 #H19 #n
381  cases n [1: // ]
382  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
383  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
384  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
385  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
386  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
387  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
388  #n' normalize in ⊢ (% → ?);
389  #absurd repeat (lapply (le_S_S_to_le … absurd) #absurd)
390  cases (lt_to_not_zero … absurd)
391qed.
392
393lemma get_index_v_set_index_miss:
394  ∀T: Type[0].
395  ∀n, i, j: nat.
396  ∀v: Vector T n.
397  ∀b: T.
398  ∀i_proof: i < n.
399  ∀j_proof: j < n.
400  i ≠ j →
401    get_index_v T n (set_index T n v i b i_proof) j j_proof =
402      get_index_v T n v j j_proof.
403  #T #n #i #j #v lapply i lapply j elim v #i #j
404  [1:
405    #b #i_proof
406    cases (lt_to_not_zero … i_proof)
407  |2:
408    #tl #inductive_hypothesis #j' #i' #b #i_proof #j_proof #i_neq_j
409    lapply i_proof lapply i_neq_j cases i'
410    [1:
411      -i_neq_j #i_neq_j -i_proof #i_proof
412      whd in match (set_index ??????);
413      lapply j_proof lapply i_neq_j cases j'
414      [1:
415        #relevant @⊥ cases relevant -relevant #absurd @absurd %
416      |2:
417        #j' #_ -j_proof #j_proof %
418      ]
419    |2:
420      #i' -i_neq_j #i_neq_j -i_proof #i_proof
421      lapply j_proof lapply i_neq_j cases j'
422      [1:
423        #_ #j_proof %
424      |2:
425        #j' #i_neq_j #j_proof
426        @inductive_hypothesis @nmk #relevant
427        cases i_neq_j #absurd @absurd >relevant %
428      ]
429    ]
430  ]
431qed.
432
433lemma get_index_v_special_function_registers_8051_not_acc_a:
434  ∀M: internal_pseudo_address_map.
435  ∀cm: pseudo_assembly_program.
436  ∀s: PreStatus pseudo_assembly_program cm.
437  ∀sigma: Word → Word.
438  ∀policy: Word → bool.
439  ∀n: nat.
440  ∀proof: n < 19.
441    n ≠ 17 →
442   (get_index_v Byte 19
443    (special_function_registers_8051 pseudo_assembly_program cm s) n
444    proof =
445   get_index_v Byte 19
446     (special_function_registers_8051 (BitVectorTrie Byte 16)
447       (code_memory_of_pseudo_assembly_program cm sigma policy)
448       (status_of_pseudo_status M cm s sigma policy)) n
449       proof).
450  #M #cm #s #sigma #policy #n #proof lapply proof
451  @(n_lt_19_elim_prop … proof) -proof #proof
452  [18:
453    #absurd @⊥ cases absurd -absurd #absurd @absurd %
454  ]
455  #_ cases s #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
456  whd in match status_of_pseudo_status; normalize nodelta
457  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
458  cases M #left #right cases right normalize nodelta try %
459  -right * #address
460  @pair_elim #high #low #high_low_refl normalize nodelta
461  whd in match sfr_8051_index; normalize nodelta
462  >get_index_v_set_index_miss try %
463  #absurd destruct(absurd)
464qed.
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
481(* XXX: this needs an extra invariant relating address and word that we look
482        up!
483*)
484definition map_lower_internal_ram_address_using_pseudo_address_map:
485    ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝
486  λM: internal_pseudo_address_map.
487  λsigma: Word → Word.
488  λaddress: Byte.
489  λvalue: Byte.
490  match assoc_list_lookup ?? address (eq_bv …) (\fst M) with
491  [ None ⇒ value
492  | Some upper_lower_word ⇒
493    let 〈upper_lower, word〉 ≝ upper_lower_word in
494    let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in
495      if eq_upper_lower upper_lower upper then
496        high
497      else
498        low
499  ].
500
501lemma get_8051_sfr_status_of_pseudo_status:
502  ∀M.
503  ∀cm, ps, sigma, policy.
504  ∀sfr.
505    (sfr = SFR_ACC_A → \snd M = data) →
506    get_8051_sfr (BitVectorTrie Byte 16)
507      (code_memory_of_pseudo_assembly_program cm sigma policy)
508      (status_of_pseudo_status M cm ps sigma policy) sfr =
509    get_8051_sfr pseudo_assembly_program cm ps sfr.
510  #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant
511  [18:
512     >relevant %
513  ]
514  cases sndM try % * #address
515  whd in match get_8051_sfr;
516  whd in match status_of_pseudo_status; normalize nodelta
517  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
518  @pair_elim #upper #lower #upper_lower_refl
519  @get_index_v_set_index_miss @nmk #relevant
520  normalize in relevant; destruct(relevant)
521qed.
522
523lemma bitvector_cases_hd_tl:
524  ∀n: nat.
525  ∀w: BitVector (S n).
526   ∃hd: bool. ∃tl: BitVector n.
527    w ≃ hd:::tl.
528  #n #w cases (BitVector_Sn … w) #hd #relevant %{hd} @relevant
529qed.
530
531lemma external_ram_set_bit_addressable_sfr:
532  ∀M: Type[0].
533  ∀cm: M.
534  ∀ps.
535  ∀w.
536  ∀result: Byte.
537    external_ram M cm
538      (set_bit_addressable_sfr M cm ps w result) =
539    external_ram M cm ps.
540  #M #cm #ps #w #result cases daemon (* XXX: prove this with Russell in Status.ma!
541  whd in match set_bit_addressable_sfr; normalize nodelta
542  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
543  cases (eqb ??) normalize nodelta [1: % ]
544  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
545  cases (eqb ??) normalize nodelta [1: % ]
546  cases (eqb ??) normalize nodelta [1: % ]
547  cases (eqb ??) normalize nodelta [1: % ]
548  cases (eqb ??) normalize nodelta [1: % ]
549  cases (eqb ??) normalize nodelta [1: % ]
550  cases (eqb ??) normalize nodelta [1: % ]
551  cases (eqb ??) normalize nodelta [1: % ]
552  cases (eqb ??) normalize nodelta [1: % ]
553  cases (eqb ??) normalize nodelta [1: % ]
554  cases (eqb ??) normalize nodelta [1: % ]
555  cases (eqb ??) normalize nodelta [1: % ]
556  cases (eqb ??) normalize nodelta [1: % ]
557  cases (eqb ??) normalize nodelta [1: % ]
558  cases (eqb ??) normalize nodelta [1: % ]
559  cases (eqb ??) normalize nodelta [1: % ]
560  cases (eqb ??) normalize nodelta [1: % ]
561  cases (eqb ??) normalize nodelta [1: % ]
562  cases (eqb ??) normalize nodelta [1: % ]
563  cases (eqb ??) normalize nodelta [1: % ]
564  cases (eqb ??) normalize nodelta [1: % ]
565  cases (eqb ??) normalize nodelta [1: % ]
566  cases (eqb ??) normalize nodelta [1: % ]
567  cases (eqb ??) normalize nodelta [1: % ]
568  cases not_implemented *)
569qed.
570
571lemma external_ram_set_arg_8:
572  ∀M: Type[0].
573  ∀cm: M.
574  ∀ps.
575  ∀addr1: [[direct; indirect; registr; acc_a; acc_b ]].
576  ∀result.
577    external_ram M cm (set_arg_8 M cm ps addr1 result) =
578      external_ram M cm ps.
579  [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
580  #M #cm #ps #addr1 #result
581  @(subaddressing_mode_elim … addr1) try #w try %
582  whd in ⊢ (??(???%)?); whd in ⊢ (??(???(???%))?); (* XXX: to be understood, slow match *)
583  [1:
584    cases (vsplit bool ???) #nu #nl normalize nodelta
585    cases (vsplit bool ???) #ignore #three_bits normalize nodelta
586    cases (get_index_v bool ????) normalize nodelta try %
587    @external_ram_set_bit_addressable_sfr
588  |2:
589    cases (vsplit bool ???) #nu #nl normalize nodelta
590    cases (vsplit bool ???) #ignore #three_bits normalize nodelta
591    cases (get_index_v bool ????) normalize nodelta %
592  ]
593qed.
594
595lemma special_function_registers_8051_set_clock:
596  ∀M: Type[0].
597  ∀cm: M.
598  ∀ps.
599  ∀t.
600    special_function_registers_8051 M cm (set_clock M cm ps t) =
601      special_function_registers_8051 M cm ps.
602  //
603qed.
604
605lemma get_arg_8_pseudo_addressing_mode_ok:
606  ∀M: internal_pseudo_address_map.
607  ∀cm: pseudo_assembly_program.
608  ∀ps: PreStatus pseudo_assembly_program cm.
609  ∀sigma: Word → Word.
610  ∀policy: Word → bool.
611  ∀addr1: [[registr; direct]].
612    addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →
613      get_arg_8 (BitVectorTrie Byte 16)
614        (code_memory_of_pseudo_assembly_program cm sigma policy)
615        (status_of_pseudo_status M cm ps sigma policy) true addr1 =
616      get_arg_8 pseudo_assembly_program cm ps true addr1.
617  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
618  #M #cm #ps #sigma #policy #addr1
619  @(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%);
620  [1:
621    whd in ⊢ (??%? → ??%?);
622    whd in match bit_address_of_register; normalize nodelta
623    @pair_elim #un #ln #un_ln_refl
624    lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
625    @(pair_replace ?????????? un_ln_refl)
626    [1:
627      whd in match get_8051_sfr; normalize nodelta
628      whd in match sfr_8051_index; normalize nodelta
629      @eq_f <get_index_v_special_function_registers_8051_not_acc_a
630      try % #absurd destruct(absurd)
631    |2:
632      #assembly_mode_ok_refl
633      >low_internal_ram_of_pseudo_internal_ram_miss
634      [1:
635        %
636      |2:
637        cases (assoc_list_exists ?????) in assembly_mode_ok_refl; normalize nodelta
638        #absurd try % @sym_eq assumption
639      ]
640    ]
641  |2:
642    #addressing_mode_ok_refl whd in ⊢ (??%?);
643    @pair_elim #nu #nl #nu_nl_refl normalize nodelta
644    @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
645    inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
646    [1:
647      whd in ⊢ (??%%); normalize nodelta
648      cases (eqb ??) normalize nodelta [1: % ]
649      cases (eqb ??) normalize nodelta [1: % ]
650      cases (eqb ??) normalize nodelta [1: % ]
651      cases (eqb ??) normalize nodelta [1: % ]
652      cases (eqb ??) normalize nodelta [1:
653        @get_8051_sfr_status_of_pseudo_status
654        #absurd destruct(absurd)
655      ]
656      cases (eqb ??) normalize nodelta [1:
657        @get_8051_sfr_status_of_pseudo_status
658        #absurd destruct(absurd)
659      ]
660      cases (eqb ??) normalize nodelta [1:
661        @get_8051_sfr_status_of_pseudo_status
662        #absurd destruct(absurd)
663      ]
664      cases (eqb ??) normalize nodelta [1:
665        @get_8051_sfr_status_of_pseudo_status
666        #absurd destruct(absurd)
667      ]
668      cases (eqb ??) normalize nodelta [1:
669        @get_8051_sfr_status_of_pseudo_status
670        #absurd destruct(absurd)
671      ]
672      cases (eqb ??) normalize nodelta [1: % ]
673      cases (eqb ??) normalize nodelta [1: % ]
674      cases (eqb ??) normalize nodelta [1: % ]
675      cases (eqb ??) normalize nodelta [1: % ]
676      cases (eqb ??) normalize nodelta [1: % ]
677      cases (eqb ??) normalize nodelta [1:
678        @get_8051_sfr_status_of_pseudo_status
679        #absurd destruct(absurd)
680      ]
681      cases (eqb ??) normalize nodelta [1:
682        @get_8051_sfr_status_of_pseudo_status
683        #absurd destruct(absurd)
684      ]
685      cases (eqb ??) normalize nodelta [1:
686        @get_8051_sfr_status_of_pseudo_status
687        #absurd destruct(absurd)
688      ]
689      cases (eqb ??) normalize nodelta [1:
690        @get_8051_sfr_status_of_pseudo_status
691        #absurd destruct(absurd)
692      ]
693      cases (eqb ??) normalize nodelta [1:
694        @get_8051_sfr_status_of_pseudo_status
695        #absurd destruct(absurd)
696      ]
697      cases (eqb ??) normalize nodelta [1:
698        @get_8051_sfr_status_of_pseudo_status
699        #absurd destruct(absurd)
700      ]
701      cases (eqb ??) normalize nodelta [1:
702        @get_8051_sfr_status_of_pseudo_status
703        #absurd destruct(absurd)
704      ]
705      cases (eqb ??) normalize nodelta [1:
706        @get_8051_sfr_status_of_pseudo_status
707        #absurd destruct(absurd)
708      ]
709      cases (eqb ??) normalize nodelta [1:
710        @get_8051_sfr_status_of_pseudo_status
711        #absurd destruct(absurd)
712      ]
713      cases (eqb ??) normalize nodelta [1:
714        @get_8051_sfr_status_of_pseudo_status
715        #absurd destruct(absurd)
716      ]
717      inversion (eqb ??) #eqb_refl normalize nodelta [1:
718        @get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl
719        whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl)
720        >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
721        #assoc_list_assm cases (conjunction_true … assoc_list_assm) #_
722        #relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) %
723      ]
724      cases (eqb ??) normalize nodelta [1:
725        @get_8051_sfr_status_of_pseudo_status
726        #absurd destruct(absurd)
727      ] %
728    |2:
729      lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant
730      whd in match status_of_pseudo_status; normalize nodelta
731      >low_internal_ram_of_pseudo_internal_ram_miss try %
732      cut(arg = false:::(three_bits@@nl))
733      [1:
734        <get_index_v_refl
735        cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits)
736        [1:
737          cut(ignore = [[get_index_v bool 4 nu 0 ?]])
738          [1:
739            @le_S_S @le_O_n
740          |2:
741            cut(ignore = \fst (vsplit bool 1 3 nu))
742            [1:
743              >ignore_three_bits_refl %
744            |2:
745              #ignore_refl >ignore_refl
746              cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl
747              >nu_refl %
748            ]
749          |3:
750            #ignore_refl >ignore_refl in ignore_three_bits_refl;
751            #relevant lapply (vsplit_ok ?????? (sym_eq … relevant))
752            #nu_refl <nu_refl %
753          ]
754        |2:
755          #nu_refl change with (? = (?:::three_bits)@@?) <nu_refl
756          @sym_eq @vsplit_ok >nu_nl_refl %
757        ]
758      |2:
759        #arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant;
760        normalize nodelta
761        [1:
762          cases (eq_bv ???) normalize #absurd destruct(absurd)
763        |2:
764          #_ %
765        ]
766      ]
767    ]
768  ]
769qed.
770
771lemma special_function_registers_8051_set_program_counter:
772  ∀M: Type[0].
773  ∀cm: M.
774  ∀ps.
775  ∀pc: Word.
776    special_function_registers_8051 M cm (set_program_counter M cm ps pc) =
777      special_function_registers_8051 M cm ps.
778  //
779qed.
780
781lemma special_function_registers_8052_set_program_counter:
782  ∀M: Type[0].
783  ∀cm: M.
784  ∀ps.
785  ∀pc: Word.
786    special_function_registers_8052 M cm (set_program_counter M cm ps pc) =
787      special_function_registers_8052 M cm ps.
788  //
789qed.
790
791lemma set_index_set_index_commutation:
792  ∀A: Type[0].
793  ∀n: nat.
794  ∀v: Vector A n.
795  ∀m, o: nat.
796  ∀m_lt_proof: m < n.
797  ∀o_lt_proof: o < n.
798  ∀e, f: A.
799    m ≠ o →
800      set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof =
801        set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof.
802  #A #n #v elim v
803  [1:
804    #m #o #m_lt_proof
805    normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof)
806  |2:
807    #n' #hd #tl #inductive_hypothesis
808    #m #o
809    cases m cases o
810    [1:
811      #m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant
812      @relevant %
813    |2,3:
814      #o' normalize //
815    |4:
816      #m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm
817      normalize @eq_f @inductive_hypothesis @nmk #relevant
818      >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) %
819    ]
820  ]
821qed.
822
823lemma special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051:
824  ∀M: internal_pseudo_address_map.
825  ∀cm: pseudo_assembly_program.
826  ∀ps.
827  ∀sigma: Word → Word.
828  ∀policy: Word → bool.
829  ∀sfr.
830  ∀result: Byte.
831    eqb (sfr_8051_index sfr) (sfr_8051_index SFR_ACC_A) = false →
832      special_function_registers_8051 (BitVectorTrie Byte 16)
833        (code_memory_of_pseudo_assembly_program cm sigma policy)
834        (set_8051_sfr (BitVectorTrie Byte 16)
835        (code_memory_of_pseudo_assembly_program cm sigma policy)
836        (status_of_pseudo_status M cm ps sigma policy) sfr result) =
837      sfr_8051_of_pseudo_sfr_8051 M
838        (special_function_registers_8051 pseudo_assembly_program cm
839        (set_8051_sfr pseudo_assembly_program cm ps sfr result)) sigma.
840  #M #cm #ps #sigma #policy #sfr #result #sfr_neq_assm
841  whd in match (set_8051_sfr ?????);
842  cases M #callM * try % #upper_lower #address
843  whd in match (special_function_registers_8051 ???);
844  whd in match (sfr_8051_of_pseudo_sfr_8051 ???);
845  @pair_elim #high #low #high_low_refl normalize nodelta
846  cases (eq_upper_lower ??) normalize nodelta
847  whd in match (set_8051_sfr ?????);
848  @set_index_set_index_commutation @nmk #relevant
849  @(absurd ? relevant (eqb_false_to_not_eq ?? sfr_neq_assm))
850qed.
851
852lemma special_function_registers_8051_set_arg_8:
853  ∀M: internal_pseudo_address_map.
854  ∀cm: pseudo_assembly_program.
855  ∀ps.
856  ∀sigma: Word → Word.
857  ∀policy: Word → bool.
858  ∀addr1: [[ registr; direct ]].
859  ∀result.
860    addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →
861    special_function_registers_8051 (BitVectorTrie Byte 16)
862      (code_memory_of_pseudo_assembly_program cm sigma policy)
863      (set_arg_8 (BitVectorTrie Byte 16)
864        (code_memory_of_pseudo_assembly_program cm sigma policy)
865        (status_of_pseudo_status M cm ps sigma policy) addr1 result) =
866   sfr_8051_of_pseudo_sfr_8051 M
867     (special_function_registers_8051 pseudo_assembly_program cm
868     (set_arg_8 pseudo_assembly_program cm ps addr1 result)) sigma.
869  cases daemon
870(*
871  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
872  #M #cm #ps #sigma #policy #addr1 #result
873  @(subaddressing_mode_elim … addr1) #w #addressing_mode_ok_refl try %
874  whd in match (set_arg_8 ?????); whd in ⊢ (??(???(???%))?);
875  whd in match (set_arg_8 ?????) in ⊢ (???%); whd in ⊢ (???(??(???(???%))?));
876  cases (vsplit bool ???) #nu #nl normalize nodelta
877  cases (vsplit bool ???) #ignore #three_bits normalize nodelta
878  cases (get_index_v bool ????) normalize nodelta try %
879  whd in match (set_bit_addressable_sfr ?????); whd in match (set_bit_addressable_sfr ?????) in ⊢ (???%);
880  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
881  cases (eqb ??) normalize nodelta [1: % ]
882  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
883  cases (eqb ??) normalize nodelta [1: % ]
884  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
885  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
886  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
887  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
888  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
889  cases (eqb ??) normalize nodelta [1: % ]
890  cases (eqb ??) normalize nodelta [1: % ]
891  cases (eqb ??) normalize nodelta [1: % ]
892  cases (eqb ??) normalize nodelta [1: % ]
893  cases (eqb ??) normalize nodelta [1: % ]
894  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
895  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
896  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
897  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
898  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
899  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
900  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
901  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
902  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
903  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
904  inversion (eqb ??) #eqb_refl normalize nodelta [1:
905    whd in addressing_mode_ok_refl:(??%?); <(eqb_true_to_eq … eqb_refl) in addressing_mode_ok_refl;
906    >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
907    #relevant cases (conjunction_true … relevant) #_ #eq_acc_assm
908    whd in match (status_of_pseudo_status ?????);
909    whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
910    >(eq_accumulator_address_map_entry_true_to_eq … eq_acc_assm) normalize nodelta %
911  ]
912  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
913  cases not_implemented *)
914qed.
915
916include alias "ASM/Vector.ma".
917
918lemma main_lemma_preinstruction:
919  ∀M, M': internal_pseudo_address_map.
920  ∀preamble: preamble.
921  ∀instr_list: list labelled_instruction.
922  ∀cm: pseudo_assembly_program.
923  ∀EQcm: cm = 〈preamble, instr_list〉.
924  ∀is_well_labelled_witness: is_well_labelled_p instr_list.
925  ∀sigma: Word → Word.
926  ∀policy: Word → bool.
927  ∀sigma_policy_witness: sigma_policy_specification cm sigma policy.
928  ∀ps: PseudoStatus cm.
929  ∀ppc: Word.
930  ∀program_counter_in_bounds_witness: nat_of_bitvector … ppc < |instr_list|.
931  ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps.
932  ∀labels: label_map.
933  ∀costs: BitVectorTrie costlabel 16.
934  ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉.
935  ∀newppc: Word.
936  ∀lookup_labels: Identifier → Word.
937  ∀EQlookup_labels: lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)).
938  ∀lookup_datalabels: Identifier → Word.
939  ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
940  ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1).
941  ∀instr: preinstruction Identifier.
942  ∀fetch_pseudo_refl: \fst  (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr.
943  ∀ticks: nat × nat.
944  ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_datalabels sigma policy ppc (Instruction instr).
945  ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
946  ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x).
947  ∀s: PreStatus pseudo_assembly_program cm.
948  ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))).
949  ∀P: preinstruction Identifier → PseudoStatus cm → Prop.
950  ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc)
951              (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
952                  lookup_datalabels (Instruction instr)))) →
953              next_internal_pseudo_address_map0 ? cm addr_of (Instruction instr) M ps = Some internal_pseudo_address_map M' →
954                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))
955                  (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) →
956                    ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) =
957                      status_of_pseudo_status M' cm s sigma policy).
958    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
959  (* XXX: takes about 45 minutes to type check! *)
960  #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
961  #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
962  #costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels
963  #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr #fetch_pseudo_refl
964  #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
965  (*#sigma_increment_commutation #maps_assm #fetch_many_assm *)
966  letin a ≝ Identifier letin m ≝ pseudo_assembly_program
967  cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s))
968  [2: * // ]
969  @(
970  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
971  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
972  match instr in preinstruction return λx. x = instr → Σs'.? with
973        [ ADD addr1 addr2 ⇒ λinstr_refl.
974            let s ≝ add_ticks1 s in
975            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
976                                                   (get_arg_8 … s false addr2) false in
977            let cy_flag ≝ get_index' ? O  ? flags in
978            let ac_flag ≝ get_index' ? 1 ? flags in
979            let ov_flag ≝ get_index' ? 2 ? flags in
980            let s ≝ set_arg_8 … s ACC_A result in
981              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
982        | ADDC addr1 addr2 ⇒ λinstr_refl.
983            let s ≝ add_ticks1 s in
984            let old_cy_flag ≝ get_cy_flag ?? s in
985            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
986                                                   (get_arg_8 … s false addr2) old_cy_flag in
987            let cy_flag ≝ get_index' ? O ? flags in
988            let ac_flag ≝ get_index' ? 1 ? flags in
989            let ov_flag ≝ get_index' ? 2 ? flags in
990            let s ≝ set_arg_8 … s ACC_A result in
991              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
992        | SUBB addr1 addr2 ⇒ λinstr_refl.
993            let s ≝ add_ticks1 s in
994            let old_cy_flag ≝ get_cy_flag ?? s in
995            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
996                                                   (get_arg_8 … s false addr2) old_cy_flag in
997            let cy_flag ≝ get_index' ? O ? flags in
998            let ac_flag ≝ get_index' ? 1 ? flags in
999            let ov_flag ≝ get_index' ? 2 ? flags in
1000            let s ≝ set_arg_8 … s ACC_A result in
1001              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
1002        | ANL addr ⇒ λinstr_refl.
1003          let s ≝ add_ticks1 s in
1004          match addr with
1005            [ inl l ⇒
1006              match l with
1007                [ inl l' ⇒
1008                  let 〈addr1, addr2〉 ≝ l' in
1009                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
1010                    set_arg_8 … s addr1 and_val
1011                | inr r ⇒
1012                  let 〈addr1, addr2〉 ≝ r in
1013                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
1014                    set_arg_8 … s addr1 and_val
1015                ]
1016            | inr r ⇒
1017              let 〈addr1, addr2〉 ≝ r in
1018              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
1019               set_flags … s and_val (None ?) (get_ov_flag ?? s)
1020            ]
1021        | ORL addr ⇒ λinstr_refl.
1022          let s ≝ add_ticks1 s in
1023          match addr with
1024            [ inl l ⇒
1025              match l with
1026                [ inl l' ⇒
1027                  let 〈addr1, addr2〉 ≝ l' in
1028                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
1029                    set_arg_8 … s addr1 or_val
1030                | inr r ⇒
1031                  let 〈addr1, addr2〉 ≝ r in
1032                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
1033                    set_arg_8 … s addr1 or_val
1034                ]
1035            | inr r ⇒
1036              let 〈addr1, addr2〉 ≝ r in
1037              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
1038               set_flags … s or_val (None ?) (get_ov_flag … s)
1039            ]
1040        | XRL addr ⇒ λinstr_refl.
1041          let s ≝ add_ticks1 s in
1042          match addr with
1043            [ inl l' ⇒
1044              let 〈addr1, addr2〉 ≝ l' in
1045              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
1046                set_arg_8 … s addr1 xor_val
1047            | inr r ⇒
1048              let 〈addr1, addr2〉 ≝ r in
1049              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
1050                set_arg_8 … s addr1 xor_val
1051            ]
1052        | INC addr ⇒ λinstr_refl.
1053            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → Σs': PreStatus m cm. ? with
1054              [ ACC_A ⇒ λacc_a: True. λEQaddr.
1055                let s' ≝ add_ticks1 s in
1056                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
1057                 set_arg_8 … s' ACC_A result
1058              | REGISTER r ⇒ λregister: True. λEQaddr.
1059                let s' ≝ add_ticks1 s in
1060                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
1061                 set_arg_8 … s' (REGISTER r) result
1062              | DIRECT d ⇒ λdirect: True. λEQaddr.
1063                let s' ≝ add_ticks1 s in
1064                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
1065                 set_arg_8 … s' (DIRECT d) result
1066              | INDIRECT i ⇒ λindirect: True. λEQaddr.
1067                let s' ≝ add_ticks1 s in
1068                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
1069                 set_arg_8 … s' (INDIRECT i) result
1070              | DPTR ⇒ λdptr: True. λEQaddr.
1071                let s' ≝ add_ticks1 s in
1072                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
1073                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
1074                let s ≝ set_8051_sfr … s' SFR_DPL bl in
1075                 set_8051_sfr … s' SFR_DPH bu
1076              | _ ⇒ λother: False. ⊥
1077              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
1078        | NOP ⇒ λinstr_refl.
1079           let s ≝ add_ticks2 s in
1080            s
1081        | DEC addr ⇒ λinstr_refl.
1082           let s ≝ add_ticks1 s in
1083           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
1084             set_arg_8 … s addr result
1085        | MUL addr1 addr2 ⇒ λinstr_refl.
1086           let s ≝ add_ticks1 s in
1087           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
1088           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
1089           let product ≝ acc_a_nat * acc_b_nat in
1090           let ov_flag ≝ product ≥ 256 in
1091           let low ≝ bitvector_of_nat 8 (product mod 256) in
1092           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
1093           let s ≝ set_8051_sfr … s SFR_ACC_A low in
1094             set_8051_sfr … s SFR_ACC_B high
1095        | DIV addr1 addr2 ⇒ λinstr_refl.
1096           let s ≝ add_ticks1 s in
1097           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
1098           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
1099             match acc_b_nat with
1100               [ O ⇒ set_flags … s false (None Bit) true
1101               | S o ⇒
1102                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
1103                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
1104                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
1105                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
1106                   set_flags … s false (None Bit) false
1107               ]
1108        | DA addr ⇒ λinstr_refl.
1109            let s ≝ add_ticks1 s in
1110            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
1111              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
1112                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
1113                let cy_flag ≝ get_index' ? O ? flags in
1114                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
1115                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
1116                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
1117                    let new_acc ≝ nu @@ acc_nl' in
1118                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
1119                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
1120                  else
1121                    s
1122              else
1123                s
1124        | CLR addr ⇒ λinstr_refl.
1125          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
1126            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
1127              let s ≝ add_ticks1 s in
1128               set_arg_8 … s ACC_A (zero 8)
1129            | CARRY ⇒ λcarry: True.  λEQaddr.
1130              let s ≝ add_ticks1 s in
1131               set_arg_1 … s CARRY false
1132            | BIT_ADDR b ⇒ λbit_addr: True.  λEQaddr.
1133              let s ≝ add_ticks1 s in
1134               set_arg_1 … s (BIT_ADDR b) false
1135            | _ ⇒ λother: False. ⊥
1136            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
1137        | CPL addr ⇒ λinstr_refl.
1138          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
1139            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
1140                let s ≝ add_ticks1 s in
1141                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
1142                let new_acc ≝ negation_bv ? old_acc in
1143                 set_8051_sfr … s SFR_ACC_A new_acc
1144            | CARRY ⇒ λcarry: True. λEQaddr.
1145                let s ≝ add_ticks1 s in
1146                let old_cy_flag ≝ get_arg_1 … s CARRY true in
1147                let new_cy_flag ≝ ¬old_cy_flag in
1148                 set_arg_1 … s CARRY new_cy_flag
1149            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
1150                let s ≝ add_ticks1 s in
1151                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
1152                let new_bit ≝ ¬old_bit in
1153                 set_arg_1 … s (BIT_ADDR b) new_bit
1154            | _ ⇒ λother: False. ?
1155            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
1156        | SETB b ⇒ λinstr_refl.
1157            let s ≝ add_ticks1 s in
1158            set_arg_1 … s b false
1159        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
1160            let s ≝ add_ticks1 s in
1161            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
1162            let new_acc ≝ rotate_left … 1 old_acc in
1163              set_8051_sfr … s SFR_ACC_A new_acc
1164        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
1165            let s ≝ add_ticks1 s in
1166            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
1167            let new_acc ≝ rotate_right … 1 old_acc in
1168              set_8051_sfr … s SFR_ACC_A new_acc
1169        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
1170            let s ≝ add_ticks1 s in
1171            let old_cy_flag ≝ get_cy_flag ?? s in
1172            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
1173            let new_cy_flag ≝ get_index' ? O ? old_acc in
1174            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
1175            let s ≝ set_arg_1 … s CARRY new_cy_flag in
1176              set_8051_sfr … s SFR_ACC_A new_acc
1177        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
1178            let s ≝ add_ticks1 s in
1179            let old_cy_flag ≝ get_cy_flag ?? s in
1180            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
1181            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
1182            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
1183            let s ≝ set_arg_1 … s CARRY new_cy_flag in
1184              set_8051_sfr … s SFR_ACC_A new_acc
1185        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
1186            let s ≝ add_ticks1 s in
1187            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
1188            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
1189            let new_acc ≝ nl @@ nu in
1190              set_8051_sfr … s SFR_ACC_A new_acc
1191        | PUSH addr ⇒ λinstr_refl.
1192            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → Σs': PreStatus m cm. ? with
1193              [ DIRECT d ⇒ λdirect: True. λEQaddr.
1194                let s ≝ add_ticks1 s in
1195                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
1196                let s ≝ set_8051_sfr … s SFR_SP new_sp in
1197                  write_at_stack_pointer … s d
1198              | _ ⇒ λother: False. ⊥
1199              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
1200        | POP addr ⇒ λinstr_refl.
1201            let s ≝ add_ticks1 s in
1202            let contents ≝ read_at_stack_pointer ?? s in
1203            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
1204            let s ≝ set_8051_sfr … s SFR_SP new_sp in
1205              set_arg_8 … s addr contents
1206        | XCH addr1 addr2 ⇒ λinstr_refl.
1207            let s ≝ add_ticks1 s in
1208            let old_addr ≝ get_arg_8 … s false addr2 in
1209            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
1210            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
1211              set_arg_8 … s addr2 old_acc
1212        | XCHD addr1 addr2 ⇒ λinstr_refl.
1213            let s ≝ add_ticks1 s in
1214            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
1215            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
1216            let new_acc ≝ acc_nu @@ arg_nl in
1217            let new_arg ≝ arg_nu @@ acc_nl in
1218            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
1219              set_arg_8 … s addr2 new_arg
1220        | RET ⇒ λinstr_refl.
1221            let s ≝ add_ticks1 s in
1222            let high_bits ≝ read_at_stack_pointer ?? s in
1223            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
1224            let s ≝ set_8051_sfr … s SFR_SP new_sp in
1225            let low_bits ≝ read_at_stack_pointer ?? s in
1226            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
1227            let s ≝ set_8051_sfr … s SFR_SP new_sp in
1228            let new_pc ≝ high_bits @@ low_bits in
1229              set_program_counter … s new_pc
1230        | RETI ⇒ λinstr_refl.
1231            let s ≝ add_ticks1 s in
1232            let high_bits ≝ read_at_stack_pointer ?? s in
1233            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
1234            let s ≝ set_8051_sfr … s SFR_SP new_sp in
1235            let low_bits ≝ read_at_stack_pointer ?? s in
1236            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
1237            let s ≝ set_8051_sfr … s SFR_SP new_sp in
1238            let new_pc ≝ high_bits @@ low_bits in
1239              set_program_counter … s new_pc
1240        | MOVX addr ⇒ λinstr_refl.
1241          let s ≝ add_ticks1 s in
1242          (* DPM: only copies --- doesn't affect I/O *)
1243          match addr with
1244            [ inl l ⇒
1245              let 〈addr1, addr2〉 ≝ l in
1246                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
1247            | inr r ⇒
1248              let 〈addr1, addr2〉 ≝ r in
1249                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
1250            ]
1251        | MOV addr ⇒ λinstr_refl.
1252          let s ≝ add_ticks1 s in
1253          match addr with
1254            [ inl l ⇒
1255              match l with
1256                [ inl l' ⇒
1257                  match l' with
1258                    [ inl l'' ⇒
1259                      match l'' with
1260                        [ inl l''' ⇒
1261                          match l''' with
1262                            [ inl l'''' ⇒
1263                              let 〈addr1, addr2〉 ≝ l'''' in
1264                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
1265                            | inr r'''' ⇒
1266                              let 〈addr1, addr2〉 ≝ r'''' in
1267                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
1268                            ]
1269                        | inr r''' ⇒
1270                          let 〈addr1, addr2〉 ≝ r''' in
1271                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
1272                        ]
1273                    | inr r'' ⇒
1274                      let 〈addr1, addr2〉 ≝ r'' in
1275                       set_arg_16 … s (get_arg_16 … s addr2) addr1
1276                    ]
1277                | inr r ⇒
1278                  let 〈addr1, addr2〉 ≝ r in
1279                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
1280                ]
1281            | inr r ⇒
1282              let 〈addr1, addr2〉 ≝ r in
1283               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
1284            ]
1285          | JC addr ⇒ λinstr_refl.
1286                  if get_cy_flag ?? s then
1287                    let s ≝ add_ticks1 s in
1288                      set_program_counter … s (addr_of addr s)
1289                  else
1290                    let s ≝ add_ticks2 s in
1291                      s
1292            | JNC addr ⇒ λinstr_refl.
1293                  if ¬(get_cy_flag ?? s) then
1294                   let s ≝ add_ticks1 s in
1295                     set_program_counter … s (addr_of addr s)
1296                  else
1297                   let s ≝ add_ticks2 s in
1298                    s
1299            | JB addr1 addr2 ⇒ λinstr_refl.
1300                  if get_arg_1 … s addr1 false then
1301                   let s ≝ add_ticks1 s in
1302                    set_program_counter … s (addr_of addr2 s)
1303                  else
1304                   let s ≝ add_ticks2 s in
1305                    s
1306            | JNB addr1 addr2 ⇒ λinstr_refl.
1307                  if ¬(get_arg_1 … s addr1 false) then
1308                   let s ≝ add_ticks1 s in
1309                    set_program_counter … s (addr_of addr2 s)
1310                  else
1311                   let s ≝ add_ticks2 s in
1312                    s
1313            | JBC addr1 addr2 ⇒ λinstr_refl.
1314                  let s ≝ set_arg_1 … s addr1 false in
1315                    if get_arg_1 … s addr1 false then
1316                     let s ≝ add_ticks1 s in
1317                      set_program_counter … s (addr_of addr2 s)
1318                    else
1319                     let s ≝ add_ticks2 s in
1320                      s
1321            | JZ addr ⇒ λinstr_refl.
1322                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
1323                     let s ≝ add_ticks1 s in
1324                      set_program_counter … s (addr_of addr s)
1325                    else
1326                     let s ≝ add_ticks2 s in
1327                      s
1328            | JNZ addr ⇒ λinstr_refl.
1329                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
1330                     let s ≝ add_ticks1 s in
1331                      set_program_counter … s (addr_of addr s)
1332                    else
1333                     let s ≝ add_ticks2 s in
1334                      s
1335            | CJNE addr1 addr2 ⇒ λinstr_refl.
1336                  match addr1 with
1337                    [ inl l ⇒
1338                        let 〈addr1, addr2'〉 ≝ l in
1339                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
1340                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
1341                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
1342                            let s ≝ add_ticks1 s in
1343                            let s ≝ set_program_counter … s (addr_of addr2 s) in
1344                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
1345                          else
1346                            let s ≝ add_ticks2 s in
1347                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
1348                    | inr r' ⇒
1349                        let 〈addr1, addr2'〉 ≝ r' in
1350                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
1351                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
1352                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
1353                            let s ≝ add_ticks1 s in
1354                            let s ≝ set_program_counter … s (addr_of addr2 s) in
1355                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
1356                          else
1357                            let s ≝ add_ticks2 s in
1358                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
1359                    ]
1360            | DJNZ addr1 addr2 ⇒ λinstr_refl.
1361              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
1362              let s ≝ set_arg_8 … s addr1 result in
1363                if ¬(eq_bv ? result (zero 8)) then
1364                 let s ≝ add_ticks1 s in
1365                  set_program_counter … s (addr_of addr2 s)
1366                else
1367                 let s ≝ add_ticks2 s in
1368                  s
1369           ] (refl … instr))
1370  try cases other
1371  try assumption (*20s*)
1372  try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
1373  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
1374  whd in match execute_1_preinstruction; normalize nodelta
1375  [31,32: (* DJNZ *)
1376  (* XXX: work on the right hand side *)
1377  >p normalize nodelta >p1 normalize nodelta
1378  (* XXX: switch to the left hand side *)
1379  >EQP -P normalize nodelta
1380  #sigma_increment_commutation #maps_assm #fetch_many_assm
1381  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1382  <EQppc in fetch_many_assm;
1383  whd in match (short_jump_cond ??);
1384  @pair_elim #sj_possible #disp
1385  @pair_elim #result #flags #sub16_refl
1386  @pair_elim #upper #lower #vsplit_refl
1387  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
1388  #sj_possible_pair destruct(sj_possible_pair)
1389  >p1 normalize nodelta
1390  [1,3:
1391    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
1392    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
1393    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
1394    whd in ⊢ (??%?);
1395    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1396    lapply maps_assm whd in ⊢ (??%? → ?);
1397    inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta
1398    [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl -M'
1399    (* XXX: work on the left hand side *)
1400    @(pair_replace ?????????? p) normalize nodelta
1401    [1,3:
1402      >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1)
1403      [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1404      >(get_arg_8_set_program_counter … true addr1)
1405      [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1406      @get_arg_8_pseudo_addressing_mode_ok assumption
1407    |2,4:
1408      >p1 normalize nodelta >EQs
1409      alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)".
1410      >set_program_counter_status_of_pseudo_status
1411       whd in ⊢ (??%%);
1412      @split_eq_status
1413      [1,10:
1414        whd in ⊢ (??%%); >set_arg_8_set_program_counter
1415        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1416        >low_internal_ram_set_program_counter
1417        [1:
1418          >low_internal_ram_set_program_counter
1419          (* XXX: ??? *)
1420        |2:
1421          >low_internal_ram_set_clock
1422          (* XXX: ??? *)
1423        ]
1424      |2,11:
1425        whd in ⊢ (??%%); >set_arg_8_set_program_counter
1426        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1427        >high_internal_ram_set_program_counter
1428        [1:
1429          >high_internal_ram_set_program_counter
1430          (* XXX: ??? *)
1431        |2:
1432          >high_internal_ram_set_clock
1433          (* XXX: ??? *)
1434        ]
1435      |3,12:
1436        whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%);
1437        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1438        >(external_ram_set_arg_8 ??? addr1)
1439        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
1440      |4,13:
1441        whd in ⊢ (??%%); >EQaddr_of normalize nodelta
1442        [1:
1443          >program_counter_set_program_counter
1444          >set_arg_8_set_program_counter
1445          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1446          >set_clock_set_program_counter >program_counter_set_program_counter
1447          change with (add ??? = ?)
1448          (* XXX: ??? *)
1449        |2:
1450          >set_arg_8_set_program_counter
1451          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1452          >program_counter_set_program_counter
1453          >set_arg_8_set_program_counter
1454          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1455          >set_clock_set_program_counter >program_counter_set_program_counter
1456          >sigma_increment_commutation <EQppc
1457          whd in match (assembly_1_pseudoinstruction ??????);
1458          whd in match (expand_pseudo_instruction ??????);
1459          (* XXX: ??? *)
1460        ]
1461      |5,14:
1462        whd in match (special_function_registers_8051 ???);
1463        [1:
1464          >special_function_registers_8051_set_program_counter
1465          >special_function_registers_8051_set_clock
1466          >set_arg_8_set_program_counter in ⊢ (???%);
1467          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1468          >special_function_registers_8051_set_program_counter
1469          >set_arg_8_set_program_counter
1470          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1471          >special_function_registers_8051_set_program_counter
1472          @special_function_registers_8051_set_arg_8 assumption
1473        |2:
1474          >special_function_registers_8051_set_clock
1475          >set_arg_8_set_program_counter
1476          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1477          >set_arg_8_set_program_counter
1478          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1479          >special_function_registers_8051_set_program_counter
1480          >special_function_registers_8051_set_program_counter
1481          @special_function_registers_8051_set_arg_8 assumption
1482        ]
1483      |6,15:
1484        whd in match (special_function_registers_8052 ???);
1485        whd in match (special_function_registers_8052 ???) in ⊢ (???%);
1486        [1:
1487          >set_arg_8_set_program_counter
1488          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1489          >set_arg_8_set_program_counter
1490          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1491          >special_function_registers_8052_set_program_counter
1492          >special_function_registers_8052_set_program_counter
1493          @special_function_registers_8052_set_arg_8 assumption
1494        |2:
1495          whd in ⊢ (??%%);
1496          >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption
1497        ]
1498        (* XXX: we need special_function_registers_8052_set_arg_8 *)
1499      |7,16:
1500        whd in match (p1_latch ???);
1501        whd in match (p1_latch ???) in ⊢ (???%);
1502        (* XXX: we need p1_latch_8052_set_arg_8 *)
1503      |8,17:
1504        whd in match (p3_latch ???);
1505        whd in match (p3_latch ???) in ⊢ (???%);
1506        (* XXX: we need p3_latch_8052_set_arg_8 *)
1507      |9:
1508        >clock_set_clock
1509        >clock_set_program_counter in ⊢ (???%); >clock_set_clock
1510        >EQticks <instr_refl @eq_f2
1511        [1:
1512          whd in ⊢ (??%%); whd in match (ticks_of0 ??????);
1513        |2:
1514          (* XXX: we need clock_set_arg_8 *)
1515        ]
1516      |18:
1517      ]
1518    ]
1519    (* XXX: switch to the right hand side *)
1520    normalize nodelta >EQs -s >EQticks -ticks
1521    cases (¬ eq_bv ???) normalize nodelta
1522    whd in ⊢ (??%%);
1523    (* XXX: finally, prove the equality using sigma commutation *)
1524    @split_eq_status try %
1525    [1,2,3,19,20,21,28,29,30:
1526      cases daemon (* XXX: axioms as above *)
1527    |4,13,22,31:
1528    |5,14,23,32:
1529    |6,15,24,33:
1530    |7,16,25,34:
1531    |8,17,26,35:
1532      whd in ⊢ (??%%);maps_assm
1533     
1534    |9,18,27,36:
1535      whd in ⊢ (??%%);
1536      whd in match (ticks_of_instruction ?); <instr_refl
1537      cases daemon (* XXX: daemon in ticks_of0 stopping progression *)
1538    ]
1539  |2,4:
1540    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
1541    [2, 4:
1542      cases daemon (* XXX: !!! *)
1543    ]
1544    normalize nodelta >EQppc
1545    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
1546    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
1547    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
1548    #fetch_many_assm whd in fetch_many_assm; %{2}
1549    change with (execute_1 ?? = ?)
1550    @(pose … (execute_1 ? (status_of_pseudo_status …)))
1551    #status_after_1 #EQstatus_after_1
1552    <(?: ? = status_after_1)
1553    [3,6:
1554      >EQstatus_after_1 in ⊢ (???%);
1555      whd in ⊢ (???%);
1556      [1:
1557        <fetch_refl in ⊢ (???%);
1558      |2:
1559        <fetch_refl in ⊢ (???%);
1560      ]
1561      whd in ⊢ (???%);
1562      @(pair_replace ?????????? p)
1563      [1,3:
1564        cases daemon
1565      |2,4:
1566        normalize nodelta
1567        whd in match (addr_of_relative ????);
1568        cases (¬ eq_bv ???) normalize nodelta
1569        >set_clock_mk_Status_commutation
1570        whd in ⊢ (???%);
1571        change with (add ???) in match (\snd (half_add ???));
1572        >set_arg_8_set_program_counter in ⊢ (???%);
1573        [2,4,6,8: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1574        >program_counter_set_program_counter in ⊢ (???%);
1575        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
1576        [2,4,6,8:
1577          >bitvector_of_nat_sign_extension_equivalence
1578          [1,3,5,7:
1579            >EQintermediate_pc' %
1580          |*:
1581            repeat @le_S_S @le_O_n
1582          ]
1583        ]
1584        [1,3: % ]
1585      ]
1586    |1,4:
1587      skip
1588    ]
1589    [3,4:
1590      -status_after_1
1591      @(pose … (execute_1 ? (mk_PreStatus …)))
1592      #status_after_1 #EQstatus_after_1
1593      <(?: ? = status_after_1)
1594      [3,6:
1595        >EQstatus_after_1 in ⊢ (???%);
1596        whd in ⊢ (???%);
1597        (* XXX: matita bug with patterns across multiple goals *)
1598        [1:
1599          <fetch_refl'' in ⊢ (???%);
1600        |2:
1601          <fetch_refl'' in ⊢ (???%);
1602        ]
1603        [2: % |1: whd in ⊢ (???%); % ]
1604      |1,4:
1605        skip
1606      ]
1607      -status_after_1 whd in ⊢ (??%?);
1608      (* XXX: switch to the right hand side *)
1609      normalize nodelta >EQs -s >EQticks -ticks
1610      normalize nodelta whd in ⊢ (??%%);
1611    ]
1612    (* XXX: finally, prove the equality using sigma commutation *)
1613    @split_eq_status try %
1614    whd in ⊢ (??%%);
1615    cases daemon
1616  ]
1617  |30: (* CJNE *)
1618  (* XXX: work on the right hand side *)
1619  cases addr1 -addr1 #addr1 normalize nodelta
1620  cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
1621  (* XXX: switch to the left hand side *)
1622  >EQP -P normalize nodelta
1623  #sigma_increment_commutation #maps_assm #fetch_many_assm
1624
1625  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1626  <EQppc in fetch_many_assm;
1627  whd in match (short_jump_cond ??);
1628  @pair_elim #sj_possible #disp
1629  @pair_elim #result #flags #sub16_refl
1630  @pair_elim #upper #lower #vsplit_refl
1631  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
1632  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
1633  [1,3:
1634    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
1635    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
1636    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
1637    whd in ⊢ (??%?);
1638    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1639    inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
1640    lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
1641    @(if_then_else_replace ???????? eq_bv_refl)
1642    [1,3,5,7:
1643      cases daemon
1644    |2,4,6,8:
1645      (* XXX: switch to the right hand side *)
1646      normalize nodelta >EQs -s >EQticks -ticks
1647      whd in ⊢ (??%%);
1648      (* XXX: finally, prove the equality using sigma commutation *)
1649      @split_eq_status try %
1650      [3,7,11,15:
1651        whd in ⊢ (??%?);
1652        [1,3:
1653          cases daemon
1654        |2,4:
1655          cases daemon
1656        ]
1657      ]
1658      cases daemon (* XXX *)
1659    ]
1660  |2,4:
1661    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
1662    [2, 4:
1663      cases daemon (* XXX: !!! *)
1664    ]
1665    normalize nodelta >EQppc
1666    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
1667    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
1668    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
1669    #fetch_many_assm whd in fetch_many_assm; %{2}
1670    change with (execute_1 ?? = ?)
1671    @(pose … (execute_1 ? (status_of_pseudo_status …)))
1672    #status_after_1 #EQstatus_after_1
1673    <(?: ? = status_after_1)
1674    [2,5:
1675      inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
1676    |3,6:
1677      >EQstatus_after_1 in ⊢ (???%);
1678      whd in ⊢ (???%);
1679      [1: <fetch_refl in ⊢ (???%);
1680      |2: <fetch_refl in ⊢ (???%);
1681      ]
1682      whd in ⊢ (???%);
1683      inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
1684      whd in ⊢ (???%);
1685      whd in match (addr_of_relative ????);
1686      change with (add ???) in match (\snd (half_add ???));
1687      >set_clock_set_program_counter in ⊢ (???%);
1688      >program_counter_set_program_counter in ⊢ (???%);
1689      >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
1690      [2,4,6,8:
1691        >bitvector_of_nat_sign_extension_equivalence
1692        [1,3,5,7:
1693          >EQintermediate_pc' %
1694        |*:
1695          repeat @le_S_S @le_O_n
1696        ]
1697      |1,5:
1698        %
1699      ]
1700    |1,4: skip
1701    ]
1702    [1,2,3,4:
1703      -status_after_1
1704      @(pose … (execute_1 ? (mk_PreStatus …)))
1705      #status_after_1 #EQstatus_after_1
1706      <(?: ? = status_after_1)
1707      [3,6,9,12:
1708        >EQstatus_after_1 in ⊢ (???%);
1709        whd in ⊢ (???%);
1710        (* XXX: matita bug with patterns across multiple goals *)
1711        [1: <fetch_refl'' in ⊢ (???%);
1712        |2: <fetch_refl'' in ⊢ (???%);
1713        |3: <fetch_refl'' in ⊢ (???%);
1714        |4: <fetch_refl'' in ⊢ (???%);
1715        ] %
1716      |1,4,7,10:
1717        skip
1718      ]
1719      -status_after_1 whd in ⊢ (??%?);
1720      (* XXX: switch to the right hand side *)
1721      normalize nodelta >EQs -s >EQticks -ticks
1722      whd in ⊢ (??%%);
1723    ]
1724    (* XXX: finally, prove the equality using sigma commutation *)
1725    @split_eq_status try %
1726    cases daemon
1727  ]
1728  |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
1729  (* XXX: work on the right hand side *)
1730  >p normalize nodelta
1731  (* XXX: switch to the left hand side *)
1732  >EQP -P normalize nodelta
1733  #sigma_increment_commutation #maps_assm #fetch_many_assm
1734 
1735  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1736  <EQppc in fetch_many_assm;
1737  whd in match (short_jump_cond ??);
1738  @pair_elim #sj_possible #disp
1739  @pair_elim #result #flags #sub16_refl
1740  @pair_elim #upper #lower #vsplit_refl
1741  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
1742  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
1743  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1744    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
1745    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
1746    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
1747    whd in ⊢ (??%?);
1748    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1749    (* XXX: work on the left hand side *)
1750    @(if_then_else_replace ???????? p) normalize nodelta
1751    [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1752      cases daemon
1753    ]
1754    (* XXX: switch to the right hand side *)
1755    normalize nodelta >EQs -s >EQticks -ticks
1756    whd in ⊢ (??%%);
1757    (* XXX: finally, prove the equality using sigma commutation *)
1758    @split_eq_status try %
1759    cases daemon
1760  |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1761    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
1762    [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1763      cases daemon (* XXX: !!! *)
1764    ]
1765    normalize nodelta >EQppc
1766    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
1767    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
1768    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
1769    #fetch_many_assm whd in fetch_many_assm; %{2}
1770    change with (execute_1 ?? = ?)
1771    @(pose … (execute_1 ? (status_of_pseudo_status …)))
1772    #status_after_1 #EQstatus_after_1
1773    <(?: ? = status_after_1)
1774    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
1775      >EQstatus_after_1 in ⊢ (???%);
1776      whd in ⊢ (???%);
1777      [1: <fetch_refl in ⊢ (???%);
1778      |2: <fetch_refl in ⊢ (???%);
1779      |3: <fetch_refl in ⊢ (???%);
1780      |4: <fetch_refl in ⊢ (???%);
1781      |5: <fetch_refl in ⊢ (???%);
1782      |6: <fetch_refl in ⊢ (???%);
1783      |7: <fetch_refl in ⊢ (???%);
1784      |8: <fetch_refl in ⊢ (???%);
1785      |9: <fetch_refl in ⊢ (???%);
1786      |10: <fetch_refl in ⊢ (???%);
1787      |11: <fetch_refl in ⊢ (???%);
1788      |12: <fetch_refl in ⊢ (???%);
1789      |13: <fetch_refl in ⊢ (???%);
1790      |14: <fetch_refl in ⊢ (???%);
1791      ]
1792      whd in ⊢ (???%);
1793      @(if_then_else_replace ???????? p)
1794      [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1795        cases daemon
1796      |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1797        normalize nodelta
1798        whd in match (addr_of_relative ????);
1799        >set_clock_mk_Status_commutation
1800        [9,10:
1801          (* XXX: demodulation not working in this case *)
1802          >program_counter_set_arg_1 in ⊢ (???%);
1803          >program_counter_set_program_counter in ⊢ (???%);
1804        |*:
1805          /demod/
1806        ]
1807        whd in ⊢ (???%);
1808        change with (add ???) in match (\snd (half_add ???));
1809        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
1810        [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1811          >bitvector_of_nat_sign_extension_equivalence
1812          [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1813            >EQintermediate_pc' %
1814          |*:
1815            repeat @le_S_S @le_O_n
1816          ]
1817        ]
1818        %
1819      ]
1820    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
1821      skip
1822    ]
1823    -status_after_1
1824    @(pose … (execute_1 ? (mk_PreStatus …)))
1825    #status_after_1 #EQstatus_after_1
1826    <(?: ? = status_after_1)
1827    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
1828      >EQstatus_after_1 in ⊢ (???%);
1829      whd in ⊢ (???%);
1830      (* XXX: matita bug with patterns across multiple goals *)
1831      [1: <fetch_refl'' in ⊢ (???%);
1832      |2: <fetch_refl' in ⊢ (???%);
1833      |3: <fetch_refl'' in ⊢ (???%);
1834      |4: <fetch_refl' in ⊢ (???%);
1835      |5: <fetch_refl'' in ⊢ (???%);
1836      |6: <fetch_refl' in ⊢ (???%);
1837      |7: <fetch_refl'' in ⊢ (???%);
1838      |8: <fetch_refl' in ⊢ (???%);
1839      |9: <fetch_refl'' in ⊢ (???%);
1840      |10: <fetch_refl' in ⊢ (???%);
1841      |11: <fetch_refl'' in ⊢ (???%);
1842      |12: <fetch_refl' in ⊢ (???%);
1843      |13: <fetch_refl'' in ⊢ (???%);
1844      |14: <fetch_refl' in ⊢ (???%);
1845      ]
1846      whd in ⊢ (???%);
1847      [9,10:
1848      |*:
1849        /demod/
1850      ] %
1851    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
1852      skip
1853    ]
1854    -status_after_1 whd in ⊢ (??%?);
1855    (* XXX: switch to the right hand side *)
1856    normalize nodelta >EQs -s >EQticks -ticks
1857    whd in ⊢ (??%%);
1858    (* XXX: finally, prove the equality using sigma commutation *)
1859    @split_eq_status try %
1860    [3,11,19,27,36,53,61:
1861      >program_counter_set_program_counter >set_clock_mk_Status_commutation
1862      [5: >program_counter_set_program_counter ]
1863      >EQaddr_of normalize nodelta
1864      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
1865      >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
1866      @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉)
1867      >create_label_cost_refl normalize nodelta #relevant @relevant
1868      whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr))
1869      try assumption whd in match instruction_has_label; normalize nodelta
1870      <instr_refl normalize nodelta %
1871    |7,15,23,31,45,57,65:
1872      >set_clock_mk_Status_commutation >program_counter_set_program_counter
1873      whd in ⊢ (??%?); normalize nodelta
1874      >EQppc in fetch_many_assm; #fetch_many_assm
1875      [5:
1876        >program_counter_set_arg_1 >program_counter_set_program_counter
1877      ]
1878      <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
1879      <bitvector_of_nat_sign_extension_equivalence
1880      [1,3,5,7,9,11,13:
1881        whd in ⊢ (???%); cases (half_add ???) normalize //
1882      |2,4,6,8,10,12,14:
1883        @assembly1_lt_128
1884        @le_S_S @le_O_n
1885      ]
1886    |*:
1887      cases daemon
1888    ]
1889  ]
1890  |4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
1891  (* XXX: work on the right hand side *)
1892  lapply (subaddressing_modein ???)
1893  <EQaddr normalize nodelta #irrelevant
1894  try (>p normalize nodelta)
1895  try (>p1 normalize nodelta)
1896  (* XXX: switch to the left hand side *)
1897  >EQP -P normalize nodelta
1898  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1899  whd in ⊢ (??%?);
1900  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1901  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1902  (* XXX: work on the left hand side *)
1903  [1,2,3,4,5:
1904    generalize in ⊢ (??(???(?%))?);
1905  |6,7,8,9,10,11:
1906    generalize in ⊢ (??(???(?%))?);
1907  |12:
1908    generalize in ⊢ (??(???(?%))?);
1909  ]
1910  <EQaddr normalize nodelta #irrelevant
1911  try @(jmpair_as_replace ?????????? p)
1912  [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
1913  (* XXX: switch to the right hand side *)
1914  normalize nodelta >EQs -s >EQticks -ticks
1915  whd in ⊢ (??%%);
1916  (* XXX: finally, prove the equality using sigma commutation *)
1917  try @split_eq_status try % whd in ⊢ (??%%);
1918  cases daemon
1919  |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
1920  (* XXX: work on the right hand side *)
1921  >p normalize nodelta
1922  try (>p1 normalize nodelta)
1923  (* XXX: switch to the left hand side *)
1924  -instr_refl >EQP -P normalize nodelta
1925  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1926  whd in ⊢ (??%?);
1927  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1928  (* XXX: work on the left hand side *)
1929  @(pair_replace ?????????? p)
1930  [1,3,5,7,9,11,13,15,17:
1931    >set_clock_set_program_counter >set_clock_mk_Status_commutation
1932    >set_program_counter_mk_Status_commutation >clock_set_program_counter
1933    cases daemon
1934  |14,16,18:
1935    normalize nodelta
1936    @(pair_replace ?????????? p1)
1937    [1,3,5:
1938      >set_clock_mk_Status_commutation
1939      cases daemon
1940    ]
1941  ]
1942  (* XXX: switch to the right hand side *)
1943  normalize nodelta >EQs -s >EQticks -ticks
1944  whd in ⊢ (??%%);
1945  (* XXX: finally, prove the equality using sigma commutation *)
1946  try @split_eq_status try %
1947  cases daemon
1948  |10,42,43,44,45,49,52,56: (* MUL *)
1949  (* XXX: work on the right hand side *)
1950  (* XXX: switch to the left hand side *)
1951  -instr_refl >EQP -P normalize nodelta
1952  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1953  whd in ⊢ (??%?);
1954  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1955  (* XXX: work on the left hand side *)
1956  (* XXX: switch to the right hand side *)
1957  normalize nodelta >EQs -s >EQticks -ticks
1958  whd in ⊢ (??%%);
1959  (* XXX: finally, prove the equality using sigma commutation *)
1960  cases daemon
1961  |11,12: (* DIV *)
1962  (* XXX: work on the right hand side *)
1963  normalize nodelta in p;
1964  >p normalize nodelta
1965  (* XXX: switch to the left hand side *)
1966  -instr_refl >EQP -P normalize nodelta
1967  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1968  whd in ⊢ (??%?);
1969  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1970  @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
1971  >(?: pose_assm = 0) normalize nodelta
1972  [2,4:
1973    <p >pose_refl
1974    cases daemon
1975  |1,3:
1976    (* XXX: switch to the right hand side *)
1977    >EQs -s >EQticks -ticks
1978    whd in ⊢ (??%%);
1979    (* XXX: finally, prove the equality using sigma commutation *)
1980    @split_eq_status try %
1981    cases daemon
1982  ]
1983  |13,14,15: (* DA *)
1984  (* XXX: work on the right hand side *)
1985  >p normalize nodelta
1986  >p1 normalize nodelta
1987  try (>p2 normalize nodelta
1988  try (>p3 normalize nodelta
1989  try (>p4 normalize nodelta
1990  try (>p5 normalize nodelta))))
1991  (* XXX: switch to the left hand side *)
1992  -instr_refl >EQP -P normalize nodelta
1993  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1994  whd in ⊢ (??%?);
1995  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1996  (* XXX: work on the left hand side *)
1997  @(pair_replace ?????????? p)
1998  [1,3,5:
1999    /demod/
2000    cases daemon
2001  |2,4,6:
2002    @(if_then_else_replace ???????? p1)
2003    [1,3,5:
2004      cases daemon
2005    |2,4:
2006      normalize nodelta
2007      @(pair_replace ?????????? p2)
2008      [1,3:
2009        cases daemon
2010      |2,4:
2011        normalize nodelta >p3 normalize nodelta
2012        >p4 normalize nodelta try >p5
2013      ]
2014    ]
2015  (* XXX: switch to the right hand side *)
2016  normalize nodelta >EQs -s >EQticks -ticks
2017  whd in ⊢ (??%%);
2018  (* XXX: finally, prove the equality using sigma commutation *)
2019  @split_eq_status try %
2020  cases daemon
2021  ]
2022  |33,34,35,48: (* ANL, ORL, XRL, MOVX *)
2023  (* XXX: work on the right hand side *)
2024  cases addr #addr' normalize nodelta
2025  [1,3:
2026    cases addr' #addr'' normalize nodelta
2027  ]
2028  @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta
2029  (* XXX: switch to the left hand side *)
2030  -instr_refl >EQP -P normalize nodelta
2031  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2032  whd in ⊢ (??%?);
2033  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2034  (* XXX: work on the left hand side *)
2035  (* XXX: switch to the right hand side *)
2036  normalize nodelta >EQs -s >EQticks -ticks
2037  whd in ⊢ (??%%);
2038  (* XXX: finally, prove the equality using sigma commutation *)
2039  cases daemon
2040  |47: (* MOV *)
2041  (* XXX: work on the right hand side *)
2042  cases addr -addr #addr normalize nodelta
2043  [1:
2044    cases addr #addr normalize nodelta
2045    [1:
2046      cases addr #addr normalize nodelta
2047      [1:
2048        cases addr #addr normalize nodelta
2049        [1:
2050          cases addr #addr normalize nodelta
2051        ]
2052      ]
2053    ]
2054  ]
2055  cases addr #lft #rgt normalize nodelta
2056  (* XXX: switch to the left hand side *)
2057  >EQP -P normalize nodelta
2058  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2059  whd in ⊢ (??%?);
2060  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2061  (* XXX: work on the left hand side *)
2062  (* XXX: switch to the right hand side *)
2063  normalize nodelta >EQs -s >EQticks -ticks
2064  whd in ⊢ (??%%);
2065  (* XXX: finally, prove the equality using sigma commutation *)
2066  cases daemon
2067  ]
2068qed.
Note: See TracBrowser for help on using the repository browser.