source: src/ASM/StatusProofsSplit.ma @ 2274

Last change on this file since 2274 was 2274, checked in by sacerdot, 8 years ago

Dead code commented out and code out of place moved to Test.ma.

File size: 20.7 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
605(*CSC: dead and unfinished code
606lemma special_function_registers_8051_set_arg_8:
607  ∀M: internal_pseudo_address_map.
608  ∀cm: pseudo_assembly_program.
609  ∀ps.
610  ∀sigma: Word → Word.
611  ∀policy: Word → bool.
612  ∀addr1: [[ registr; direct ]].
613  ∀result.
614    addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →
615    special_function_registers_8051 (BitVectorTrie Byte 16)
616      (code_memory_of_pseudo_assembly_program cm sigma policy)
617      (set_arg_8 (BitVectorTrie Byte 16)
618        (code_memory_of_pseudo_assembly_program cm sigma policy)
619        (status_of_pseudo_status M cm ps sigma policy) addr1 result) =
620   sfr_8051_of_pseudo_sfr_8051 M
621     (special_function_registers_8051 pseudo_assembly_program cm
622     (set_arg_8 pseudo_assembly_program cm ps addr1 result)) sigma.
623  cases daemon
624(*
625  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
626  #M #cm #ps #sigma #policy #addr1 #result
627  @(subaddressing_mode_elim … addr1) #w #addressing_mode_ok_refl try %
628  whd in match (set_arg_8 ?????); whd in ⊢ (??(???(???%))?);
629  whd in match (set_arg_8 ?????) in ⊢ (???%); whd in ⊢ (???(??(???(???%))?));
630  cases (vsplit bool ???) #nu #nl normalize nodelta
631  cases (vsplit bool ???) #ignore #three_bits normalize nodelta
632  cases (get_index_v bool ????) normalize nodelta try %
633  whd in match (set_bit_addressable_sfr ?????); whd in match (set_bit_addressable_sfr ?????) in ⊢ (???%);
634  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
635  cases (eqb ??) normalize nodelta [1: % ]
636  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
637  cases (eqb ??) normalize nodelta [1: % ]
638  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
639  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
640  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
641  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
642  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
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: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
649  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
650  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
651  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
652  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
653  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
654  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
655  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
656  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
657  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
658  inversion (eqb ??) #eqb_refl normalize nodelta [1:
659    whd in addressing_mode_ok_refl:(??%?); <(eqb_true_to_eq … eqb_refl) in addressing_mode_ok_refl;
660    >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
661    #relevant cases (conjunction_true … relevant) #_ #eq_acc_assm
662    whd in match (status_of_pseudo_status ?????);
663    whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
664    >(eq_accumulator_address_map_entry_true_to_eq … eq_acc_assm) normalize nodelta %
665  ]
666  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
667  cases not_implemented *)
668qed.
669*)
Note: See TracBrowser for help on using the repository browser.