source: src/ASM/StatusProofsSplit.ma @ 2244

Last change on this file since 2244 was 2172, checked in by mulligan, 9 years ago

Moved new versions of get_ / set_arg_* into Status.ma. Commented out proofs that are no longer working.
File size: 28.6 KB
Line 
1include "ASM/AssemblyProof.ma".
2include alias "arithmetics/nat.ma".
3include alias "basics/logic.ma".
4
5lemma set_arg_16_mk_Status_commutation:
6  ∀M: Type[0].
7  ∀cm: M.
8  ∀s: PreStatus M cm.
9  ∀w: Word.
10  ∀d: [[dptr]].
11    set_arg_16 M cm s w d =
12      mk_PreStatus M cm
13        (low_internal_ram … s)
14        (high_internal_ram … s)
15        (external_ram … s)
16        (program_counter … s)
17        (special_function_registers_8051 … (set_arg_16 M cm s w d))
18        (special_function_registers_8052 … s)
19        (p1_latch … s)
20        (p3_latch … s)
21        (clock … s).
22  #M #cm #s #w #d
23  whd in match set_arg_16; normalize nodelta
24  whd in match set_arg_16'; normalize nodelta
25  @(subaddressing_mode_elim … d)
26  cases (vsplit bool 8 8 w) #bu #bl normalize nodelta
27  whd in match set_8051_sfr; normalize nodelta %
28qed.
29
30lemma set_program_counter_mk_Status_commutation:
31  ∀M: Type[0].
32  ∀cm: M.
33  ∀s: PreStatus M cm.
34  ∀w: Word.
35    set_program_counter M cm s w =
36      mk_PreStatus M cm
37        (low_internal_ram … s)
38        (high_internal_ram … s)
39        (external_ram … s)
40        w
41        (special_function_registers_8051 … s)
42        (special_function_registers_8052 … s)
43        (p1_latch … s)
44        (p3_latch … s)
45        (clock … s).
46  //
47qed.
48
49lemma set_clock_mk_Status_commutation:
50  ∀M: Type[0].
51  ∀cm: M.
52  ∀s: PreStatus M cm.
53  ∀c: nat.
54    set_clock M cm s c =
55      mk_PreStatus M cm
56        (low_internal_ram … s)
57        (high_internal_ram … s)
58        (external_ram … s)
59        (program_counter … s)
60        (special_function_registers_8051 … s)
61        (special_function_registers_8052 … s)
62        (p1_latch … s)
63        (p3_latch … s)
64        c.
65  //
66qed.
67
68lemma get_8051_sfr_set_clock:
69  ∀M: Type[0].
70  ∀cm: M.
71  ∀s: PreStatus M cm.
72  ∀sfr: SFR8051.
73  ∀t: Time.
74    get_8051_sfr M cm (set_clock M cm s t) sfr =
75      get_8051_sfr M cm s sfr.
76  #M #cm #s #sfr #t %
77qed.
78
79lemma get_8051_sfr_set_program_counter:
80  ∀M: Type[0].
81  ∀cm: M.
82  ∀s: PreStatus M cm.
83  ∀sfr: SFR8051.
84  ∀pc: Word.
85    get_8051_sfr M cm (set_program_counter M cm s pc) =
86      get_8051_sfr M cm s.
87  #M #cm #s #sfr #pc %
88qed.
89
90lemma special_function_registers_8051_set_arg_16:
91  ∀M, M': Type[0].
92  ∀cm: M.
93  ∀cm': M'.
94  ∀s: PreStatus M cm.
95  ∀s': PreStatus M' cm'.
96  ∀w, w': Word.
97  ∀d, d': [[dptr]].
98   special_function_registers_8051 ?? s = special_function_registers_8051 … s' →
99    w = w' →
100      special_function_registers_8051 ?? (set_arg_16 … s w d) =
101        special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d').
102  #M #M' #cm #cm' #s #s' #w #w'
103  #d @(subaddressing_mode_elim … d)
104  #d' @(subaddressing_mode_elim … d')
105  #EQ1 #EQ2 <EQ2 normalize cases (vsplit bool 8 8 w) #b1 #b2 normalize <EQ1 %
106qed.
107
108lemma program_counter_set_arg_1:
109  ∀M: Type[0].
110  ∀cm: M.
111  ∀s: PreStatus M cm.
112  ∀addr: [[bit_addr; carry]].
113  ∀b: Bit.
114    program_counter M cm (set_arg_1 M cm s addr b) = program_counter M cm s.
115  #M #cm #s whd in match set_arg_1; cases daemon (* whd in match set_arg_1'; normalize nodelta
116  #addr #b
117  @(subaddressing_mode_elim … addr)
118  [1:
119    #byte cases (vsplit ????) #nu #nl normalize nodelta
120    cases (vsplit ????) #ignore #three_bits normalize nodelta
121    cases (get_index_v bool ????) normalize nodelta
122    [1:
123      @program_counter_set_bit_addressable_sfr
124    |2:
125      @program_counter_set_low_internal_ram
126    ]
127  |2:
128    cases (vsplit ????) //
129  ] *)
130qed.
131
132lemma get_ov_flag_set_program_counter:
133  ∀M: Type[0].
134  ∀cm: M.
135  ∀s: PreStatus M cm.
136  ∀pc: Word.
137    get_ov_flag M cm (set_program_counter M cm s pc) =
138      get_ov_flag M cm s.
139  #M #cm #s #pc %
140qed.
141
142lemma external_ram_set_program_counter:
143  ∀M: Type[0].
144  ∀cm: M.
145  ∀s: PreStatus M cm.
146  ∀pc: Word.
147    external_ram M cm (set_program_counter M cm s pc) =
148      external_ram M cm s.
149  #M #cm #s #pc %
150qed.
151
152lemma low_internal_ram_set_program_counter:
153  ∀M: Type[0].
154  ∀cm: M.
155  ∀s: PreStatus M cm.
156  ∀pc: Word.
157    low_internal_ram M cm (set_program_counter M cm s pc) =
158      low_internal_ram M cm s.
159  #M #cm #s #pc %
160qed.
161
162lemma high_internal_ram_set_program_counter:
163  ∀M: Type[0].
164  ∀cm: M.
165  ∀s: PreStatus M cm.
166  ∀pc: Word.
167    high_internal_ram M cm (set_program_counter M cm s pc) =
168      high_internal_ram M cm s.
169  #M #cm #s #pc %
170qed.
171
172lemma get_arg_8_set_program_counter:
173  ∀M: Type[0].
174  ∀cm: M.
175  ∀s: PreStatus M cm.
176  ∀flag: bool.
177  ∀addr: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; ext_indirect; ext_indirect_dptr]].
178  ∀pc: Word.
179    get_arg_8 M cm (set_program_counter M cm s pc) flag addr =
180      get_arg_8 M cm s flag addr.
181  [2,3:
182    cases addr #subaddressing_mode
183    cases subaddressing_mode
184    try (#addr1 whd in ⊢ (% → %);)
185    whd in ⊢ (% → %); //
186  ]
187  #M #cm #s #flag #addr #pc
188  whd in match get_arg_8; normalize nodelta
189  cases addr *
190  try (#addr1 #absurd normalize in absurd; cases absurd @I)
191  try (#absurd normalize in absurd; cases absurd @I)
192  try (#addr1 #addr2) try #addr1
193  normalize nodelta %
194qed.
195
196lemma external_ram_set_flags:
197  ∀M: Type[0].
198  ∀cm: M.
199  ∀s: PreStatus M cm.
200  ∀opt: option Bit.
201  ∀bit1, bit2: Bit.
202    external_ram M cm (set_flags M cm s bit1 opt bit2) =
203      external_ram M cm s.
204  #M #cm #s #opt #bit1 #bit2 %
205qed.
206
207lemma low_internal_ram_set_flags:
208  ∀M: Type[0].
209  ∀cm: M.
210  ∀s: PreStatus M cm.
211  ∀opt: option Bit.
212  ∀bit1, bit2: Bit.
213    low_internal_ram M cm (set_flags M cm s bit1 opt bit2) =
214      low_internal_ram M cm s.
215  #M #cm #s #opt #bit1 #bit2 %
216qed.
217
218lemma high_internal_ram_set_flags:
219  ∀M: Type[0].
220  ∀cm: M.
221  ∀s: PreStatus M cm.
222  ∀opt: option Bit.
223  ∀bit1, bit2: Bit.
224    high_internal_ram M cm (set_flags M cm s bit1 opt bit2) =
225      high_internal_ram M cm s.
226  #M #cm #s #opt #bit1 #bit2 %
227qed.
228
229lemma low_internal_ram_set_clock:
230  ∀M: Type[0].
231  ∀cm: M.
232  ∀s: PreStatus M cm.
233  ∀t: Time.
234    low_internal_ram M cm (set_clock M cm s t) =
235      low_internal_ram M cm s.
236  #M #cm #s #t %
237qed.
238
239lemma high_internal_ram_set_clock:
240  ∀M: Type[0].
241  ∀cm: M.
242  ∀s: PreStatus M cm.
243  ∀t: Time.
244    high_internal_ram M cm (set_clock M cm s t) =
245      high_internal_ram M cm s.
246  #M #cm #s #t %
247qed.
248
249lemma external_ram_set_clock:
250  ∀M: Type[0].
251  ∀cm: M.
252  ∀s: PreStatus M cm.
253  ∀t: Time.
254    external_ram M cm (set_clock M cm s t) =
255      external_ram M cm s.
256  #M #cm #s #t %
257qed.
258
259lemma set_8051_sfr_set_program_counter:
260  ∀M: Type[0].
261  ∀cm: M.
262  ∀s: PreStatus M cm.
263  ∀pc: Word.
264  ∀sfr: SFR8051.
265  ∀v: Byte.
266    set_8051_sfr M cm (set_program_counter M cm s pc) sfr v =
267      set_program_counter M cm (set_8051_sfr M cm s sfr v) pc.
268  #M #cm #s #pc #sfr #v %
269qed.
270
271lemma low_internal_ram_set_8051_sfr:
272  ∀M: Type[0].
273  ∀cm: M.
274  ∀s: PreStatus M cm.
275  ∀sfr: SFR8051.
276  ∀v: Byte.
277    low_internal_ram M cm (set_8051_sfr M cm s sfr v) =
278      low_internal_ram M cm s.
279  #M #cm #s #sfr #v %
280qed.
281
282lemma high_internal_ram_set_8051_sfr:
283  ∀M: Type[0].
284  ∀cm: M.
285  ∀s: PreStatus M cm.
286  ∀sfr: SFR8051.
287  ∀v: Byte.
288    high_internal_ram M cm (set_8051_sfr M cm s sfr v) =
289      high_internal_ram M cm s.
290  #M #cm #s #sfr #v %
291qed.
292
293lemma external_ram_set_8051_sfr:
294  ∀M: Type[0].
295  ∀cm: M.
296  ∀s: PreStatus M cm.
297  ∀sfr: SFR8051.
298  ∀v: Byte.
299    external_ram M cm (set_8051_sfr M cm s sfr v) =
300      external_ram M cm s.
301  #M #cm #s #sfr #v %
302qed.
303
304lemma get_arg_8_set_clock:
305  ∀M: Type[0].
306  ∀cm: M.
307  ∀s: PreStatus M cm.
308  ∀addr.
309  ∀t: Time.
310    get_arg_8 M cm (set_clock M cm s t) addr =
311      get_arg_8 M cm s addr.
312  #M #cm #s #addr #t %
313qed.
314
315lemma set_program_counter_set_program_counter:
316  ∀M: Type[0].
317  ∀cm: M.
318  ∀s: PreStatus M cm.
319  ∀pc: Word.
320  ∀pc': Word.
321    set_program_counter M cm (set_program_counter M cm s pc) pc' =
322      set_program_counter M cm s pc'.
323  #M #cm #s #pc #pc' %
324qed.
325
326(* XXX: move elsewhere *)
327lemma bitvector_8_cases:
328  ∀w: BitVector 8.
329    ∃b0,b1,b2,b3,b4,b5,b6,b7: bool.
330      w ≃ [[b0;b1;b2;b3;b4;b5;b6;b7]].
331 #w repeat (cases (BitVector_Sn … w)  #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w)
332 >(BitVector_O … w) %
333qed.
334
335(* XXX: not true
336lemma p3_latch_set_arg_8:
337  ∀M: Type[0].
338  ∀cm: M.
339  ∀s: PreStatus M cm.
340  ∀args.
341  ∀v: Byte.
342    p3_latch M cm (set_arg_8 M cm s args v) =
343      p3_latch M cm s.
344  #M #cm #s #args #v
345  @(subaddressing_mode_elim … args)
346  try #w try %
347  whd in match set_arg_8; normalize nodelta
348  whd in match set_arg_8'; normalize nodelta
349  inversion (vsplit bool ???) #nu #nl #nu_nl_refl normalize nodelta
350  inversion (vsplit bool ???) #ignore #three_bits #ignore_three_bits_refl normalize nodelta
351  inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta try %
352  whd in match set_bit_addressable_sfr; normalize nodelta
353  @(bitvector_8_elim_prop … w)
354*)
355
356lemma status_of_pseudo_status_does_not_change_8051_sfrs:
357  ∀M: internal_pseudo_address_map.
358  ∀cm: pseudo_assembly_program.
359  ∀s: PreStatus pseudo_assembly_program cm.
360  ∀sigma: Word → Word.
361  ∀policy: Word → bool.
362    \snd M = data →
363      special_function_registers_8051 pseudo_assembly_program cm s =
364        special_function_registers_8051 (BitVectorTrie Byte 16)
365          (code_memory_of_pseudo_assembly_program cm sigma policy)
366          (status_of_pseudo_status M cm s sigma policy).
367  #M #cm #s #sigma #policy #None_proof cases s
368  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
369  whd in match status_of_pseudo_status; normalize nodelta
370  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
371  >None_proof %
372qed.
373
374lemma n_lt_19_elim_prop:
375  ∀P: nat → Prop.
376    P 0 → P 1 → P 2 → P 3 → P 4 → P 5 → P 6 → P 7 → P 8 → P 9 →
377    P 10 → P 11 → P 12 → P 13 → P 14 → P 15 → P 16 → P 17 → P 18 →
378      (∀n. n < 19 → P n).
379  #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14
380  #H15 #H16 #H17 #H18 #H19 #n
381  cases n [1: // ]
382  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
383  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
384  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
385  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
386  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
387  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
388  #n' normalize in ⊢ (% → ?);
389  #absurd repeat (lapply (le_S_S_to_le … absurd) #absurd)
390  cases (lt_to_not_zero … absurd)
391qed.
392
393lemma get_index_v_set_index_miss:
394  ∀T: Type[0].
395  ∀n, i, j: nat.
396  ∀v: Vector T n.
397  ∀b: T.
398  ∀i_proof: i < n.
399  ∀j_proof: j < n.
400  i ≠ j →
401    get_index_v T n (set_index T n v i b i_proof) j j_proof =
402      get_index_v T n v j j_proof.
403  #T #n #i #j #v lapply i lapply j elim v #i #j
404  [1:
405    #b #i_proof
406    cases (lt_to_not_zero … i_proof)
407  |2:
408    #tl #inductive_hypothesis #j' #i' #b #i_proof #j_proof #i_neq_j
409    lapply i_proof lapply i_neq_j cases i'
410    [1:
411      -i_neq_j #i_neq_j -i_proof #i_proof
412      whd in match (set_index ??????);
413      lapply j_proof lapply i_neq_j cases j'
414      [1:
415        #relevant @⊥ cases relevant -relevant #absurd @absurd %
416      |2:
417        #j' #_ -j_proof #j_proof %
418      ]
419    |2:
420      #i' -i_neq_j #i_neq_j -i_proof #i_proof
421      lapply j_proof lapply i_neq_j cases j'
422      [1:
423        #_ #j_proof %
424      |2:
425        #j' #i_neq_j #j_proof
426        @inductive_hypothesis @nmk #relevant
427        cases i_neq_j #absurd @absurd >relevant %
428      ]
429    ]
430  ]
431qed.
432
433lemma get_index_v_special_function_registers_8051_not_acc_a:
434  ∀M: internal_pseudo_address_map.
435  ∀cm: pseudo_assembly_program.
436  ∀s: PreStatus pseudo_assembly_program cm.
437  ∀sigma: Word → Word.
438  ∀policy: Word → bool.
439  ∀n: nat.
440  ∀proof: n < 19.
441    n ≠ 17 →
442   (get_index_v Byte 19
443    (special_function_registers_8051 pseudo_assembly_program cm s) n
444    proof =
445   get_index_v Byte 19
446     (special_function_registers_8051 (BitVectorTrie Byte 16)
447       (code_memory_of_pseudo_assembly_program cm sigma policy)
448       (status_of_pseudo_status M cm s sigma policy)) n
449       proof).
450  #M #cm #s #sigma #policy #n #proof lapply proof
451  @(n_lt_19_elim_prop … proof) -proof #proof
452  [18:
453    #absurd @⊥ cases absurd -absurd #absurd @absurd %
454  ]
455  #_ cases s #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
456  whd in match status_of_pseudo_status; normalize nodelta
457  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
458  cases M #left #right cases right normalize nodelta try %
459  -right * #address
460  @pair_elim #high #low #high_low_refl normalize nodelta
461  whd in match sfr_8051_index; normalize nodelta
462  >get_index_v_set_index_miss try %
463  #absurd destruct(absurd)
464qed.
465
466(*
467include alias "arithmetics/nat.ma".
468include alias "basics/logic.ma".
469include alias "ASM/BitVectorTrie.ma".
470*)
471
472lemma get_8051_sfr_status_of_pseudo_status:
473  ∀M.
474  ∀cm, ps, sigma, policy.
475  ∀sfr.
476    (sfr = SFR_ACC_A → \snd M = data) →
477    get_8051_sfr (BitVectorTrie Byte 16)
478      (code_memory_of_pseudo_assembly_program cm sigma policy)
479      (status_of_pseudo_status M cm ps sigma policy) sfr =
480    get_8051_sfr pseudo_assembly_program cm ps sfr.
481  #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant
482  [18:
483     >relevant %
484  ]
485  cases sndM try % * #address
486  whd in match get_8051_sfr;
487  whd in match status_of_pseudo_status; normalize nodelta
488  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
489  @pair_elim #upper #lower #upper_lower_refl
490  @get_index_v_set_index_miss @nmk #relevant
491  normalize in relevant; destruct(relevant)
492qed.
493
494lemma bitvector_cases_hd_tl:
495  ∀n: nat.
496  ∀w: BitVector (S n).
497   ∃hd: bool. ∃tl: BitVector n.
498    w ≃ hd:::tl.
499  #n #w cases (BitVector_Sn … w) #hd #relevant %{hd} @relevant
500qed.
501
502lemma external_ram_set_bit_addressable_sfr:
503  ∀M: Type[0].
504  ∀cm: M.
505  ∀ps.
506  ∀w.
507  ∀result: Byte.
508    external_ram M cm
509      (set_bit_addressable_sfr M cm ps w result) =
510    external_ram M cm ps.
511  #M #cm #ps #w #result cases daemon (* XXX: prove this with Russell in Status.ma!
512  whd in match set_bit_addressable_sfr; normalize nodelta
513  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
514  cases (eqb ??) normalize nodelta [1: % ]
515  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
516  cases (eqb ??) normalize nodelta [1: % ]
517  cases (eqb ??) normalize nodelta [1: % ]
518  cases (eqb ??) normalize nodelta [1: % ]
519  cases (eqb ??) normalize nodelta [1: % ]
520  cases (eqb ??) normalize nodelta [1: % ]
521  cases (eqb ??) normalize nodelta [1: % ]
522  cases (eqb ??) normalize nodelta [1: % ]
523  cases (eqb ??) normalize nodelta [1: % ]
524  cases (eqb ??) normalize nodelta [1: % ]
525  cases (eqb ??) normalize nodelta [1: % ]
526  cases (eqb ??) normalize nodelta [1: % ]
527  cases (eqb ??) normalize nodelta [1: % ]
528  cases (eqb ??) normalize nodelta [1: % ]
529  cases (eqb ??) normalize nodelta [1: % ]
530  cases (eqb ??) normalize nodelta [1: % ]
531  cases (eqb ??) normalize nodelta [1: % ]
532  cases (eqb ??) normalize nodelta [1: % ]
533  cases (eqb ??) normalize nodelta [1: % ]
534  cases (eqb ??) normalize nodelta [1: % ]
535  cases (eqb ??) normalize nodelta [1: % ]
536  cases (eqb ??) normalize nodelta [1: % ]
537  cases (eqb ??) normalize nodelta [1: % ]
538  cases (eqb ??) normalize nodelta [1: % ]
539  cases not_implemented *)
540qed.
541
542lemma external_ram_set_arg_8:
543  ∀M: Type[0].
544  ∀cm: M.
545  ∀ps.
546  ∀addr1: [[direct; indirect; registr; acc_a; acc_b ]].
547  ∀result.
548    external_ram M cm (set_arg_8 M cm ps addr1 result) =
549      external_ram M cm ps.
550  [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
551  #M #cm #ps #addr1 #result
552  @(subaddressing_mode_elim … addr1) try #w try %
553  whd in ⊢ (??(???%)?); cases daemon (*whd in ⊢ (??(???(???%))?); (* XXX: to be understood, slow match *)
554  [1:
555    cases (vsplit bool ???) #nu #nl normalize nodelta
556    cases (vsplit bool ???) #ignore #three_bits normalize nodelta
557    cases (get_index_v bool ????) normalize nodelta try %
558    @external_ram_set_bit_addressable_sfr
559  |2:
560    cases (vsplit bool ???) #nu #nl normalize nodelta
561    cases (vsplit bool ???) #ignore #three_bits normalize nodelta
562    cases (get_index_v bool ????) normalize nodelta %
563  ] *)
564qed.
565
566lemma special_function_registers_8051_set_clock:
567  ∀M: Type[0].
568  ∀cm: M.
569  ∀ps.
570  ∀t.
571    special_function_registers_8051 M cm (set_clock M cm ps t) =
572      special_function_registers_8051 M cm ps.
573  //
574qed.
575
576lemma get_arg_8_pseudo_addressing_mode_ok:
577  ∀M: internal_pseudo_address_map.
578  ∀cm: pseudo_assembly_program.
579  ∀ps: PreStatus pseudo_assembly_program cm.
580  ∀sigma: Word → Word.
581  ∀policy: Word → bool.
582  ∀addr1: [[registr; direct]].
583    addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →
584      get_arg_8 (BitVectorTrie Byte 16)
585        (code_memory_of_pseudo_assembly_program cm sigma policy)
586        (status_of_pseudo_status M cm ps sigma policy) true addr1 =
587      get_arg_8 pseudo_assembly_program cm ps true addr1.
588  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
589  #M #cm #ps #sigma #policy #addr1
590  @(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%);
591  [1:
592    whd in ⊢ (??%? → ??%?);
593    whd in match bit_address_of_register; normalize nodelta
594    @pair_elim #un #ln #un_ln_refl
595    lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
596    @(pair_replace ?????????? un_ln_refl)
597    [1:
598      whd in match get_8051_sfr; normalize nodelta
599      whd in match sfr_8051_index; normalize nodelta
600      @eq_f <get_index_v_special_function_registers_8051_not_acc_a
601      try % #absurd destruct(absurd)
602    |2:
603      #assembly_mode_ok_refl
604      >low_internal_ram_of_pseudo_internal_ram_miss
605      [1:
606        %
607      |2:
608        cases (assoc_list_exists ?????) in assembly_mode_ok_refl; normalize nodelta
609        #absurd try % @sym_eq assumption
610      ]
611    ]
612  |2:
613    #addressing_mode_ok_refl whd in ⊢ (??%?);
614    @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (*
615    @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
616    inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
617    [1:
618      whd in ⊢ (??%%); normalize nodelta
619      cases (eqb ??) normalize nodelta [1: % ]
620      cases (eqb ??) normalize nodelta [1: % ]
621      cases (eqb ??) normalize nodelta [1: % ]
622      cases (eqb ??) normalize nodelta [1: % ]
623      cases (eqb ??) normalize nodelta [1:
624        @get_8051_sfr_status_of_pseudo_status
625        #absurd destruct(absurd)
626      ]
627      cases (eqb ??) normalize nodelta [1:
628        @get_8051_sfr_status_of_pseudo_status
629        #absurd destruct(absurd)
630      ]
631      cases (eqb ??) normalize nodelta [1:
632        @get_8051_sfr_status_of_pseudo_status
633        #absurd destruct(absurd)
634      ]
635      cases (eqb ??) normalize nodelta [1:
636        @get_8051_sfr_status_of_pseudo_status
637        #absurd destruct(absurd)
638      ]
639      cases (eqb ??) normalize nodelta [1:
640        @get_8051_sfr_status_of_pseudo_status
641        #absurd destruct(absurd)
642      ]
643      cases (eqb ??) normalize nodelta [1: % ]
644      cases (eqb ??) normalize nodelta [1: % ]
645      cases (eqb ??) normalize nodelta [1: % ]
646      cases (eqb ??) normalize nodelta [1: % ]
647      cases (eqb ??) normalize nodelta [1: % ]
648      cases (eqb ??) normalize nodelta [1:
649        @get_8051_sfr_status_of_pseudo_status
650        #absurd destruct(absurd)
651      ]
652      cases (eqb ??) normalize nodelta [1:
653        @get_8051_sfr_status_of_pseudo_status
654        #absurd destruct(absurd)
655      ]
656      cases (eqb ??) normalize nodelta [1:
657        @get_8051_sfr_status_of_pseudo_status
658        #absurd destruct(absurd)
659      ]
660      cases (eqb ??) normalize nodelta [1:
661        @get_8051_sfr_status_of_pseudo_status
662        #absurd destruct(absurd)
663      ]
664      cases (eqb ??) normalize nodelta [1:
665        @get_8051_sfr_status_of_pseudo_status
666        #absurd destruct(absurd)
667      ]
668      cases (eqb ??) normalize nodelta [1:
669        @get_8051_sfr_status_of_pseudo_status
670        #absurd destruct(absurd)
671      ]
672      cases (eqb ??) normalize nodelta [1:
673        @get_8051_sfr_status_of_pseudo_status
674        #absurd destruct(absurd)
675      ]
676      cases (eqb ??) normalize nodelta [1:
677        @get_8051_sfr_status_of_pseudo_status
678        #absurd destruct(absurd)
679      ]
680      cases (eqb ??) normalize nodelta [1:
681        @get_8051_sfr_status_of_pseudo_status
682        #absurd destruct(absurd)
683      ]
684      cases (eqb ??) normalize nodelta [1:
685        @get_8051_sfr_status_of_pseudo_status
686        #absurd destruct(absurd)
687      ]
688      inversion (eqb ??) #eqb_refl normalize nodelta [1:
689        @get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl
690        whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl)
691        >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
692        #assoc_list_assm cases (conjunction_true … assoc_list_assm) #_
693        #relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) %
694      ]
695      cases (eqb ??) normalize nodelta [1:
696        @get_8051_sfr_status_of_pseudo_status
697        #absurd destruct(absurd)
698      ] %
699    |2:
700      lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant
701      whd in match status_of_pseudo_status; normalize nodelta
702      >low_internal_ram_of_pseudo_internal_ram_miss try %
703      cut(arg = false:::(three_bits@@nl))
704      [1:
705        <get_index_v_refl
706        cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits)
707        [1:
708          cut(ignore = [[get_index_v bool 4 nu 0 ?]])
709          [1:
710            @le_S_S @le_O_n
711          |2:
712            cut(ignore = \fst (vsplit bool 1 3 nu))
713            [1:
714              >ignore_three_bits_refl %
715            |2:
716              #ignore_refl >ignore_refl
717              cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl
718              >nu_refl %
719            ]
720          |3:
721            #ignore_refl >ignore_refl in ignore_three_bits_refl;
722            #relevant lapply (vsplit_ok ?????? (sym_eq … relevant))
723            #nu_refl <nu_refl %
724          ]
725        |2:
726          #nu_refl change with (? = (?:::three_bits)@@?) <nu_refl
727          @sym_eq @vsplit_ok >nu_nl_refl %
728        ]
729      |2:
730        #arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant;
731        normalize nodelta
732        [1:
733          cases (eq_bv ???) normalize #absurd destruct(absurd)
734        |2:
735          #_ %
736        ]
737      ]
738    ]
739  ] *)
740qed.
741
742lemma special_function_registers_8051_set_program_counter:
743  ∀M: Type[0].
744  ∀cm: M.
745  ∀ps.
746  ∀pc: Word.
747    special_function_registers_8051 M cm (set_program_counter M cm ps pc) =
748      special_function_registers_8051 M cm ps.
749  //
750qed.
751
752lemma special_function_registers_8052_set_program_counter:
753  ∀M: Type[0].
754  ∀cm: M.
755  ∀ps.
756  ∀pc: Word.
757    special_function_registers_8052 M cm (set_program_counter M cm ps pc) =
758      special_function_registers_8052 M cm ps.
759  //
760qed.
761
762lemma set_index_set_index_commutation:
763  ∀A: Type[0].
764  ∀n: nat.
765  ∀v: Vector A n.
766  ∀m, o: nat.
767  ∀m_lt_proof: m < n.
768  ∀o_lt_proof: o < n.
769  ∀e, f: A.
770    m ≠ o →
771      set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof =
772        set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof.
773  #A #n #v elim v
774  [1:
775    #m #o #m_lt_proof
776    normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof)
777  |2:
778    #n' #hd #tl #inductive_hypothesis
779    #m #o
780    cases m cases o
781    [1:
782      #m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant
783      @relevant %
784    |2,3:
785      #o' normalize //
786    |4:
787      #m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm
788      normalize @eq_f @inductive_hypothesis @nmk #relevant
789      >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) %
790    ]
791  ]
792qed.
793
794lemma special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051:
795  ∀M: internal_pseudo_address_map.
796  ∀cm: pseudo_assembly_program.
797  ∀ps.
798  ∀sigma: Word → Word.
799  ∀policy: Word → bool.
800  ∀sfr.
801  ∀result: Byte.
802    eqb (sfr_8051_index sfr) (sfr_8051_index SFR_ACC_A) = false →
803      special_function_registers_8051 (BitVectorTrie Byte 16)
804        (code_memory_of_pseudo_assembly_program cm sigma policy)
805        (set_8051_sfr (BitVectorTrie Byte 16)
806        (code_memory_of_pseudo_assembly_program cm sigma policy)
807        (status_of_pseudo_status M cm ps sigma policy) sfr result) =
808      sfr_8051_of_pseudo_sfr_8051 M
809        (special_function_registers_8051 pseudo_assembly_program cm
810        (set_8051_sfr pseudo_assembly_program cm ps sfr result)) sigma.
811  #M #cm #ps #sigma #policy #sfr #result #sfr_neq_assm
812  whd in match (set_8051_sfr ?????);
813  cases M #callM * try % #upper_lower #address
814  whd in match (special_function_registers_8051 ???);
815  whd in match (sfr_8051_of_pseudo_sfr_8051 ???);
816  @pair_elim #high #low #high_low_refl normalize nodelta
817  cases (eq_upper_lower ??) normalize nodelta
818  whd in match (set_8051_sfr ?????);
819  @set_index_set_index_commutation @nmk #relevant
820  @(absurd ? relevant (eqb_false_to_not_eq ?? sfr_neq_assm))
821qed.
822
823lemma special_function_registers_8051_set_arg_8:
824  ∀M: internal_pseudo_address_map.
825  ∀cm: pseudo_assembly_program.
826  ∀ps.
827  ∀sigma: Word → Word.
828  ∀policy: Word → bool.
829  ∀addr1: [[ registr; direct ]].
830  ∀result.
831    addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →
832    special_function_registers_8051 (BitVectorTrie Byte 16)
833      (code_memory_of_pseudo_assembly_program cm sigma policy)
834      (set_arg_8 (BitVectorTrie Byte 16)
835        (code_memory_of_pseudo_assembly_program cm sigma policy)
836        (status_of_pseudo_status M cm ps sigma policy) addr1 result) =
837   sfr_8051_of_pseudo_sfr_8051 M
838     (special_function_registers_8051 pseudo_assembly_program cm
839     (set_arg_8 pseudo_assembly_program cm ps addr1 result)) sigma.
840  cases daemon
841(*
842  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
843  #M #cm #ps #sigma #policy #addr1 #result
844  @(subaddressing_mode_elim … addr1) #w #addressing_mode_ok_refl try %
845  whd in match (set_arg_8 ?????); whd in ⊢ (??(???(???%))?);
846  whd in match (set_arg_8 ?????) in ⊢ (???%); whd in ⊢ (???(??(???(???%))?));
847  cases (vsplit bool ???) #nu #nl normalize nodelta
848  cases (vsplit bool ???) #ignore #three_bits normalize nodelta
849  cases (get_index_v bool ????) normalize nodelta try %
850  whd in match (set_bit_addressable_sfr ?????); whd in match (set_bit_addressable_sfr ?????) in ⊢ (???%);
851  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
852  cases (eqb ??) normalize nodelta [1: % ]
853  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
854  cases (eqb ??) normalize nodelta [1: % ]
855  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
856  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
857  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
858  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
859  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
860  cases (eqb ??) normalize nodelta [1: % ]
861  cases (eqb ??) normalize nodelta [1: % ]
862  cases (eqb ??) normalize nodelta [1: % ]
863  cases (eqb ??) normalize nodelta [1: % ]
864  cases (eqb ??) normalize nodelta [1: % ]
865  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
866  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
867  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
868  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
869  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
870  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
871  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
872  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
873  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
874  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
875  inversion (eqb ??) #eqb_refl normalize nodelta [1:
876    whd in addressing_mode_ok_refl:(??%?); <(eqb_true_to_eq … eqb_refl) in addressing_mode_ok_refl;
877    >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
878    #relevant cases (conjunction_true … relevant) #_ #eq_acc_assm
879    whd in match (status_of_pseudo_status ?????);
880    whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
881    >(eq_accumulator_address_map_entry_true_to_eq … eq_acc_assm) normalize nodelta %
882  ]
883  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
884  cases not_implemented *)
885qed.
Note: See TracBrowser for help on using the repository browser.