source: src/ASM/AssemblyProofSplit.ma @ 2047

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

Big bugs in policy calculations found. Waiting for Jaap's commit.

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