source: src/ASM/Test.ma @ 2172

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

Moved new versions of get_ / set_arg_* into Status.ma. Commented out proofs that are no longer working.

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