source: src/ASM/StatusProofsSplit.ma @ 2272

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

Changed proof strategy for main lemma after noticed that the current approach would not work with POP, RET, etc. Ported throughout the assembly proof and all the way up to Test.ma.

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