source: src/ASM/StatusProofsSplit.ma @ 2407

Last change on this file since 2407 was 2285, checked in by sacerdot, 8 years ago
  1. duplicated code erased
  2. POP case finished up to lemmas on read_at_stack_pointer
File size: 20.3 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 special_function_registers_8051_set_arg_16:
69  ∀M, M': Type[0].
70  ∀cm: M.
71  ∀cm': M'.
72  ∀s: PreStatus M cm.
73  ∀s': PreStatus M' cm'.
74  ∀w, w': Word.
75  ∀d, d': [[dptr]].
76   special_function_registers_8051 ?? s = special_function_registers_8051 … s' →
77    w = w' →
78      special_function_registers_8051 ?? (set_arg_16 … s w d) =
79        special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d').
80  #M #M' #cm #cm' #s #s' #w #w'
81  #d @(subaddressing_mode_elim … d)
82  #d' @(subaddressing_mode_elim … d')
83  #EQ1 #EQ2 <EQ2 normalize cases (vsplit bool 8 8 w) #b1 #b2 normalize <EQ1 %
84qed.
85
86lemma program_counter_set_arg_1:
87  ∀M: Type[0].
88  ∀cm: M.
89  ∀s: PreStatus M cm.
90  ∀addr: [[bit_addr; carry]].
91  ∀b: Bit.
92    program_counter M cm (set_arg_1 M cm s addr b) = program_counter M cm s.
93  #M #cm #s whd in match set_arg_1; cases daemon (* whd in match set_arg_1'; normalize nodelta
94  #addr #b
95  @(subaddressing_mode_elim … addr)
96  [1:
97    #byte cases (vsplit ????) #nu #nl normalize nodelta
98    cases (vsplit ????) #ignore #three_bits normalize nodelta
99    cases (get_index_v bool ????) normalize nodelta
100    [1:
101      @program_counter_set_bit_addressable_sfr
102    |2:
103      @program_counter_set_low_internal_ram
104    ]
105  |2:
106    cases (vsplit ????) //
107  ] *)
108qed.
109
110lemma get_ov_flag_set_program_counter:
111  ∀M: Type[0].
112  ∀cm: M.
113  ∀s: PreStatus M cm.
114  ∀pc: Word.
115    get_ov_flag M cm (set_program_counter M cm s pc) =
116      get_ov_flag M cm s.
117  #M #cm #s #pc %
118qed.
119
120lemma external_ram_set_program_counter:
121  ∀M: Type[0].
122  ∀cm: M.
123  ∀s: PreStatus M cm.
124  ∀pc: Word.
125    external_ram M cm (set_program_counter M cm s pc) =
126      external_ram M cm s.
127  #M #cm #s #pc %
128qed.
129
130lemma low_internal_ram_set_program_counter:
131  ∀M: Type[0].
132  ∀cm: M.
133  ∀s: PreStatus M cm.
134  ∀pc: Word.
135    low_internal_ram M cm (set_program_counter M cm s pc) =
136      low_internal_ram M cm s.
137  #M #cm #s #pc %
138qed.
139
140lemma high_internal_ram_set_program_counter:
141  ∀M: Type[0].
142  ∀cm: M.
143  ∀s: PreStatus M cm.
144  ∀pc: Word.
145    high_internal_ram M cm (set_program_counter M cm s pc) =
146      high_internal_ram M cm s.
147  #M #cm #s #pc %
148qed.
149
150lemma get_arg_8_set_program_counter:
151  ∀M: Type[0].
152  ∀cm: M.
153  ∀s: PreStatus M cm.
154  ∀flag: bool.
155  ∀addr: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; ext_indirect; ext_indirect_dptr]].
156  ∀pc: Word.
157    get_arg_8 M cm (set_program_counter M cm s pc) flag addr =
158      get_arg_8 M cm s flag addr.
159  [2,3:
160    cases addr #subaddressing_mode
161    cases subaddressing_mode
162    try (#addr1 whd in ⊢ (% → %);)
163    whd in ⊢ (% → %); //
164  ]
165  #M #cm #s #flag #addr #pc
166  whd in match get_arg_8; normalize nodelta
167  cases addr *
168  try (#addr1 #absurd normalize in absurd; cases absurd @I)
169  try (#absurd normalize in absurd; cases absurd @I)
170  try (#addr1 #addr2) try #addr1
171  normalize nodelta %
172qed.
173
174lemma external_ram_set_flags:
175  ∀M: Type[0].
176  ∀cm: M.
177  ∀s: PreStatus M cm.
178  ∀opt: option Bit.
179  ∀bit1, bit2: Bit.
180    external_ram M cm (set_flags M cm s bit1 opt bit2) =
181      external_ram M cm s.
182  #M #cm #s #opt #bit1 #bit2 %
183qed.
184
185lemma low_internal_ram_set_flags:
186  ∀M: Type[0].
187  ∀cm: M.
188  ∀s: PreStatus M cm.
189  ∀opt: option Bit.
190  ∀bit1, bit2: Bit.
191    low_internal_ram M cm (set_flags M cm s bit1 opt bit2) =
192      low_internal_ram M cm s.
193  #M #cm #s #opt #bit1 #bit2 %
194qed.
195
196lemma high_internal_ram_set_flags:
197  ∀M: Type[0].
198  ∀cm: M.
199  ∀s: PreStatus M cm.
200  ∀opt: option Bit.
201  ∀bit1, bit2: Bit.
202    high_internal_ram M cm (set_flags M cm s bit1 opt bit2) =
203      high_internal_ram M cm s.
204  #M #cm #s #opt #bit1 #bit2 %
205qed.
206
207lemma low_internal_ram_set_clock:
208  ∀M: Type[0].
209  ∀cm: M.
210  ∀s: PreStatus M cm.
211  ∀t: Time.
212    low_internal_ram M cm (set_clock M cm s t) =
213      low_internal_ram M cm s.
214  #M #cm #s #t %
215qed.
216
217lemma high_internal_ram_set_clock:
218  ∀M: Type[0].
219  ∀cm: M.
220  ∀s: PreStatus M cm.
221  ∀t: Time.
222    high_internal_ram M cm (set_clock M cm s t) =
223      high_internal_ram M cm s.
224  #M #cm #s #t %
225qed.
226
227lemma external_ram_set_clock:
228  ∀M: Type[0].
229  ∀cm: M.
230  ∀s: PreStatus M cm.
231  ∀t: Time.
232    external_ram M cm (set_clock M cm s t) =
233      external_ram M cm s.
234  #M #cm #s #t %
235qed.
236
237lemma set_8051_sfr_set_program_counter:
238  ∀M: Type[0].
239  ∀cm: M.
240  ∀s: PreStatus M cm.
241  ∀pc: Word.
242  ∀sfr: SFR8051.
243  ∀v: Byte.
244    set_8051_sfr M cm (set_program_counter M cm s pc) sfr v =
245      set_program_counter M cm (set_8051_sfr M cm s sfr v) pc.
246  #M #cm #s #pc #sfr #v %
247qed.
248
249lemma low_internal_ram_set_8051_sfr:
250  ∀M: Type[0].
251  ∀cm: M.
252  ∀s: PreStatus M cm.
253  ∀sfr: SFR8051.
254  ∀v: Byte.
255    low_internal_ram M cm (set_8051_sfr M cm s sfr v) =
256      low_internal_ram M cm s.
257  #M #cm #s #sfr #v %
258qed.
259
260lemma high_internal_ram_set_8051_sfr:
261  ∀M: Type[0].
262  ∀cm: M.
263  ∀s: PreStatus M cm.
264  ∀sfr: SFR8051.
265  ∀v: Byte.
266    high_internal_ram M cm (set_8051_sfr M cm s sfr v) =
267      high_internal_ram M cm s.
268  #M #cm #s #sfr #v %
269qed.
270
271lemma external_ram_set_8051_sfr:
272  ∀M: Type[0].
273  ∀cm: M.
274  ∀s: PreStatus M cm.
275  ∀sfr: SFR8051.
276  ∀v: Byte.
277    external_ram M cm (set_8051_sfr M cm s sfr v) =
278      external_ram M cm s.
279  #M #cm #s #sfr #v %
280qed.
281
282lemma get_arg_8_set_clock:
283  ∀M: Type[0].
284  ∀cm: M.
285  ∀s: PreStatus M cm.
286  ∀addr.
287  ∀t: Time.
288    get_arg_8 M cm (set_clock M cm s t) addr =
289      get_arg_8 M cm s addr.
290  #M #cm #s #addr #t %
291qed.
292
293lemma set_program_counter_set_program_counter:
294  ∀M: Type[0].
295  ∀cm: M.
296  ∀s: PreStatus M cm.
297  ∀pc: Word.
298  ∀pc': Word.
299    set_program_counter M cm (set_program_counter M cm s pc) pc' =
300      set_program_counter M cm s pc'.
301  #M #cm #s #pc #pc' %
302qed.
303
304(* XXX: move elsewhere *)
305lemma bitvector_8_cases:
306  ∀w: BitVector 8.
307    ∃b0,b1,b2,b3,b4,b5,b6,b7: bool.
308      w ≃ [[b0;b1;b2;b3;b4;b5;b6;b7]].
309 #w repeat (cases (BitVector_Sn … w)  #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w)
310 >(BitVector_O … w) %
311qed.
312
313(* XXX: not true
314lemma p3_latch_set_arg_8:
315  ∀M: Type[0].
316  ∀cm: M.
317  ∀s: PreStatus M cm.
318  ∀args.
319  ∀v: Byte.
320    p3_latch M cm (set_arg_8 M cm s args v) =
321      p3_latch M cm s.
322  #M #cm #s #args #v
323  @(subaddressing_mode_elim … args)
324  try #w try %
325  whd in match set_arg_8; normalize nodelta
326  whd in match set_arg_8'; normalize nodelta
327  inversion (vsplit bool ???) #nu #nl #nu_nl_refl normalize nodelta
328  inversion (vsplit bool ???) #ignore #three_bits #ignore_three_bits_refl normalize nodelta
329  inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta try %
330  whd in match set_bit_addressable_sfr; normalize nodelta
331  @(bitvector_8_elim_prop … w)
332*)
333
334lemma status_of_pseudo_status_does_not_change_8051_sfrs:
335  ∀M: internal_pseudo_address_map.
336  ∀cm: pseudo_assembly_program.
337  ∀s: PreStatus pseudo_assembly_program cm.
338  ∀sigma: Word → Word.
339  ∀policy: Word → bool.
340    \snd M = None … →
341      special_function_registers_8051 pseudo_assembly_program cm s =
342        special_function_registers_8051 (BitVectorTrie Byte 16)
343          (code_memory_of_pseudo_assembly_program cm sigma policy)
344          (status_of_pseudo_status M cm s sigma policy).
345  #M #cm #s #sigma #policy #None_proof cases s
346  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
347  whd in match status_of_pseudo_status; normalize nodelta
348  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
349  >None_proof %
350qed.
351
352lemma n_lt_19_elim_prop:
353  ∀P: nat → Prop.
354    P 0 → P 1 → P 2 → P 3 → P 4 → P 5 → P 6 → P 7 → P 8 → P 9 →
355    P 10 → P 11 → P 12 → P 13 → P 14 → P 15 → P 16 → P 17 → P 18 →
356      (∀n. n < 19 → P n).
357  #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14
358  #H15 #H16 #H17 #H18 #H19 #n
359  cases n [1: // ]
360  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
361  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
362  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
363  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
364  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
365  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
366  #n' normalize in ⊢ (% → ?);
367  #absurd repeat (lapply (le_S_S_to_le … absurd) #absurd)
368  cases (lt_to_not_zero … absurd)
369qed.
370
371lemma get_index_v_set_index_miss:
372  ∀T: Type[0].
373  ∀n, i, j: nat.
374  ∀v: Vector T n.
375  ∀b: T.
376  ∀i_proof: i < n.
377  ∀j_proof: j < n.
378  i ≠ j →
379    get_index_v T n (set_index T n v i b i_proof) j j_proof =
380      get_index_v T n v j j_proof.
381  #T #n #i #j #v lapply i lapply j elim v #i #j
382  [1:
383    #b #i_proof
384    cases (lt_to_not_zero … i_proof)
385  |2:
386    #tl #inductive_hypothesis #j' #i' #b #i_proof #j_proof #i_neq_j
387    lapply i_proof lapply i_neq_j cases i'
388    [1:
389      -i_neq_j #i_neq_j -i_proof #i_proof
390      whd in match (set_index ??????);
391      lapply j_proof lapply i_neq_j cases j'
392      [1:
393        #relevant @⊥ cases relevant -relevant #absurd @absurd %
394      |2:
395        #j' #_ -j_proof #j_proof %
396      ]
397    |2:
398      #i' -i_neq_j #i_neq_j -i_proof #i_proof
399      lapply j_proof lapply i_neq_j cases j'
400      [1:
401        #_ #j_proof %
402      |2:
403        #j' #i_neq_j #j_proof
404        @inductive_hypothesis @nmk #relevant
405        cases i_neq_j #absurd @absurd >relevant %
406      ]
407    ]
408  ]
409qed.
410
411lemma get_index_v_special_function_registers_8051_not_acc_a:
412  ∀M: internal_pseudo_address_map.
413  ∀cm: pseudo_assembly_program.
414  ∀s: PreStatus pseudo_assembly_program cm.
415  ∀sigma: Word → Word.
416  ∀policy: Word → bool.
417  ∀n: nat.
418  ∀proof: n < 19.
419    n ≠ 17 →
420   (get_index_v Byte 19
421    (special_function_registers_8051 pseudo_assembly_program cm s) n
422    proof =
423   get_index_v Byte 19
424     (special_function_registers_8051 (BitVectorTrie Byte 16)
425       (code_memory_of_pseudo_assembly_program cm sigma policy)
426       (status_of_pseudo_status M cm s sigma policy)) n
427       proof).
428  #M #cm #s #sigma #policy #n #proof lapply proof
429  @(n_lt_19_elim_prop … proof) -proof #proof
430  [18:
431    #absurd @⊥ cases absurd -absurd #absurd @absurd %
432  ]
433  #_ cases s #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
434  whd in match status_of_pseudo_status; normalize nodelta
435  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
436  cases M #left #right cases right normalize nodelta try %
437  -right * * #address normalize nodelta
438  @pair_elim #high #low #high_low_refl normalize nodelta
439  whd in match sfr_8051_index; normalize nodelta
440  >get_index_v_set_index_miss try %
441  #absurd destruct(absurd)
442qed.
443
444(*
445include alias "arithmetics/nat.ma".
446include alias "basics/logic.ma".
447include alias "ASM/BitVectorTrie.ma".
448*)
449
450lemma bitvector_cases_hd_tl:
451  ∀n: nat.
452  ∀w: BitVector (S n).
453   ∃hd: bool. ∃tl: BitVector n.
454    w ≃ hd:::tl.
455  #n #w cases (BitVector_Sn … w) #hd #relevant %{hd} @relevant
456qed.
457
458lemma external_ram_set_bit_addressable_sfr:
459  ∀M: Type[0].
460  ∀cm: M.
461  ∀ps.
462  ∀w.
463  ∀result: Byte.
464    external_ram M cm
465      (set_bit_addressable_sfr M cm ps w result) =
466    external_ram M cm ps.
467  #M #cm #ps #w #result cases daemon (* XXX: prove this with Russell in Status.ma!
468  whd in match set_bit_addressable_sfr; normalize nodelta
469  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
470  cases (eqb ??) normalize nodelta [1: % ]
471  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
472  cases (eqb ??) normalize nodelta [1: % ]
473  cases (eqb ??) normalize nodelta [1: % ]
474  cases (eqb ??) normalize nodelta [1: % ]
475  cases (eqb ??) normalize nodelta [1: % ]
476  cases (eqb ??) normalize nodelta [1: % ]
477  cases (eqb ??) normalize nodelta [1: % ]
478  cases (eqb ??) normalize nodelta [1: % ]
479  cases (eqb ??) normalize nodelta [1: % ]
480  cases (eqb ??) normalize nodelta [1: % ]
481  cases (eqb ??) normalize nodelta [1: % ]
482  cases (eqb ??) normalize nodelta [1: % ]
483  cases (eqb ??) normalize nodelta [1: % ]
484  cases (eqb ??) normalize nodelta [1: % ]
485  cases (eqb ??) normalize nodelta [1: % ]
486  cases (eqb ??) normalize nodelta [1: % ]
487  cases (eqb ??) normalize nodelta [1: % ]
488  cases (eqb ??) normalize nodelta [1: % ]
489  cases (eqb ??) normalize nodelta [1: % ]
490  cases (eqb ??) normalize nodelta [1: % ]
491  cases (eqb ??) normalize nodelta [1: % ]
492  cases (eqb ??) normalize nodelta [1: % ]
493  cases (eqb ??) normalize nodelta [1: % ]
494  cases (eqb ??) normalize nodelta [1: % ]
495  cases not_implemented *)
496qed.
497
498lemma external_ram_set_arg_8:
499  ∀M: Type[0].
500  ∀cm: M.
501  ∀ps.
502  ∀addr1: [[direct; indirect; registr; acc_a; acc_b ]].
503  ∀result.
504    external_ram M cm (set_arg_8 M cm ps addr1 result) =
505      external_ram M cm ps.
506  [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
507  #M #cm #ps #addr1 #result
508  @(subaddressing_mode_elim … addr1) try #w try %
509  whd in ⊢ (??(???%)?); cases daemon (*whd in ⊢ (??(???(???%))?); (* XXX: to be understood, slow match *)
510  [1:
511    cases (vsplit bool ???) #nu #nl normalize nodelta
512    cases (vsplit bool ???) #ignore #three_bits normalize nodelta
513    cases (get_index_v bool ????) normalize nodelta try %
514    @external_ram_set_bit_addressable_sfr
515  |2:
516    cases (vsplit bool ???) #nu #nl normalize nodelta
517    cases (vsplit bool ???) #ignore #three_bits normalize nodelta
518    cases (get_index_v bool ????) normalize nodelta %
519  ] *)
520qed.
521
522lemma special_function_registers_8051_set_clock:
523  ∀M: Type[0].
524  ∀cm: M.
525  ∀ps.
526  ∀t.
527    special_function_registers_8051 M cm (set_clock M cm ps t) =
528      special_function_registers_8051 M cm ps.
529  //
530qed.
531
532lemma special_function_registers_8051_set_program_counter:
533  ∀M: Type[0].
534  ∀cm: M.
535  ∀ps.
536  ∀pc: Word.
537    special_function_registers_8051 M cm (set_program_counter M cm ps pc) =
538      special_function_registers_8051 M cm ps.
539  //
540qed.
541
542lemma special_function_registers_8052_set_program_counter:
543  ∀M: Type[0].
544  ∀cm: M.
545  ∀ps.
546  ∀pc: Word.
547    special_function_registers_8052 M cm (set_program_counter M cm ps pc) =
548      special_function_registers_8052 M cm ps.
549  //
550qed.
551
552lemma set_index_set_index_commutation:
553  ∀A: Type[0].
554  ∀n: nat.
555  ∀v: Vector A n.
556  ∀m, o: nat.
557  ∀m_lt_proof: m < n.
558  ∀o_lt_proof: o < n.
559  ∀e, f: A.
560    m ≠ o →
561      set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof =
562        set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof.
563  #A #n #v elim v
564  [1:
565    #m #o #m_lt_proof
566    normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof)
567  |2:
568    #n' #hd #tl #inductive_hypothesis
569    #m #o
570    cases m cases o
571    [1:
572      #m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant
573      @relevant %
574    |2,3:
575      #o' normalize //
576    |4:
577      #m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm
578      normalize @eq_f @inductive_hypothesis @nmk #relevant
579      >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) %
580    ]
581  ]
582qed.
583
584(*CSC: dead and unfinished code
585lemma special_function_registers_8051_set_arg_8:
586  ∀M: internal_pseudo_address_map.
587  ∀cm: pseudo_assembly_program.
588  ∀ps.
589  ∀sigma: Word → Word.
590  ∀policy: Word → bool.
591  ∀addr1: [[ registr; direct ]].
592  ∀result.
593    addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →
594    special_function_registers_8051 (BitVectorTrie Byte 16)
595      (code_memory_of_pseudo_assembly_program cm sigma policy)
596      (set_arg_8 (BitVectorTrie Byte 16)
597        (code_memory_of_pseudo_assembly_program cm sigma policy)
598        (status_of_pseudo_status M cm ps sigma policy) addr1 result) =
599   sfr_8051_of_pseudo_sfr_8051 M
600     (special_function_registers_8051 pseudo_assembly_program cm
601     (set_arg_8 pseudo_assembly_program cm ps addr1 result)) sigma.
602  cases daemon
603(*
604  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
605  #M #cm #ps #sigma #policy #addr1 #result
606  @(subaddressing_mode_elim … addr1) #w #addressing_mode_ok_refl try %
607  whd in match (set_arg_8 ?????); whd in ⊢ (??(???(???%))?);
608  whd in match (set_arg_8 ?????) in ⊢ (???%); whd in ⊢ (???(??(???(???%))?));
609  cases (vsplit bool ???) #nu #nl normalize nodelta
610  cases (vsplit bool ???) #ignore #three_bits normalize nodelta
611  cases (get_index_v bool ????) normalize nodelta try %
612  whd in match (set_bit_addressable_sfr ?????); whd in match (set_bit_addressable_sfr ?????) in ⊢ (???%);
613  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
614  cases (eqb ??) normalize nodelta [1: % ]
615  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
616  cases (eqb ??) normalize nodelta [1: % ]
617  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
618  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
619  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
620  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
621  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
622  cases (eqb ??) normalize nodelta [1: % ]
623  cases (eqb ??) normalize nodelta [1: % ]
624  cases (eqb ??) normalize nodelta [1: % ]
625  cases (eqb ??) normalize nodelta [1: % ]
626  cases (eqb ??) normalize nodelta [1: % ]
627  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
628  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
629  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
630  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
631  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
632  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
633  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
634  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
635  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
636  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
637  inversion (eqb ??) #eqb_refl normalize nodelta [1:
638    whd in addressing_mode_ok_refl:(??%?); <(eqb_true_to_eq … eqb_refl) in addressing_mode_ok_refl;
639    >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
640    #relevant cases (conjunction_true … relevant) #_ #eq_acc_assm
641    whd in match (status_of_pseudo_status ?????);
642    whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
643    >(eq_accumulator_address_map_entry_true_to_eq … eq_acc_assm) normalize nodelta %
644  ]
645  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
646  cases not_implemented *)
647qed.
648*)
Note: See TracBrowser for help on using the repository browser.