source: src/ASM/Test.ma @ 2171

Last change on this file since 2171 was 2171, checked in by mulligan, 6 years ago

Finished the commutations
File size: 58.7 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "ASM/Assembly.ma".
16include "ASM/Interpret.ma".
17include "ASM/StatusProofs.ma".
18include alias "arithmetics/nat.ma".
19include "ASM/AssemblyProof.ma".
20
21lemma set_program_counter_status_of_pseudo_status:
22  ∀M.
23  ∀cm.
24  ∀ps.
25  ∀sigma.
26  ∀policy.
27  ∀new_ppc.
28    set_program_counter (BitVectorTrie Byte 16)
29      (code_memory_of_pseudo_assembly_program cm sigma policy)
30      (status_of_pseudo_status M cm ps sigma policy)
31      (sigma new_ppc) =
32    status_of_pseudo_status M cm (set_program_counter … cm ps new_ppc) sigma policy.
33  //
34qed.
35
36lemma set_p1_latch_status_of_pseudo_status:
37  ∀M.
38  ∀code_memory.
39  ∀sigma.
40  ∀policy.
41  ∀s.
42  ∀v.
43    set_p1_latch (BitVectorTrie Byte 16)
44      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
45      (status_of_pseudo_status M code_memory s sigma policy) v =
46    status_of_pseudo_status M code_memory
47      (set_p1_latch pseudo_assembly_program code_memory s v) sigma policy.
48  //
49qed.
50
51lemma set_p3_latch_status_of_pseudo_status:
52  ∀M.
53  ∀code_memory.
54  ∀sigma.
55  ∀policy.
56  ∀s.
57  ∀v.
58    set_p3_latch (BitVectorTrie Byte 16)
59      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
60      (status_of_pseudo_status M code_memory s sigma policy) v =
61    status_of_pseudo_status M code_memory
62      (set_p3_latch pseudo_assembly_program code_memory s v) sigma policy.
63  //
64qed.
65
66definition map_acc_a_using_internal_pseudo_address_map:
67    ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte ≝
68  λM, sigma, v.
69  match \snd M with
70  [ data ⇒ v
71  | address upper_lower word ⇒
72    let mapped ≝ sigma word in
73    let 〈high, low〉 ≝ vsplit bool 8 8 mapped in
74      if eq_upper_lower upper_lower upper then
75        high
76      else
77        low
78  ].
79
80(*CSC: Taken from AssemblyProofSplit.ma; there named map_lower_internal... *)
81definition map_internal_ram_address_using_pseudo_address_map:
82  ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝
83  λM: internal_pseudo_address_map.
84  λsigma: Word → Word.
85  λaddress: Byte.
86  λvalue: Byte.
87  match assoc_list_lookup ?? address (eq_bv …) (\fst M) with
88  [ None ⇒ value
89  | Some upper_lower_word ⇒
90    let 〈upper_lower, word〉 ≝ upper_lower_word in
91    let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in
92      if eq_upper_lower upper_lower upper then
93        high
94      else
95        low
96  ].
97
98definition map_address_using_internal_pseudo_address_map:
99    ∀M: internal_pseudo_address_map. (Word → Word) → SFR8051 → Byte → Byte ≝
100  λM, sigma, sfr, v.
101  match sfr with
102  [ SFR_ACC_A ⇒ map_acc_a_using_internal_pseudo_address_map M sigma v
103  | _         ⇒ v
104  ].
105
106lemma set_index_set_index_overwrite:
107  ∀A: Type[0].
108  ∀n: nat.
109  ∀v: Vector A n.
110  ∀index: nat.
111  ∀e, e': A.
112  ∀proof.
113  ∀proof'.
114    set_index A n v index e proof =
115      set_index A n (set_index A n v index e' proof') index e proof.
116  #A #n #v elim v normalize
117  [1:
118    #index #e #e' #absurd cases (lt_to_not_zero … absurd)
119  |2:
120    #n' #hd #tl #inductive_hypothesis #index #e #e' cases index #proof #proof'
121    normalize //
122  ]
123qed.
124
125lemma set_index_set_index_commutation:
126  ∀A: Type[0].
127  ∀n: nat.
128  ∀v: Vector A n.
129  ∀m, o: nat.
130  ∀m_lt_proof: m < n.
131  ∀o_lt_proof: o < n.
132  ∀e, f: A.
133    m ≠ o →
134      set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof =
135        set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof.
136  #A #n #v elim v
137  [1:
138    #m #o #m_lt_proof
139    normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof)
140  |2:
141    #n' #hd #tl #inductive_hypothesis
142    #m #o
143    cases m cases o
144    [1:
145      #m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant
146      @relevant %
147    |2,3:
148      #o' normalize //
149    |4:
150      #m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm
151      normalize @eq_f @inductive_hypothesis @nmk #relevant
152      >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) %
153    ]
154  ]
155qed.
156
157(* XXX: move elsewhere *)
158lemma get_index_v_set_index_miss:
159  ∀a: Type[0].
160  ∀n: nat.
161  ∀v: Vector a n.
162  ∀i, j: nat.
163  ∀e: a.
164  ∀i_proof: i < n.
165  ∀j_proof: j < n.
166    i ≠ j →
167      get_index_v a n (set_index a n v i e i_proof) j j_proof =
168        get_index_v a n v j j_proof.
169  #a #n #v elim v
170  [1:
171    #i #j #e #i_proof
172    cases (lt_to_not_zero … i_proof)
173  |2:
174    #n' #hd #tl #inductive_hypothesis #i #j
175    cases i cases j
176    [1:
177      #e #i_proof #j_proof #neq_assm
178      cases (absurd ? (refl … 0) neq_assm)
179    |2,3:
180      #i' #e #i_proof #j_proof #_ %
181    |4:
182      #i' #j' #e #i_proof #j_proof #neq_assm
183      @inductive_hypothesis @nmk #eq_assm
184      >eq_assm in neq_assm; #neq_assm
185      cases (absurd ? (refl ??) neq_assm)
186    ]
187  ]
188qed.
189
190lemma set_index_status_of_pseudo_status:
191  ∀M, code_memory, sigma, policy, s, sfr, v, v'.
192    map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
193(set_index Byte 19
194  (special_function_registers_8051 (BitVectorTrie Byte 16)
195   (code_memory_of_pseudo_assembly_program code_memory sigma policy)
196   (status_of_pseudo_status M code_memory s sigma policy))
197  (sfr_8051_index sfr) v' (sfr8051_index_19 sfr)
198  =sfr_8051_of_pseudo_sfr_8051 M
199   (special_function_registers_8051 pseudo_assembly_program code_memory
200    (set_8051_sfr pseudo_assembly_program code_memory s sfr v)) sigma).
201  #M #code_memory #sigma #policy #s #sfr #v #v' #sfr_neq_acc_a_assm
202  whd in match status_of_pseudo_status; normalize nodelta
203  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
204  inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta
205  [1:
206    <sfr_neq_acc_a_assm cases sfr
207    [18:
208      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
209      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
210      >sndM_refl %
211    ]
212    %
213  |2:
214    @pair_elim #high #low #high_low_refl normalize nodelta
215    inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
216    <sfr_neq_acc_a_assm cases sfr
217    [18,37:
218      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
219      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
220      >sndM_refl normalize nodelta >high_low_refl normalize nodelta
221      >eq_upper_lower_refl normalize nodelta
222      whd in match (set_8051_sfr ?????);
223      [1:
224        <set_index_set_index_overwrite in ⊢ (??%?);
225        <set_index_set_index_overwrite in ⊢ (???%); %
226      |2:
227        <set_index_set_index_overwrite in ⊢ (??%?);
228        <set_index_set_index_overwrite in ⊢ (???%); %
229      ]
230    ]
231    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
232    whd in match (set_8051_sfr ?????); @set_index_set_index_commutation normalize
233    @nmk #absurd destruct(absurd)
234  ]
235qed.
236
237lemma get_index_v_status_of_pseudo_status:
238  ∀M, code_memory, sigma, policy, s, sfr.
239    (get_index_v Byte 19
240      (special_function_registers_8051 (BitVectorTrie Byte 16)
241      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
242      (status_of_pseudo_status M code_memory s sigma policy))
243      (sfr_8051_index sfr) (sfr8051_index_19 sfr) =
244    map_address_using_internal_pseudo_address_map M sigma sfr
245      (get_index_v Byte 19
246        (special_function_registers_8051 pseudo_assembly_program code_memory s)
247        (sfr_8051_index sfr) (sfr8051_index_19 sfr))).
248  #M #code_memory #sigma #policy #s #sfr
249  whd in match status_of_pseudo_status; normalize nodelta
250  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
251  inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta
252 [1:
253    cases sfr
254    [18:
255      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
256      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
257      >sndM_refl %
258    ]
259    %
260  |2:
261    @pair_elim #high #low #high_low_refl normalize nodelta
262    inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
263    cases sfr
264    [18,37:
265      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
266      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
267      >sndM_refl normalize nodelta >high_low_refl normalize nodelta
268      >eq_upper_lower_refl normalize nodelta
269      whd in match (set_8051_sfr ?????); //
270    ]
271    @get_index_v_set_index_miss whd in ⊢ (?(??%%));
272    @nmk #absurd destruct(absurd)
273  ]
274qed.
275
276lemma set_8051_sfr_status_of_pseudo_status:
277  ∀M, code_memory, sigma, policy, s, sfr, v,v'.
278  map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
279(set_8051_sfr (BitVectorTrie Byte 16)
280  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
281  (status_of_pseudo_status M code_memory s sigma policy) sfr v'
282  =status_of_pseudo_status M code_memory
283   (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
284  #M #code_memory #sigma #policy #s #sfr #v #v' #v_ok
285  whd in ⊢ (??%%); @split_eq_status try % /2/
286qed.
287
288lemma get_8051_sfr_status_of_pseudo_status:
289  ∀M, code_memory, sigma, policy, s, sfr.
290  (get_8051_sfr (BitVectorTrie Byte 16)
291    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
292    (status_of_pseudo_status M code_memory s sigma policy) sfr =
293  map_address_using_internal_pseudo_address_map M sigma sfr
294   (get_8051_sfr pseudo_assembly_program code_memory s sfr)).
295  #M #code_memory #sigma #policy #s #sfr
296  whd in match get_8051_sfr; normalize nodelta
297  @get_index_v_status_of_pseudo_status
298qed.
299
300lemma get_8052_sfr_status_of_pseudo_status:
301  ∀M, code_memory, sigma, policy, s, sfr.
302  (get_8052_sfr (BitVectorTrie Byte 16)
303    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
304    (status_of_pseudo_status M code_memory s sigma policy) sfr =
305   (get_8052_sfr pseudo_assembly_program code_memory s sfr)).
306  //
307qed.
308
309lemma set_8052_sfr_status_of_pseudo_status:
310  ∀M, code_memory, sigma, policy, s, sfr, v.
311(set_8052_sfr (BitVectorTrie Byte 16)
312  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
313  (status_of_pseudo_status M code_memory s sigma policy) sfr v
314  =status_of_pseudo_status M code_memory
315   (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
316 //
317qed.
318
319definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝
320  λb: Byte.
321    let address ≝ nat_of_bitvector … b in
322      if (eqb address 128) then None ?
323      else if (eqb address 144) then Some … (inl … SFR_P1)
324      else if (eqb address 160) then None ?
325      else if (eqb address 176) then Some … (inl … SFR_P3)
326      else if (eqb address 153) then Some … (inl … SFR_SBUF)
327      else if (eqb address 138) then Some … (inl … SFR_TL0)
328      else if (eqb address 139) then Some … (inl … SFR_TL1)
329      else if (eqb address 140) then Some … (inl … SFR_TH0)
330      else if (eqb address 141) then Some … (inl … SFR_TH1)
331      else if (eqb address 200) then Some … (inr … SFR_T2CON)
332      else if (eqb address 202) then Some … (inr … SFR_RCAP2L)
333      else if (eqb address 203) then Some … (inr … SFR_RCAP2H)
334      else if (eqb address 204) then Some … (inr … SFR_TL2)
335      else if (eqb address 205) then Some … (inr … SFR_TH2)
336      else if (eqb address 135) then Some … (inl … SFR_PCON)
337      else if (eqb address 136) then Some … (inl … SFR_TCON)
338      else if (eqb address 137) then Some … (inl … SFR_TMOD)
339      else if (eqb address 152) then Some … (inl … SFR_SCON)
340      else if (eqb address 168) then Some … (inl … SFR_IE)
341      else if (eqb address 184) then Some … (inl … SFR_IP)
342      else if (eqb address 129) then Some … (inl … SFR_SP)
343      else if (eqb address 130) then Some … (inl … SFR_DPL)
344      else if (eqb address 131) then Some … (inl … SFR_DPH)
345      else if (eqb address 208) then Some … (inl … SFR_PSW)
346      else if (eqb address 224) then Some … (inl … SFR_ACC_A)
347      else if (eqb address 240) then Some … (inl … SFR_ACC_B)
348      else None ?.
349
350definition set_bit_addressable_sfr:
351    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte →
352      PreStatus M code_memory ≝
353  λM: Type[0].
354  λcode_memory:M.
355  λs: PreStatus M code_memory.
356  λb: Byte.
357  λv: Byte.
358   match sfr_of_Byte b with
359   [ None ⇒ match not_implemented in False with [ ]
360   | Some sfr8051_8052 ⇒
361      match sfr8051_8052 with
362      [ inl sfr ⇒
363         match sfr with
364         [ SFR_P1 ⇒
365           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
366           set_p1_latch ?? s v
367         | SFR_P3 ⇒
368           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
369           set_p3_latch ?? s v
370         | _ ⇒ set_8051_sfr ?? s sfr v ]
371      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]].
372
373definition map_address_Byte_using_internal_pseudo_address_map ≝
374 λM,sigma,d,v.
375  match sfr_of_Byte d with
376  [ None ⇒ v
377  | Some sfr8051_8052 ⇒
378     match sfr8051_8052 with
379     [ inl sfr ⇒
380        map_address_using_internal_pseudo_address_map M sigma sfr v
381     | inr _ ⇒ v ]].
382
383lemma set_bit_addressable_sfr_status_of_pseudo_status':
384      let M ≝ pseudo_assembly_program in ∀code_memory: M. ∀s: PreStatus M code_memory. ∀d: Byte. ∀v: Byte.
385        Σp: PreStatus M code_memory. ∀M. ∀sigma. ∀policy. ∀v'.
386  map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
387 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
388  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
389  (status_of_pseudo_status M code_memory s sigma policy) d v'
390  =status_of_pseudo_status M code_memory
391   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
392  whd in match set_bit_addressable_sfr;
393  whd in match map_address_Byte_using_internal_pseudo_address_map;
394  normalize nodelta
395  @(let M ≝ pseudo_assembly_program in
396  λcode_memory:M.
397  λs: PreStatus M code_memory.
398  λb: Byte.
399  λv: Byte.
400   match sfr_of_Byte b with
401   [ None ⇒ match not_implemented in False with [ ]
402   | Some sfr8051_8052 ⇒
403      match sfr8051_8052 with
404      [ inl sfr ⇒
405         match sfr with
406         [ SFR_P1 ⇒
407           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
408           set_p1_latch ?? s v
409         | SFR_P3 ⇒
410           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
411           set_p3_latch ?? s v
412         | _ ⇒ set_8051_sfr ?? s sfr v ]
413      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]])
414 normalize nodelta
415 /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/
416 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta //
417qed.
418
419lemma set_bit_addressable_sfr_status_of_pseudo_status:
420 ∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte.
421  ∀M. ∀sigma. ∀policy. ∀v'.
422  map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
423 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
424  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
425  (status_of_pseudo_status M code_memory s sigma policy) d v'
426  =status_of_pseudo_status M code_memory
427   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
428 #code #s #d #v cases (set_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_
429 #H @H
430qed.
431
432lemma set_low_internal_ram_status_of_pseudo_status:
433 ∀cm,sigma,policy,M,s,ram.
434  set_low_internal_ram (BitVectorTrie Byte 16)
435  (code_memory_of_pseudo_assembly_program cm sigma policy)
436  (status_of_pseudo_status M cm s sigma policy)
437  (low_internal_ram_of_pseudo_low_internal_ram M ram)
438  = status_of_pseudo_status M cm
439    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
440 //
441qed.
442
443(* Real axiom ATM *)
444axiom insert_low_internal_ram_of_pseudo_low_internal_ram:
445 ∀M,sigma,cm,s,addr,v,v'.
446 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
447  insert Byte 7 addr v'
448  (low_internal_ram_of_pseudo_low_internal_ram M
449   (low_internal_ram pseudo_assembly_program cm s))
450  =low_internal_ram_of_pseudo_low_internal_ram M
451   (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
452               
453lemma insert_low_internal_ram_status_of_pseudo_status:
454 ∀M,cm,sigma,policy,s,addr,v,v'.
455 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
456  insert Byte 7 addr v'
457   (low_internal_ram (BitVectorTrie Byte 16)
458    (code_memory_of_pseudo_assembly_program cm sigma policy)
459    (status_of_pseudo_status M cm s sigma policy))
460  = low_internal_ram_of_pseudo_low_internal_ram M
461     (insert Byte 7 addr v
462      (low_internal_ram pseudo_assembly_program cm s)).
463 /2 by insert_low_internal_ram_of_pseudo_low_internal_ram/
464qed.
465
466(* Real axiom ATM *)
467axiom insert_high_internal_ram_of_pseudo_high_internal_ram:
468 ∀M,sigma,cm,s,addr,v,v'.
469 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
470  insert Byte 7 addr v'
471  (high_internal_ram_of_pseudo_high_internal_ram M
472   (high_internal_ram pseudo_assembly_program cm s))
473  =high_internal_ram_of_pseudo_high_internal_ram M
474   (insert Byte 7 addr v (high_internal_ram pseudo_assembly_program cm s)).
475
476lemma insert_high_internal_ram_status_of_pseudo_status:
477 ∀M,cm,sigma,policy,s,addr,v,v'.
478 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
479  insert Byte 7 addr v'
480   (high_internal_ram (BitVectorTrie Byte 16)
481    (code_memory_of_pseudo_assembly_program cm sigma policy)
482    (status_of_pseudo_status M cm s sigma policy))
483  = high_internal_ram_of_pseudo_high_internal_ram M
484     (insert Byte 7 addr v
485      (high_internal_ram pseudo_assembly_program cm s)).
486 /2 by insert_high_internal_ram_of_pseudo_high_internal_ram/
487qed.
488
489lemma bit_address_of_register_status_of_pseudo_status:
490 ∀M,cm,s,sigma,policy,r.
491  bit_address_of_register …
492  (code_memory_of_pseudo_assembly_program cm sigma policy)
493  (status_of_pseudo_status M cm s sigma policy) r =
494  bit_address_of_register … cm s r.
495 #M #cm #s #sigma #policy #r whd in ⊢ (??%%);
496 >get_8051_sfr_status_of_pseudo_status
497 @pair_elim #un #ln #_
498 @pair_elim #r1 #r0 #_ %
499qed.
500
501(*CSC: provable using the axiom in AssemblyProof, but this one seems more
502  primitive *)
503axiom lookup_low_internal_ram_of_pseudo_low_internal_ram:
504 ∀M,sigma,cm,s,addr.
505  lookup Byte 7 addr
506  (low_internal_ram_of_pseudo_low_internal_ram M
507   (low_internal_ram pseudo_assembly_program cm s)) (zero 8)
508  =
509  map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr)
510  (lookup Byte 7 addr
511   (low_internal_ram pseudo_assembly_program cm s) (zero 8)).
512
513(*CSC: provable using the axiom in AssemblyProof, but this one seems more
514  primitive *)
515axiom lookup_high_internal_ram_of_pseudo_high_internal_ram:
516 ∀M,sigma,cm,s,addr.
517  lookup Byte 7 addr
518  (high_internal_ram_of_pseudo_high_internal_ram M
519   (high_internal_ram pseudo_assembly_program cm s)) (zero 8)
520  =
521  map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr)
522  (lookup Byte 7 addr
523   (high_internal_ram pseudo_assembly_program cm s) (zero 8)).
524
525lemma get_register_status_of_pseudo_status:
526 ∀M,cm,sigma,policy,s,r.
527  get_register …
528   (code_memory_of_pseudo_assembly_program cm sigma policy)
529   (status_of_pseudo_status M cm s sigma policy) r =
530  map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r)
531   (get_register … cm s r).
532 #M #cm #sigma #policy #s #r whd in match get_register; normalize nodelta
533 whd in match status_of_pseudo_status; normalize nodelta
534 >bit_address_of_register_status_of_pseudo_status
535 @lookup_low_internal_ram_of_pseudo_low_internal_ram
536qed.
537
538lemma external_ram_status_of_pseudo_status:
539 ∀M,cm,s,sigma,policy.
540  external_ram …
541   (code_memory_of_pseudo_assembly_program cm sigma policy)
542   (status_of_pseudo_status M cm s sigma policy) =
543  external_ram … cm s.
544 //
545qed.
546
547lemma set_external_ram_status_of_pseudo_status:
548  ∀M,cm,ps,sigma,policy,ram.
549    set_external_ram …
550      (code_memory_of_pseudo_assembly_program cm sigma policy)
551      (status_of_pseudo_status M cm ps sigma policy)
552      ram =
553    status_of_pseudo_status M cm (set_external_ram … cm ps ram) sigma policy.
554  //
555qed.
556
557lemma set_register_status_of_pseudo_status:
558 ∀M,cm,s,sigma,policy,r,v,v'.
559  map_internal_ram_address_using_pseudo_address_map M sigma
560   (false:::bit_address_of_register pseudo_assembly_program cm s r) v =v' →
561  set_register (BitVectorTrie Byte 16)
562   (code_memory_of_pseudo_assembly_program cm sigma policy)
563   (status_of_pseudo_status M cm s sigma policy) r v'
564  = status_of_pseudo_status M cm (set_register pseudo_assembly_program cm s r v)
565    sigma policy.
566 #M #cm #s #sigma #policy #r #v #v' #v_ok
567 whd in match set_register; normalize nodelta
568 >bit_address_of_register_status_of_pseudo_status
569 >(insert_low_internal_ram_status_of_pseudo_status … v_ok)
570 @set_low_internal_ram_status_of_pseudo_status
571qed.
572
573definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝
574 λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λsigma. λaddr.
575  match addr with
576  [ INDIRECT i ⇒
577     assoc_list_lookup ??
578      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None …
579  | EXT_INDIRECT e ⇒
580     assoc_list_lookup ??
581      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None …
582  | ACC_DPTR ⇒
583    (* XXX: \snd M = None plus in the very rare case when we are trying to dereference a null (O) pointer
584            in the ACC_A *)
585      map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) =
586        get_8051_sfr … cm s SFR_ACC_A
587  | ACC_PC ⇒
588      (* XXX: as above *)
589      map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) =
590        get_8051_sfr … cm s SFR_ACC_A ∧ sigma (program_counter … s) = program_counter … s
591  | _ ⇒ True ].
592
593definition map_address_mode_using_internal_pseudo_address_map_ok2 ≝
594 λT,M,sigma,cm.λs:PreStatus T cm.λaddr,v.
595  match addr with
596  [ DIRECT d ⇒
597     let 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit … 1 7 d in
598     match head' … bit_one with
599     [ true ⇒
600      map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v
601     | false ⇒
602      map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ]
603  | INDIRECT i ⇒
604     let register ≝ get_register ?? s [[ false; false; i ]] in
605     map_internal_ram_address_using_pseudo_address_map M sigma register v
606  | REGISTER r ⇒
607     map_internal_ram_address_using_pseudo_address_map M sigma
608      (false:::bit_address_of_register … s r) v
609  | ACC_A ⇒
610     map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v
611  | _ ⇒ v ].
612
613definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
614                                   acc_a ; acc_b ; ext_indirect ;
615                                   ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝
616  λm, cm, s, a, v.
617    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
618                                                acc_a ; acc_b ; ext_indirect ;
619                                                ext_indirect_dptr ]] x) →
620                   PreStatus m cm
621            with
622      [ DIRECT d ⇒
623        λdirect: True.
624          let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
625            match head' … bit_one with
626              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
627              | false ⇒
628                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
629                  set_low_internal_ram ?? s memory
630              ]
631      | INDIRECT i ⇒
632        λindirect: True.
633          let register ≝ get_register ?? s [[ false; false; i ]] in
634          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
635            match head' … bit_one with
636              [ false ⇒
637                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
638                  set_low_internal_ram ?? s memory
639              | true ⇒
640                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
641                  set_high_internal_ram ?? s memory
642              ]
643      | REGISTER r ⇒ λregister: True. set_register ?? s r v
644      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
645      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
646      | EXT_INDIRECT e ⇒
647        λext_indirect: True.
648          let address ≝ get_register ?? s [[ false; false; e ]] in
649          let padded_address ≝ pad 8 8 address in
650          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
651            set_external_ram ?? s memory
652      | EXT_INDIRECT_DPTR ⇒
653        λext_indirect_dptr: True.
654          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
655          let memory ≝ insert ? 16 address v (external_ram ?? s) in
656            set_external_ram ?? s memory
657      | _ ⇒
658        λother: False.
659          match other in False with [ ]
660      ] (subaddressing_modein … a).
661
662(*CSC: move elsewhere*)
663lemma eq_head': ∀A,n,v. v = head' A n v ::: tail … v.
664 #A #n #v inversion v in ⊢ ?;
665 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) /2/
666 | #m #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ' >EQ' % ]
667qed.
668
669(*CSC: move elsewhere*)
670lemma tail_singleton: ∀A,v. tail A 0 v = [[]].
671 #A #v inversion v in ⊢ ?;
672 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) #H destruct(H)
673 | #n #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ1 >EQ1 normalize
674   /2 by jmeq_to_eq/
675 ]
676qed.
677
678(*CSC: move elsewhere*)
679lemma eq_cons_head_append:
680 ∀A,n.∀hd: Vector A 1. ∀tl: Vector A n.
681  head' A 0 hd:::tl = hd@@tl.
682 #A #n #hd #tl >(eq_head' … hd) >tail_singleton %
683qed.
684
685lemma set_arg_8_status_of_pseudo_status:
686  ∀cm.
687  ∀ps.
688  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
689  ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'.
690   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
691   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
692    set_arg_8 (BitVectorTrie Byte 16)
693      (code_memory_of_pseudo_assembly_program cm sigma policy)
694      (status_of_pseudo_status M cm ps sigma policy)
695      addr value' =
696    status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
697  whd in match set_arg_8; normalize nodelta
698  @(let m ≝ pseudo_assembly_program in λcm, s. λa: [[ direct ; indirect ; registr ;
699                                   acc_a ; acc_b ; ext_indirect ;
700                                   ext_indirect_dptr ]]. λv.
701    match a return λaddr. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
702                                                acc_a ; acc_b ; ext_indirect ;
703                                                ext_indirect_dptr ]] addr) →
704                   Σp.?
705            with
706      [ DIRECT d ⇒
707        λdirect: True.
708          deplet 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit ? 1 7 d in
709            match head' … bit_one with
710              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
711              | false ⇒
712                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
713                  set_low_internal_ram ?? s memory
714              ]
715      | INDIRECT i ⇒
716        λindirect: True.
717          let register ≝ get_register ?? s [[ false; false; i ]] in
718          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
719            match head' … bit_one with
720              [ false ⇒
721                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
722                  set_low_internal_ram ?? s memory
723              | true ⇒
724                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
725                  set_high_internal_ram ?? s memory
726              ]
727      | REGISTER r ⇒ λregister: True. set_register ?? s r v
728      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
729      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
730      | EXT_INDIRECT e ⇒
731        λext_indirect: True.
732          let address ≝ get_register ?? s [[ false; false; e ]] in
733          let padded_address ≝ pad 8 8 address in
734          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
735            set_external_ram ?? s memory
736      | EXT_INDIRECT_DPTR ⇒
737        λext_indirect_dptr: True.
738          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
739          let memory ≝ insert ? 16 address v (external_ram ?? s) in
740            set_external_ram ?? s memory
741      | _ ⇒
742        λother: False.
743          match other in False with [ ]
744      ] (subaddressing_modein … a)) normalize nodelta
745  #M #sigma #policy #v'
746  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
747  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
748  [1,2:
749    <vsplit_refl normalize nodelta >p normalize nodelta
750    [ >(vsplit_ok … vsplit_refl) #_ @set_bit_addressable_sfr_status_of_pseudo_status
751    | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
752  |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p;
753      >get_register_status_of_pseudo_status
754      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
755      >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
756      [ >(insert_high_internal_ram_status_of_pseudo_status … v)
757      | >(insert_low_internal_ram_status_of_pseudo_status … v) ]
758      // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
759  |5: #EQ1 #EQ2 <EQ2 >get_register_status_of_pseudo_status
760      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
761      >EQ1 normalize nodelta
762      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status
763  |6: #EQ1 #EQ2 <EQ2 /2 by set_register_status_of_pseudo_status/
764  |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/
765  |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
766  |9: #_ #EQ <EQ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status
767      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ]
768qed.
769
770definition get_bit_addressable_sfr:
771    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → bool → Byte ≝
772  λM: Type[0].
773  λcode_memory:M.
774  λs: PreStatus M code_memory.
775  λb: Byte.
776  λl: bool.
777  match sfr_of_Byte b with
778  [ None ⇒ match not_implemented in False with [ ]
779  | Some sfr8051_8052 ⇒
780    match sfr8051_8052 with
781    [ inl sfr ⇒
782      match sfr with
783      [ SFR_P1 ⇒
784        if l then
785          p1_latch … s
786        else
787          get_8051_sfr … s SFR_P1
788      | SFR_P3 ⇒
789        if l then
790          p3_latch … s
791        else
792          get_8051_sfr … s SFR_P3
793      | _ ⇒ get_8051_sfr … s sfr
794      ]
795    | inr sfr ⇒ get_8052_sfr M code_memory s sfr
796    ]
797  ].
798
799definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ;
800                                          acc_a ; acc_b ; data ; acc_dptr ;
801                                          acc_pc ; ext_indirect ;
802                                          ext_indirect_dptr ]] → Byte ≝
803  λm, cm, s, l, a.
804    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
805                                                acc_a ; acc_b ; data ; acc_dptr ;
806                                                acc_pc ; ext_indirect ;
807                                                ext_indirect_dptr ]] x) → ? with
808      [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
809      | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
810      | DATA d ⇒ λdata: True. d
811      | REGISTER r ⇒ λregister: True. get_register ?? s r
812      | EXT_INDIRECT_DPTR ⇒
813        λext_indirect_dptr: True.
814          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
815            lookup ? 16 address (external_ram ?? s) (zero 8)
816      | EXT_INDIRECT e ⇒
817        λext_indirect: True.
818          let address ≝ get_register ?? s [[ false; false; e ]]  in
819          let padded_address ≝ pad 8 8 address in
820            lookup ? 16 padded_address (external_ram ?? s) (zero 8)
821      | ACC_DPTR ⇒
822        λacc_dptr: True.
823          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
824          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
825          let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
826            lookup ? 16 address (external_ram ?? s) (zero 8)
827      | ACC_PC ⇒
828        λacc_pc: True.
829          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
830          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
831            lookup ? 16 address (external_ram ?? s) (zero 8)
832      | DIRECT d ⇒
833        λdirect: True.
834          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
835            match head' … hd with
836            [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
837            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
838            ]
839      | INDIRECT i ⇒
840        λindirect: True.
841          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
842            match head' … hd with
843            [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)
844            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
845            ]
846      | _ ⇒ λother.
847        match other in False with [ ]
848      ] (subaddressing_modein … a).
849
850lemma p1_latch_status_of_pseudo_status:
851    ∀M.
852    ∀code_memory: pseudo_assembly_program.
853    ∀s: PreStatus … code_memory.
854    ∀sigma.
855    ∀policy.
856    (p1_latch (BitVectorTrie Byte 16)
857      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
858      (status_of_pseudo_status M code_memory s sigma policy) =
859    (p1_latch pseudo_assembly_program code_memory s)).
860  //
861qed.
862
863lemma p3_latch_status_of_pseudo_status:
864    ∀M.
865    ∀code_memory: pseudo_assembly_program.
866    ∀s: PreStatus … code_memory.
867    ∀sigma.
868    ∀policy.
869    (p3_latch (BitVectorTrie Byte 16)
870      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
871      (status_of_pseudo_status M code_memory s sigma policy) =
872    (p3_latch pseudo_assembly_program code_memory s)).
873  //
874qed.
875
876lemma get_bit_addressable_sfr_status_of_pseudo_status':
877  let M ≝ pseudo_assembly_program in
878    ∀code_memory: M.
879    ∀s: PreStatus M code_memory.
880    ∀d: Byte.
881    ∀l: bool.
882      Σp: Byte. ∀M. ∀sigma. ∀policy.
883        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
884          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
885          (status_of_pseudo_status M code_memory s sigma policy) d l =
886        map_address_Byte_using_internal_pseudo_address_map M sigma
887         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)).
888  whd in match get_bit_addressable_sfr;
889  whd in match map_address_Byte_using_internal_pseudo_address_map;
890  normalize nodelta
891  @(let M ≝ pseudo_assembly_program in
892    λcode_memory:M.
893    λs: PreStatus M code_memory.
894    λb: Byte.
895    λl: bool.
896    match sfr_of_Byte b with
897    [ None ⇒ match not_implemented in False with [ ]
898    | Some sfr8051_8052 ⇒
899    match sfr8051_8052 with
900    [ inl sfr ⇒
901      match sfr with
902      [ SFR_P1 ⇒
903        if l then
904          p1_latch … s
905        else
906          get_8051_sfr … s SFR_P1
907      | SFR_P3 ⇒
908        if l then
909          p3_latch … s
910        else
911          get_8051_sfr … s SFR_P3
912      | _ ⇒ get_8051_sfr … s sfr
913      ]
914    | inr sfr ⇒ get_8052_sfr M code_memory s sfr
915    ]
916    ])
917  #M #sigma #policy normalize nodelta
918  /by get_8051_sfr_status_of_pseudo_status, p1_latch_status_of_pseudo_status, p3_latch_status_of_pseudo_status/
919qed.
920
921lemma get_bit_addressable_sfr_status_of_pseudo_status:
922  let M ≝ pseudo_assembly_program in
923    ∀code_memory: M.
924    ∀s: PreStatus M code_memory.
925    ∀d: Byte.
926    ∀l: bool.
927    ∀M. ∀sigma. ∀policy.
928        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
929          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
930          (status_of_pseudo_status M code_memory s sigma policy) d l =
931        map_address_Byte_using_internal_pseudo_address_map M sigma
932         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)).
933 #code #s #d #v cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_
934 #H @H
935qed.
936
937lemma program_counter_status_of_pseudo_status:
938    ∀code_memory: pseudo_assembly_program.
939    ∀s: PreStatus ? code_memory.
940    ∀M. ∀sigma. ∀policy.
941      program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy)
942          (status_of_pseudo_status M code_memory s sigma policy) =
943        sigma (program_counter … s).
944  //
945qed.
946
947lemma get_cy_flag_status_of_pseudo_status:
948  ∀M, cm, sigma, policy, s.
949  (get_cy_flag (BitVectorTrie Byte 16)
950    (code_memory_of_pseudo_assembly_program cm sigma policy)
951    (status_of_pseudo_status M cm s sigma policy) =
952  get_cy_flag pseudo_assembly_program cm s).
953  #M #cm #sigma #policy #s
954  whd in match get_cy_flag; normalize nodelta
955  >get_index_v_status_of_pseudo_status %
956qed.
957
958lemma get_arg_8_status_of_pseudo_status:
959  ∀cm.
960  ∀ps.
961  ∀l.
962  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
963    Σp: Byte. ∀M. ∀sigma. ∀policy.
964      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
965      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
966      (status_of_pseudo_status M cm ps sigma policy) l addr =
967      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr).
968  whd in match get_arg_8; normalize nodelta
969  @(let m ≝ pseudo_assembly_program in
970    λcm: m. λs: PreStatus m cm. λl: bool. λa: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; acc_pc; ext_indirect; ext_indirect_dptr]].
971    match a return λx. bool_to_Prop (is_in ? [[ direct; indirect; registr; acc_a; acc_b; data; acc_dptr; acc_pc; ext_indirect; ext_indirect_dptr ]] x) → Σp. ? with
972      [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
973      | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
974      | DATA d ⇒ λdata: True. d
975      | REGISTER r ⇒ λregister: True. get_register ?? s r
976      | EXT_INDIRECT_DPTR ⇒
977        λext_indirect_dptr: True.
978          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
979            lookup ? 16 address (external_ram ?? s) (zero 8)
980      | EXT_INDIRECT e ⇒
981        λext_indirect: True.
982          let address ≝ get_register ?? s [[ false; false; e ]]  in
983          let padded_address ≝ pad 8 8 address in
984            lookup ? 16 padded_address (external_ram ?? s) (zero 8)
985      | ACC_DPTR ⇒
986        λacc_dptr: True.
987          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
988          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
989          let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
990            lookup ? 16 address (external_ram ?? s) (zero 8)
991      | ACC_PC ⇒
992        λacc_pc: True.
993          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
994          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
995            lookup ? 16 address (external_ram ?? s) (zero 8)
996      | DIRECT d ⇒
997        λdirect: True.
998          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
999            match head' … hd with
1000            [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
1001            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
1002            ]
1003      | INDIRECT i ⇒
1004        λindirect: True.
1005          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
1006            match head' … hd with
1007            [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)
1008            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
1009            ]
1010      | _ ⇒ λother: False.
1011        match other in False with [ ]
1012      ] (subaddressing_modein … a)) normalize nodelta
1013  #M #sigma #policy
1014  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
1015  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
1016  [1:
1017    #_ >p normalize nodelta >p1 normalize nodelta
1018    @get_bit_addressable_sfr_status_of_pseudo_status
1019  |2:
1020    #_>p normalize nodelta >p1 normalize nodelta
1021    @lookup_low_internal_ram_of_pseudo_low_internal_ram
1022  |3,4:
1023    #assoc_list_assm >get_register_status_of_pseudo_status
1024    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
1025    >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta
1026    [1:
1027      >(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma)
1028    |2:
1029      >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
1030    ]
1031    @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
1032  |5:
1033    #assoc_list_assm >get_register_status_of_pseudo_status
1034    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
1035    >assoc_list_assm normalize nodelta %
1036  |6,7,8,9:
1037    #_ /2/
1038  |10:
1039    #acc_a_assm >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status
1040    >get_8051_sfr_status_of_pseudo_status
1041    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
1042    >acc_a_assm >p normalize nodelta //
1043  |11:
1044    * #map_acc_a_assm #sigma_assm >get_8051_sfr_status_of_pseudo_status >program_counter_status_of_pseudo_status
1045    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
1046    >sigma_assm >map_acc_a_assm >p normalize nodelta //
1047  |12:
1048    #_ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status
1049    >external_ram_status_of_pseudo_status //
1050  ]
1051qed.
1052
1053lemma get_arg_16_status_of_pseudo_status:
1054  ∀cm.
1055  ∀ps.
1056  ∀addr: [[data16]].
1057  ∀M. ∀sigma. ∀policy.
1058      get_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1059      (status_of_pseudo_status M cm ps sigma policy) addr =
1060      (get_arg_16 … cm ps addr).
1061  //
1062qed.
1063
1064lemma set_arg_16_status_of_pseudo_status:
1065  ∀cm.
1066  ∀ps.
1067  ∀addr: [[dptr]].
1068  ∀v: Word.
1069  ∀M. ∀sigma. ∀policy.
1070      set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1071      (status_of_pseudo_status M cm ps sigma policy) v addr =
1072      status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy.
1073  #cm #ps #addr #v #M #sigma #policy
1074  @(subaddressing_mode_elim … addr)
1075  whd in match set_arg_16; normalize nodelta
1076  whd in match set_arg_16'; normalize nodelta
1077  @(vsplit_elim bool ???) #bu #bl #bu_bl_refl normalize nodelta
1078  >(set_8051_sfr_status_of_pseudo_status … bu)
1079  [1: >(set_8051_sfr_status_of_pseudo_status … bl) ]
1080  //
1081qed.
1082
1083definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] →
1084                       bool → bool ≝
1085  λm, cm, s, a, l.
1086    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
1087                                                 n_bit_addr ;
1088                                                 carry ]] x) → ? with
1089      [ BIT_ADDR b ⇒
1090        λbit_addr: True.
1091        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1092        match head' … bit_1 with
1093        [ true ⇒
1094          let address ≝ nat_of_bitvector … seven_bits in
1095          let d ≝ address ÷ 8 in
1096          let m ≝ address mod 8 in
1097          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1098          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
1099            get_index_v … sfr m ?
1100        | false ⇒
1101          let address ≝ nat_of_bitvector … seven_bits in
1102          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1103          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1104            get_index_v … t (modulus address 8) ?
1105        ]
1106      | N_BIT_ADDR n ⇒
1107        λn_bit_addr: True.
1108        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
1109        match head' … bit_1 with
1110        [ true ⇒
1111          let address ≝ nat_of_bitvector … seven_bits in
1112          let d ≝ address ÷ 8 in
1113          let m ≝ address mod 8 in
1114          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1115          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
1116            ¬(get_index_v … sfr m ?)
1117        | false ⇒
1118          let address ≝ nat_of_bitvector … seven_bits in
1119          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1120          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1121            ¬(get_index_v … t (modulus address 8) ?)
1122        ]
1123      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
1124      | _ ⇒ λother.
1125        match other in False with [ ]
1126      ] (subaddressing_modein … a).
1127      @modulus_less_than
1128qed.
1129
1130definition map_bit_address_mode_using_internal_pseudo_address_map_get ≝
1131 λM:internal_pseudo_address_map.λcm: pseudo_assembly_program.λs:PreStatus ? cm.λsigma: Word → Word. λaddr. λl.
1132  match addr with
1133  [ BIT_ADDR b ⇒
1134    let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1135    match head' … bit_1 with
1136    [ true ⇒
1137      let address ≝ nat_of_bitvector … seven_bits in
1138      let d ≝ address ÷ 8 in
1139      let m ≝ address mod 8 in
1140      let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1141        map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l
1142    | false ⇒
1143      let address ≝ nat_of_bitvector … seven_bits in
1144      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1145      let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1146        map_internal_ram_address_using_pseudo_address_map M sigma
1147          (false:::address') t = t
1148    ]
1149  | N_BIT_ADDR b ⇒
1150    let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1151    match head' … bit_1 with
1152    [ true ⇒
1153      let address ≝ nat_of_bitvector … seven_bits in
1154      let d ≝ address ÷ 8 in
1155      let m ≝ address mod 8 in
1156      let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1157        map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l
1158    | false ⇒
1159      let address ≝ nat_of_bitvector … seven_bits in
1160      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1161      let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1162        map_internal_ram_address_using_pseudo_address_map M sigma
1163          (false:::address') t = t
1164    ]
1165  | _ ⇒ True ].
1166
1167lemma get_arg_1_status_of_pseudo_status':
1168  ∀cm.
1169  ∀ps.
1170  ∀addr: [[bit_addr; n_bit_addr; carry]].
1171  ∀l.
1172    Σb: bool. ∀M. ∀sigma. ∀policy.
1173      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
1174      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1175      (status_of_pseudo_status M cm ps sigma policy) addr l =
1176      (get_arg_1 … cm ps addr l).
1177  whd in match get_arg_1; normalize nodelta
1178  @(let m ≝ pseudo_assembly_program in
1179    λcm: m. λs: PseudoStatus cm. λa:[[bit_addr; n_bit_addr; carry]]. λl.
1180    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
1181                                                 n_bit_addr ;
1182                                                 carry ]] x) → Σb: bool. ? with
1183      [ BIT_ADDR b ⇒
1184        λbit_addr: True.
1185        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1186        match head' … bit_1 with
1187        [ true ⇒
1188          let address ≝ nat_of_bitvector … seven_bits in
1189          let d ≝ address ÷ 8 in
1190          let m ≝ address mod 8 in
1191          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1192          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
1193            get_index_v … sfr m ?
1194        | false ⇒
1195          let address ≝ nat_of_bitvector … seven_bits in
1196          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1197          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1198            get_index_v … t (modulus address 8) ?
1199        ]
1200      | N_BIT_ADDR n ⇒
1201        λn_bit_addr: True.
1202        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
1203        match head' … bit_1 with
1204        [ true ⇒
1205          let address ≝ nat_of_bitvector … seven_bits in
1206          let d ≝ address ÷ 8 in
1207          let m ≝ address mod 8 in
1208          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1209          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
1210            ¬(get_index_v … sfr m ?)
1211        | false ⇒
1212          let address ≝ nat_of_bitvector … seven_bits in
1213          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1214          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1215            ¬(get_index_v … t (modulus address 8) ?)
1216        ]
1217      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
1218      | _ ⇒ λother.
1219        match other in False with [ ]
1220      ] (subaddressing_modein … a)) normalize nodelta
1221  try @modulus_less_than
1222  #M #sigma #policy
1223  [1:
1224    #_ @get_cy_flag_status_of_pseudo_status
1225  |2,4:
1226    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
1227    >get_bit_addressable_sfr_status_of_pseudo_status #map_address_assm
1228    >map_address_assm %
1229  |3,5:
1230    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
1231    whd in match status_of_pseudo_status; normalize nodelta
1232    >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
1233    #map_address_assm >map_address_assm %
1234  ]
1235qed.
1236
1237lemma get_arg_1_status_of_pseudo_status:
1238  ∀cm.
1239  ∀ps.
1240  ∀addr: [[bit_addr; n_bit_addr; carry]].
1241  ∀l.
1242  ∀M. ∀sigma. ∀policy.
1243      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
1244      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1245      (status_of_pseudo_status M cm ps sigma policy) addr l =
1246      (get_arg_1 … cm ps addr l).
1247  #cm #ps #addr #l
1248  cases (get_arg_1_status_of_pseudo_status' cm ps addr l) #_ #assm
1249  @assm
1250qed.
1251
1252definition set_arg_1': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → Σs':PreStatus M code_memory. clock ? code_memory s = clock ? code_memory s' ≝
1253  λm: Type[0].
1254  λcm.
1255  λs: PreStatus m cm.
1256  λa: [[bit_addr; carry]].
1257  λv: Bit.
1258    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with
1259      [ BIT_ADDR b ⇒ λbit_addr: True.
1260        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1261        match head' … bit_1 with
1262        [ true ⇒
1263          let address ≝ nat_of_bitvector … seven_bits in
1264          let d ≝ address ÷ 8 in
1265          let m ≝ address mod 8 in
1266          let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1267          let sfr ≝ get_bit_addressable_sfr … s t true in
1268          let new_sfr ≝ set_index … sfr m v ? in
1269            set_bit_addressable_sfr … s new_sfr t
1270        | false ⇒
1271          let address ≝ nat_of_bitvector … seven_bits in
1272          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1273          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1274          let n_bit ≝ set_index … t (modulus address 8) v ? in
1275          let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
1276            set_low_internal_ram … s memory
1277        ]
1278      | CARRY ⇒
1279        λcarry: True.
1280        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1281        let new_psw ≝ v:::seven_bits in
1282          set_8051_sfr ?? s SFR_PSW new_psw
1283      | _ ⇒
1284        λother: False.
1285          match other in False with
1286            [ ]
1287      ] (subaddressing_modein … a).
1288  try (repeat @le_S_S @le_O_n)
1289  try @modulus_less_than
1290  /by/
1291  cases daemon (* XXX: russell type for preservation of clock on set_bit_addressable_sfr *)
1292qed.
1293
1294definition set_arg_1:
1295    ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] →
1296      Bit → PreStatus M code_memory ≝ set_arg_1'.
1297
1298definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝
1299  λM: internal_pseudo_address_map.
1300  λcm: pseudo_assembly_program.
1301  λs: PreStatus ? cm.
1302  λsigma: Word → Word.
1303  λaddr: [[bit_addr; carry]].
1304  λv: Bit.
1305  match addr with
1306  [ BIT_ADDR b ⇒
1307    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1308    match head' … bit_1 with
1309    [ true ⇒
1310      let address ≝ nat_of_bitvector … seven_bits in
1311      let d ≝ address ÷ 8 in
1312      let m ≝ address mod 8 in
1313      let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1314      let sfr ≝ get_bit_addressable_sfr … s t true in
1315        map_address_Byte_using_internal_pseudo_address_map M sigma t sfr = sfr
1316    | false ⇒
1317      let address ≝ nat_of_bitvector … seven_bits in
1318      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1319      let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1320        map_internal_ram_address_using_pseudo_address_map M sigma
1321          (false:::address') t = t
1322    ]   
1323  | CARRY ⇒ True
1324  | _ ⇒ True
1325  ].
1326
1327definition map_bit_address_mode_using_internal_pseudo_address_map_set_2 ≝
1328  λM: internal_pseudo_address_map.
1329  λcm: pseudo_assembly_program.
1330  λs: PreStatus ? cm.
1331  λsigma: Word → Word.
1332  λaddr: [[bit_addr; carry]].
1333  λv: Bit.
1334  match addr with
1335  [ BIT_ADDR b ⇒
1336    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1337    match head' … bit_1 with
1338    [ true ⇒
1339      let address ≝ nat_of_bitvector … seven_bits in
1340      let d ≝ address ÷ 8 in
1341      let m ≝ address mod 8 in
1342      let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1343      let sfr ≝ get_bit_addressable_sfr … s t true in
1344      let new_sfr ≝ set_index … sfr m v ? in
1345        map_address_Byte_using_internal_pseudo_address_map M sigma new_sfr t = t
1346    | false ⇒
1347      let address ≝ nat_of_bitvector … seven_bits in
1348      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1349      let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1350      let n_bit ≝ set_index … t (modulus address 8) v ? in
1351      let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
1352        map_internal_ram_address_using_pseudo_address_map M sigma
1353          (false:::address') n_bit = n_bit
1354    ]   
1355  | CARRY ⇒ True
1356  | _ ⇒ True
1357  ].
1358  @modulus_less_than
1359qed.
1360
1361lemma set_arg_1_status_of_pseudo_status:
1362  ∀cm: pseudo_assembly_program.
1363  ∀ps: PreStatus pseudo_assembly_program cm.
1364  ∀addr: [[bit_addr; carry]].
1365  ∀b: Bit.
1366    Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy.
1367      map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
1368      map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b →
1369        set_arg_1 (BitVectorTrie Byte 16)
1370          (code_memory_of_pseudo_assembly_program cm sigma policy)
1371          (status_of_pseudo_status M cm ps sigma policy) addr b =
1372        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b) sigma policy.
1373  whd in match set_arg_1; normalize nodelta
1374  whd in match set_arg_1'; normalize nodelta
1375  whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_1; normalize nodelta
1376  whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_2; normalize nodelta
1377  @(let m ≝ pseudo_assembly_program in
1378    λcm.
1379    λs: PreStatus m cm.
1380    λa: [[bit_addr; carry]].
1381    λv: Bit.
1382    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σp. ? with
1383      [ BIT_ADDR b ⇒ λbit_addr: True.
1384        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1385        match head' … bit_1 with
1386        [ true ⇒
1387          let address ≝ nat_of_bitvector … seven_bits in
1388          let d ≝ address ÷ 8 in
1389          let m ≝ address mod 8 in
1390          let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1391          let sfr ≝ get_bit_addressable_sfr … s t true in
1392          let new_sfr ≝ set_index … sfr m v ? in
1393            set_bit_addressable_sfr … s new_sfr t
1394        | false ⇒
1395          let address ≝ nat_of_bitvector … seven_bits in
1396          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1397          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1398          let n_bit ≝ set_index … t (modulus address 8) v ? in
1399          let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
1400            set_low_internal_ram … s memory
1401        ]
1402      | CARRY ⇒
1403        λcarry: True.
1404        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1405        let new_psw ≝ v:::seven_bits in
1406          set_8051_sfr ?? s SFR_PSW new_psw
1407      | _ ⇒
1408        λother: False.
1409          match other in False with
1410            [ ]
1411      ] (subaddressing_modein … a)) normalize nodelta
1412  try @modulus_less_than #M #sigma #policy
1413  [1:
1414    #_ #_ >get_8051_sfr_status_of_pseudo_status
1415    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
1416    >p normalize nodelta @set_8051_sfr_status_of_pseudo_status %
1417  |2,3:
1418    >get_8051_sfr_status_of_pseudo_status
1419    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
1420    >p normalize nodelta >p1 normalize nodelta
1421    #map_bit_address_assm_1 #map_bit_address_assm_2
1422    [1:
1423      >get_bit_addressable_sfr_status_of_pseudo_status
1424      >map_bit_address_assm_1
1425      >(set_bit_addressable_sfr_status_of_pseudo_status cm s … map_bit_address_assm_2) %
1426    |2:
1427      whd in match status_of_pseudo_status in ⊢ (??(????%)?); normalize nodelta
1428      >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
1429      >map_bit_address_assm_1
1430      >(insert_low_internal_ram_of_pseudo_low_internal_ram … map_bit_address_assm_2)
1431      >set_low_internal_ram_status_of_pseudo_status in ⊢ (??%?); %
1432    ]
1433  ]
1434qed.
Note: See TracBrowser for help on using the repository browser.