source: src/ASM/Test.ma @ 2276

Last change on this file since 2276 was 2276, checked in by sacerdot, 7 years ago

...

File size: 81.1 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 let_pair_in_status_of_pseudo_status:
8  ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
9    c' = c →
10    (∀left, right.
11      s' left right c' = status_of_pseudo_status M cm (s left right c') sigma policy) →
12    (let 〈left, right〉 ≝ c' in s' left right c') =
13    status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy.
14  #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta //
15qed.
16
17lemma let_pair_as_in_status_of_pseudo_status:
18  ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
19    c' = c →
20    (∀left, right, H, H'. s' left right H' c' = status_of_pseudo_status M cm (s left right H c) sigma policy) →
21    (let 〈left, right〉 as H' ≝ c' in s' left right H' c') =
22    status_of_pseudo_status M cm (let 〈left, right〉 as H ≝ c in s left right H c) sigma policy.
23  #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta #destruct_refl
24  destruct(destruct_refl) /2/
25qed.
26
27lemma if_then_else_status_of_pseudo_status:
28  ∀M: internal_pseudo_address_map.
29  ∀cm: pseudo_assembly_program.
30  ∀sigma: Word → Word.
31  ∀policy: Word → bool.
32  ∀s, s', s'', s'''.
33  ∀t, t': bool.
34    t = t' →
35    s' = status_of_pseudo_status M cm s sigma policy →
36    s''' = status_of_pseudo_status M cm s'' sigma policy →
37      if t then
38        s'
39      else
40        s''' =
41      status_of_pseudo_status M cm (if t' then s else s'') sigma policy.
42  #M #cm #sigma #policy #s #s' #s'' #s''' #t #t' #t_refl #s_refl
43  >t_refl normalize nodelta >s_refl cases t' normalize nodelta //
44qed.
45
46lemma set_program_counter_status_of_pseudo_status:
47  ∀M.
48  ∀cm.
49  ∀sigma.
50  ∀policy.
51  ∀s, s'.
52  ∀new_ppc, new_ppc'.
53    sigma new_ppc = new_ppc' →
54    s' = status_of_pseudo_status M cm s sigma policy →
55    set_program_counter (BitVectorTrie Byte 16)
56      (code_memory_of_pseudo_assembly_program cm sigma policy)
57      s' new_ppc' =
58    status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy.
59  #M #cm #sigma #policy #s #s' #new_ppc #new_ppc'
60  #new_ppc_refl #s_refl <new_ppc_refl >s_refl //
61qed.
62
63lemma set_p1_latch_status_of_pseudo_status:
64  ∀M.
65  ∀code_memory.
66  ∀sigma.
67  ∀policy.
68  ∀s,s'.
69  ∀v.
70   s' = status_of_pseudo_status M code_memory s sigma policy →
71    set_p1_latch (BitVectorTrie Byte 16)
72      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
73      s' v =
74    status_of_pseudo_status M code_memory
75      (set_p1_latch pseudo_assembly_program code_memory s v) sigma policy.
76  #M #cm #sigma #policy #s #s' #new_ppc #s_refl >s_refl //
77qed.
78
79lemma set_p3_latch_status_of_pseudo_status:
80  ∀M.
81  ∀code_memory.
82  ∀sigma.
83  ∀policy.
84  ∀s, s'.
85  ∀v.
86  s' = status_of_pseudo_status M code_memory s sigma policy →
87    set_p3_latch (BitVectorTrie Byte 16)
88      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
89      s' v =
90    status_of_pseudo_status M code_memory
91      (set_p3_latch pseudo_assembly_program code_memory s v) sigma policy.
92  #M #code_memory #sigma #policy #s #s' #v #s_refl >s_refl //
93qed.
94
95definition map_address_using_internal_pseudo_address_map:
96    ∀M: internal_pseudo_address_map. (Word → Word) → SFR8051 → Byte → Byte ≝
97  λM, sigma, sfr, v.
98  match sfr with
99  [ SFR_ACC_A ⇒ map_acc_a_using_internal_pseudo_address_map M sigma v
100  | _         ⇒ v
101  ].
102
103lemma set_index_set_index_overwrite:
104  ∀A: Type[0].
105  ∀n: nat.
106  ∀v: Vector A n.
107  ∀index: nat.
108  ∀e, e': A.
109  ∀proof.
110  ∀proof'.
111    set_index A n v index e proof =
112      set_index A n (set_index A n v index e' proof') index e proof.
113  #A #n #v elim v normalize
114  [1:
115    #index #e #e' #absurd cases (lt_to_not_zero … absurd)
116  |2:
117    #n' #hd #tl #inductive_hypothesis #index #e #e' cases index #proof #proof'
118    normalize //
119  ]
120qed.
121
122lemma set_index_set_index_commutation:
123  ∀A: Type[0].
124  ∀n: nat.
125  ∀v: Vector A n.
126  ∀m, o: nat.
127  ∀m_lt_proof: m < n.
128  ∀o_lt_proof: o < n.
129  ∀e, f: A.
130    m ≠ o →
131      set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof =
132        set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof.
133  #A #n #v elim v
134  [1:
135    #m #o #m_lt_proof
136    normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof)
137  |2:
138    #n' #hd #tl #inductive_hypothesis
139    #m #o
140    cases m cases o
141    [1:
142      #m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant
143      @relevant %
144    |2,3:
145      #o' normalize //
146    |4:
147      #m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm
148      normalize @eq_f @inductive_hypothesis @nmk #relevant
149      >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) %
150    ]
151  ]
152qed.
153
154(* XXX: move elsewhere *)
155lemma get_index_v_set_index_miss:
156  ∀a: Type[0].
157  ∀n: nat.
158  ∀v: Vector a n.
159  ∀i, j: nat.
160  ∀e: a.
161  ∀i_proof: i < n.
162  ∀j_proof: j < n.
163    i ≠ j →
164      get_index_v a n (set_index a n v i e i_proof) j j_proof =
165        get_index_v a n v j j_proof.
166  #a #n #v elim v
167  [1:
168    #i #j #e #i_proof
169    cases (lt_to_not_zero … i_proof)
170  |2:
171    #n' #hd #tl #inductive_hypothesis #i #j
172    cases i cases j
173    [1:
174      #e #i_proof #j_proof #neq_assm
175      cases (absurd ? (refl … 0) neq_assm)
176    |2,3:
177      #i' #e #i_proof #j_proof #_ %
178    |4:
179      #i' #j' #e #i_proof #j_proof #neq_assm
180      @inductive_hypothesis @nmk #eq_assm
181      >eq_assm in neq_assm; #neq_assm
182      cases (absurd ? (refl ??) neq_assm)
183    ]
184  ]
185qed.
186
187lemma get_index_v_set_index_hit:
188  ∀A: Type[0].
189  ∀n: nat.
190  ∀v: Vector A n.
191  ∀i: nat.
192  ∀e: A.
193  ∀i_lt_n_proof: i < n.
194  ∀i_lt_n_proof': i < n.
195    get_index_v A n (set_index A n v i e i_lt_n_proof) i i_lt_n_proof' = e.
196  #A #n #v elim v
197  [1:
198    #i #e #i_lt_n_proof
199    cases (lt_to_not_zero … i_lt_n_proof)
200  |2:
201    #n' #hd #tl #inductive_hypothesis #i #e
202    cases i
203    [1:
204      #i_lt_n_proof #i_lt_n_proof' %
205    |2:
206      #i' #i_lt_n_proof' #i_lt_n_proof''
207      whd in ⊢ (??%?); @inductive_hypothesis
208    ]
209  ]
210qed.
211
212lemma set_index_status_of_pseudo_status:
213  ∀M, code_memory, sigma, policy, s, sfr, v, v'.
214    map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
215(set_index Byte 19
216  (special_function_registers_8051 (BitVectorTrie Byte 16)
217   (code_memory_of_pseudo_assembly_program code_memory sigma policy)
218   (status_of_pseudo_status M code_memory s sigma policy))
219  (sfr_8051_index sfr) v' (sfr8051_index_19 sfr)
220  =sfr_8051_of_pseudo_sfr_8051 M
221   (special_function_registers_8051 pseudo_assembly_program code_memory
222    (set_8051_sfr pseudo_assembly_program code_memory s sfr v)) sigma).
223  #M #code_memory #sigma #policy #s #sfr #v #v' #sfr_neq_acc_a_assm
224  whd in match status_of_pseudo_status; normalize nodelta
225  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
226  inversion (\snd M) try ( * #upper_lower #address) #sndM_refl normalize nodelta
227  [1:
228    <sfr_neq_acc_a_assm cases sfr
229    [18:
230      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
231      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
232      >sndM_refl %
233    ]
234    %
235  |2:
236    inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
237    @pair_elim #high #low #high_low_refl normalize nodelta
238    whd in match set_8051_sfr; normalize nodelta
239    <sfr_neq_acc_a_assm
240    cases sfr in high_low_refl sfr_neq_acc_a_assm;
241    [18,37:
242      @pair_elim #high' #low' #high_low_refl'
243      #high_low_refl
244      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
245      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
246      >sndM_refl normalize nodelta whd in match map_value_using_opt_address_entry; normalize nodelta
247      >eq_upper_lower_refl normalize nodelta
248      [1:
249        #relevant >relevant
250        <set_index_set_index_overwrite in ⊢ (??%?);
251        <set_index_set_index_overwrite in ⊢ (???%);
252        >get_index_v_set_index_hit in high_low_refl';
253        #assm >assm in relevant; normalize nodelta * %
254      |2:
255        #relevant >relevant
256        <set_index_set_index_overwrite in ⊢ (??%?);
257        <set_index_set_index_overwrite in ⊢ (???%);
258        >get_index_v_set_index_hit in high_low_refl';
259        #assm >assm in relevant; normalize nodelta * %
260      ]
261    ]
262    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
263    #relevant * >get_index_v_set_index_miss
264    try (% #absurd normalize in absurd; destruct(absurd))
265    >relevant normalize nodelta
266    @set_index_set_index_commutation % #absurd normalize in absurd; destruct(absurd)
267  ]
268qed.
269
270lemma get_index_v_status_of_pseudo_status:
271  ∀M, code_memory, sigma, policy, s, s', sfr.
272    map_address_using_internal_pseudo_address_map M sigma sfr
273      (get_index_v Byte 19
274        (special_function_registers_8051 pseudo_assembly_program code_memory s)
275        (sfr_8051_index sfr) (sfr8051_index_19 sfr)) = s' →
276    get_index_v Byte 19
277      (special_function_registers_8051 (BitVectorTrie Byte 16)
278      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
279      (status_of_pseudo_status M code_memory s sigma policy))
280      (sfr_8051_index sfr) (sfr8051_index_19 sfr) = s'.
281  #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl
282  whd in match status_of_pseudo_status; normalize nodelta
283  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
284  inversion (\snd M) try ( * #upper_lower #address) #sndM_refl normalize nodelta
285 [1:
286    cases sfr
287    [18:
288      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
289      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
290      >sndM_refl %
291    ]
292    %
293  |2:
294   inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
295    @pair_elim #high #low #high_low_refl normalize nodelta
296    cases sfr
297    [18,37:
298      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
299      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
300      whd in match map_value_using_opt_address_entry; normalize nodelta
301      >sndM_refl normalize nodelta >high_low_refl normalize nodelta
302      >eq_upper_lower_refl normalize nodelta
303      whd in match (set_8051_sfr ?????); //
304    ]
305    @get_index_v_set_index_miss whd in ⊢ (?(??%%));
306    @nmk #absurd destruct(absurd)
307  ]
308qed.
309
310lemma set_8051_sfr_status_of_pseudo_status:
311  ∀M, code_memory, sigma, policy, s, s', sfr, v,v'.
312    s' = status_of_pseudo_status M code_memory s sigma policy →
313    map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
314      set_8051_sfr ? (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v' =
315      status_of_pseudo_status M code_memory
316        (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy.
317  #M #code_memory #sigma #policy #s #s' #sfr #v #v' #s_ok #v_ok
318  >s_ok whd in ⊢ (??%%); @split_eq_status try % /2 by set_index_status_of_pseudo_status/
319qed.
320
321(*lemma get_8051_sfr_status_of_pseudo_status:
322  ∀M.
323  ∀cm, ps, sigma, policy.
324  ∀sfr.
325    (sfr = SFR_ACC_A → \snd M = None …) →
326    get_8051_sfr (BitVectorTrie Byte 16)
327      (code_memory_of_pseudo_assembly_program cm sigma policy)
328      (status_of_pseudo_status M cm ps sigma policy) sfr =
329    get_8051_sfr pseudo_assembly_program cm ps sfr.
330  #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant
331  [18: >relevant % ]
332  cases sndM try % * #address
333  whd in match get_8051_sfr;
334  whd in match status_of_pseudo_status; normalize nodelta
335  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta #address
336  cases (eq_upper_lower ??) normalize nodelta
337  @pair_elim #upper #lower #upper_lower_refl
338  @get_index_v_set_index_miss @nmk #relevant
339  normalize in relevant; destruct(relevant)
340qed.*)
341
342lemma get_8051_sfr_status_of_pseudo_status:
343  ∀M, code_memory, sigma, policy, s, s', s'', sfr.
344    s' = status_of_pseudo_status M code_memory s sigma policy →
345    map_address_using_internal_pseudo_address_map M sigma sfr
346     (get_8051_sfr pseudo_assembly_program code_memory s sfr) = s'' →
347  get_8051_sfr (BitVectorTrie Byte 16)
348    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
349     s' sfr = s''.
350  #M #code_memory #sigma #policy #s #s' #s'' #sfr #s_refl #s_refl' >s_refl <s_refl'
351  whd in match get_8051_sfr; normalize nodelta
352  @get_index_v_status_of_pseudo_status %
353qed.
354
355lemma get_8052_sfr_status_of_pseudo_status:
356  ∀M, code_memory, sigma, policy, s, s', sfr.
357  s' = status_of_pseudo_status M code_memory s sigma policy →
358  (get_8052_sfr (BitVectorTrie Byte 16)
359    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
360    s' sfr =
361   (get_8052_sfr pseudo_assembly_program code_memory s sfr)).
362  #M #code_memory #sigma #policy #s #s' #sfr #s_refl >s_refl //
363qed.
364
365lemma set_8052_sfr_status_of_pseudo_status:
366  ∀M, code_memory, sigma, policy, s, s', sfr, v.
367  s' = status_of_pseudo_status M code_memory s sigma policy →
368    (set_8052_sfr (BitVectorTrie Byte 16)
369      (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v =
370    status_of_pseudo_status M code_memory
371     (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
372  #M #code_memory #sigma #policy #s #s' #sfr #v #s_refl >s_refl //
373qed.
374 
375definition map_address_Byte_using_internal_pseudo_address_map ≝
376 λM,sigma,d,v.
377  match sfr_of_Byte d with
378  [ None ⇒ v
379  | Some sfr8051_8052 ⇒
380    match sfr8051_8052 with
381    [ inl sfr ⇒
382      map_address_using_internal_pseudo_address_map M sigma sfr v
383    | inr _ ⇒ v
384    ]
385  ].
386
387lemma set_bit_addressable_sfr_status_of_pseudo_status':
388  let M ≝ pseudo_assembly_program in
389    ∀code_memory: M.
390    ∀s: PreStatus M code_memory.
391    ∀d: Byte.
392    ∀v: Byte.
393      Σp: PreStatus M code_memory.
394        ∀M.
395        ∀sigma.
396        ∀policy.
397        ∀s'.
398        ∀v'.
399          s' = status_of_pseudo_status M code_memory s sigma policy →
400            map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
401              (set_bit_addressable_sfr (BitVectorTrie Byte 16)
402                (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' d v' =
403              status_of_pseudo_status M code_memory
404                (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
405  whd in match map_address_Byte_using_internal_pseudo_address_map;
406  whd in match set_bit_addressable_sfr;
407  normalize nodelta
408  @(let M ≝ pseudo_assembly_program in
409  λcode_memory:M.
410  λs: PreStatus M code_memory.
411  λb: Byte.
412  λv: Byte.
413   match sfr_of_Byte b with
414   [ None ⇒ match not_implemented in False with [ ]
415   | Some sfr8051_8052 ⇒
416      match sfr8051_8052 with
417      [ inl sfr ⇒
418         match sfr with
419         [ SFR_P1 ⇒
420           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
421           set_p1_latch ?? s v
422         | SFR_P3 ⇒
423           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
424           set_p3_latch ?? s v
425         | _ ⇒ set_8051_sfr ?? s sfr v ]
426      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]])
427  normalize nodelta #M #sigma #policy #s' #v' #s_refl >s_refl
428  /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/
429  whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
430  #v_refl >v_refl //
431qed.
432
433lemma set_bit_addressable_sfr_status_of_pseudo_status:
434 ∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte.
435  ∀M. ∀sigma. ∀policy. ∀s': Status ?. ∀v'.
436  s' = status_of_pseudo_status M code_memory s sigma policy →
437  map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
438 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
439  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
440  s' d v'
441  =status_of_pseudo_status M code_memory
442   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
443 #code #s #d #v cases (set_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_
444 #H @H
445qed.
446
447lemma set_low_internal_ram_status_of_pseudo_status:
448 ∀cm,sigma,policy,M,s,s',ram.
449  s' = status_of_pseudo_status M cm s sigma policy →
450  set_low_internal_ram (BitVectorTrie Byte 16)
451  (code_memory_of_pseudo_assembly_program cm sigma policy)
452  s'
453  (low_internal_ram_of_pseudo_low_internal_ram M sigma ram)
454  = status_of_pseudo_status M cm
455    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
456  #cm #sigma #policy #M #s #s' #ram #s_refl >s_refl //
457qed.
458
459(* Real axiom ATM *)
460axiom insert_low_internal_ram_of_pseudo_low_internal_ram:
461 ∀M,sigma,cm,s,addr,v,v'.
462 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
463  insert Byte 7 addr v'
464  (low_internal_ram_of_pseudo_low_internal_ram M sigma
465   (low_internal_ram pseudo_assembly_program cm s))
466  =low_internal_ram_of_pseudo_low_internal_ram M sigma
467   (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
468               
469lemma insert_low_internal_ram_status_of_pseudo_status:
470 ∀M,cm,sigma,policy,s,addr,v,v'.
471 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
472  insert Byte 7 addr v'
473   (low_internal_ram (BitVectorTrie Byte 16)
474    (code_memory_of_pseudo_assembly_program cm sigma policy)
475    (status_of_pseudo_status M cm s sigma policy))
476  = low_internal_ram_of_pseudo_low_internal_ram M sigma
477     (insert Byte 7 addr v
478      (low_internal_ram pseudo_assembly_program cm s)).
479 /2 by insert_low_internal_ram_of_pseudo_low_internal_ram/
480qed.
481
482(* Real axiom ATM *)
483axiom insert_high_internal_ram_of_pseudo_high_internal_ram:
484 ∀M,sigma,cm,s,addr,v,v'.
485 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
486  insert Byte 7 addr v'
487  (high_internal_ram_of_pseudo_high_internal_ram M sigma
488   (high_internal_ram pseudo_assembly_program cm s))
489  =high_internal_ram_of_pseudo_high_internal_ram M sigma
490   (insert Byte 7 addr v (high_internal_ram pseudo_assembly_program cm s)).
491
492lemma insert_high_internal_ram_status_of_pseudo_status:
493 ∀M,cm,sigma,policy,s,addr,v,v'.
494 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
495  insert Byte 7 addr v'
496   (high_internal_ram (BitVectorTrie Byte 16)
497    (code_memory_of_pseudo_assembly_program cm sigma policy)
498    (status_of_pseudo_status M cm s sigma policy))
499  = high_internal_ram_of_pseudo_high_internal_ram M sigma
500     (insert Byte 7 addr v
501      (high_internal_ram pseudo_assembly_program cm s)).
502 /2 by insert_high_internal_ram_of_pseudo_high_internal_ram/
503qed.
504
505lemma bit_address_of_register_status_of_pseudo_status:
506 ∀M,cm,s,sigma,policy,r.
507  bit_address_of_register …
508  (code_memory_of_pseudo_assembly_program cm sigma policy)
509  (status_of_pseudo_status M cm s sigma policy) r =
510  bit_address_of_register … cm s r.
511 #M #cm #s #sigma #policy #r whd in ⊢ (??%%);
512 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
513 @pair_elim #un #ln #_
514 @pair_elim #r1 #r0 #_ %
515qed.
516
517(*CSC: provable using the axiom in AssemblyProof, but this one seems more
518  primitive *)
519axiom lookup_low_internal_ram_of_pseudo_low_internal_ram:
520 ∀M,sigma,cm,s,s',addr.
521  map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr)
522  (lookup Byte 7 addr
523   (low_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' →
524  lookup Byte 7 addr
525  (low_internal_ram_of_pseudo_low_internal_ram M sigma
526   (low_internal_ram pseudo_assembly_program cm s)) (zero 8)
527  = s'.
528
529(*CSC: provable using the axiom in AssemblyProof, but this one seems more
530  primitive *)
531axiom lookup_high_internal_ram_of_pseudo_high_internal_ram:
532 ∀M,sigma,cm,s,s',addr.
533  map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr)
534  (lookup Byte 7 addr
535   (high_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' →
536  lookup Byte 7 addr
537  (high_internal_ram_of_pseudo_high_internal_ram M sigma
538   (high_internal_ram pseudo_assembly_program cm s)) (zero 8)
539  = s'.
540
541lemma get_register_status_of_pseudo_status:
542 ∀M,cm,sigma,policy,s,s',s'',r.
543  status_of_pseudo_status M cm s sigma policy = s' →
544  map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r)
545   (get_register … cm s r) = s'' →
546  get_register …
547   (code_memory_of_pseudo_assembly_program cm sigma policy)
548   s' r = s''.
549 #M #cm #sigma #policy #s #s' #s'' #r #s_refl #s_refl' <s_refl <s_refl'
550 whd in match get_register; normalize nodelta
551 whd in match status_of_pseudo_status; normalize nodelta
552 >bit_address_of_register_status_of_pseudo_status
553 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … (refl …))
554qed.
555
556lemma external_ram_status_of_pseudo_status:
557 ∀M,cm,s,sigma,policy.
558  external_ram …
559   (code_memory_of_pseudo_assembly_program cm sigma policy)
560   (status_of_pseudo_status M cm s sigma policy) =
561  external_ram … cm s.
562 //
563qed.
564
565lemma set_external_ram_status_of_pseudo_status:
566  ∀M,cm,ps,sigma,policy,ram.
567    set_external_ram …
568      (code_memory_of_pseudo_assembly_program cm sigma policy)
569      (status_of_pseudo_status M cm ps sigma policy)
570      ram =
571    status_of_pseudo_status M cm (set_external_ram … cm ps ram) sigma policy.
572  //
573qed.
574
575lemma set_register_status_of_pseudo_status:
576 ∀M,sigma,policy,cm,s,s',r,v,v'.
577  s' = status_of_pseudo_status M cm s sigma policy →
578  map_internal_ram_address_using_pseudo_address_map M sigma
579   (false:::bit_address_of_register pseudo_assembly_program cm s r) v =v' →
580  set_register (BitVectorTrie Byte 16)
581   (code_memory_of_pseudo_assembly_program cm sigma policy)
582   s' r v'
583  = status_of_pseudo_status M cm (set_register pseudo_assembly_program cm s r v)
584    sigma policy.
585  #M #sigma #policy #cm #s #s' #r #v #v' #s_refl >s_refl #v_ok
586 whd in match set_register; normalize nodelta
587 >bit_address_of_register_status_of_pseudo_status
588 >(insert_low_internal_ram_status_of_pseudo_status … v_ok)
589 @set_low_internal_ram_status_of_pseudo_status %
590qed.
591
592definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝
593 λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λsigma. λaddr.
594  let 〈low,high,accA〉 ≝ M in
595  match addr with
596  [ INDIRECT i ⇒
597     lookup_opt …
598      (bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) low = None …
599  | EXT_INDIRECT e ⇒
600     lookup_opt …
601      (bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) low = None …
602  | ACC_DPTR ⇒
603    (* XXX: \snd M = None plus in the very rare case when we are trying to dereference a null (O) pointer
604            in the ACC_A *)
605      map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) =
606        get_8051_sfr … cm s SFR_ACC_A
607  | ACC_PC ⇒
608      (* XXX: as above *)
609      map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) =
610        get_8051_sfr … cm s SFR_ACC_A ∧ sigma (program_counter … s) = program_counter … s
611  | _ ⇒ True ].
612
613definition map_address_mode_using_internal_pseudo_address_map_ok2 ≝
614 λT,M,sigma,cm.λs:PreStatus T cm.λaddr,v.
615  match addr with
616  [ DIRECT d ⇒
617     let 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit … 1 7 d in
618     match head' … bit_one with
619     [ true ⇒
620      map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v
621     | false ⇒
622      map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ]
623  | INDIRECT i ⇒
624     let register ≝ get_register ?? s [[ false; false; i ]] in
625     map_internal_ram_address_using_pseudo_address_map M sigma register v
626  | REGISTER r ⇒
627     map_internal_ram_address_using_pseudo_address_map M sigma
628      (false:::bit_address_of_register … s r) v
629  | ACC_A ⇒
630     map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v
631  | _ ⇒ v ].
632
633(*CSC: move elsewhere*)
634lemma eq_head': ∀A,n,v. v = head' A n v ::: tail … v.
635 #A #n #v inversion v in ⊢ ?;
636 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) /2/
637 | #m #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ' >EQ' % ]
638qed.
639
640(*CSC: move elsewhere*)
641lemma tail_singleton: ∀A,v. tail A 0 v = [[]].
642 #A #v inversion v in ⊢ ?;
643 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) #H destruct(H)
644 | #n #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ1 >EQ1 normalize
645   /2 by jmeq_to_eq/
646 ]
647qed.
648
649(*CSC: move elsewhere*)
650lemma eq_cons_head_append:
651 ∀A,n.∀hd: Vector A 1. ∀tl: Vector A n.
652  head' A 0 hd:::tl = hd@@tl.
653 #A #n #hd #tl >(eq_head' … hd) >tail_singleton %
654qed.
655
656lemma set_arg_8_status_of_pseudo_status':
657  ∀cm.
658  ∀ps.
659  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
660  ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
661   s' = status_of_pseudo_status M cm ps sigma policy →
662   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
663   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
664    set_arg_8 (BitVectorTrie Byte 16)
665      (code_memory_of_pseudo_assembly_program cm sigma policy)
666      s' addr value' =
667    status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
668  whd in match set_arg_8; normalize nodelta
669  @(let m ≝ pseudo_assembly_program in λcm, s. λa: [[ direct ; indirect ; registr ;
670                                   acc_a ; acc_b ; ext_indirect ;
671                                   ext_indirect_dptr ]]. λv.
672    match a return λaddr. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
673                                                acc_a ; acc_b ; ext_indirect ;
674                                                ext_indirect_dptr ]] addr) →
675                   Σp.?
676            with
677      [ DIRECT d ⇒
678        λdirect: True.
679          deplet 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit ? 1 7 d in
680            match head' … bit_one with
681              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
682              | false ⇒
683                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
684                  set_low_internal_ram ?? s memory
685              ]
686             
687      | INDIRECT i ⇒
688        λindirect: True.
689          let register ≝ get_register ?? s [[ false; false; i ]] in
690          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
691            match head' … bit_one with
692              [ false ⇒
693                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
694                  set_low_internal_ram ?? s memory
695              | true ⇒
696                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
697                  set_high_internal_ram ?? s memory
698              ]
699      | REGISTER r ⇒ λregister: True. set_register ?? s r v
700      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
701      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
702      | EXT_INDIRECT e ⇒
703        λext_indirect: True.
704          let address ≝ get_register ?? s [[ false; false; e ]] in
705          let padded_address ≝ pad 8 8 address in
706          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
707            set_external_ram ?? s memory
708      | EXT_INDIRECT_DPTR ⇒
709        λext_indirect_dptr: True.
710          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
711          let memory ≝ insert ? 16 address v (external_ram ?? s) in
712            set_external_ram ?? s memory
713      | _ ⇒
714        λother: False.
715          match other in False with [ ]
716      ] (subaddressing_modein … a)) normalize nodelta
717  #M #sigma #policy #s' #v' #s_refl >s_refl
718  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
719  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
720  [1,2:
721    <vsplit_refl normalize nodelta >p normalize nodelta
722    [ >(vsplit_ok … vsplit_refl) #_ @set_bit_addressable_sfr_status_of_pseudo_status
723    | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
724  |3,4: cases M * -M #low #high #accA normalize nodelta
725      #EQ1 #EQ2 change with (get_register ????) in match register in p;
726      >(get_register_status_of_pseudo_status … (refl …) (refl …))
727      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
728      whd in match (lookup_from_internal_ram ??);
729      >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
730      [ >(insert_high_internal_ram_status_of_pseudo_status … v)
731      | >(insert_low_internal_ram_status_of_pseudo_status … v) ]
732      // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
733  |5: cases M * -M #low #high #accA normalize nodelta
734      #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) (refl …))
735      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
736      whd in match lookup_from_internal_ram; normalize nodelta
737      >EQ1 normalize nodelta
738      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status
739  |6: #EQ1 #EQ2 <EQ2 /2 by set_register_status_of_pseudo_status/
740  |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/
741  |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
742  |9: #_ #EQ <EQ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
743      >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
744      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] %
745qed.
746
747lemma set_arg_8_status_of_pseudo_status:
748  ∀cm.
749  ∀ps.
750  ∀addr, addr':[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
751  ∀value.
752  ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
753   addr = addr' →
754   s' = status_of_pseudo_status M cm ps sigma policy →
755   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
756   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
757    set_arg_8 (BitVectorTrie Byte 16)
758      (code_memory_of_pseudo_assembly_program cm sigma policy)
759      s' addr value' =
760    status_of_pseudo_status M cm (set_arg_8 … cm ps addr' value) sigma policy.
761  #cm #ps #addr #addr' #value
762  cases (set_arg_8_status_of_pseudo_status' cm ps addr value) #_ #relevant
763  #M #sigma #policy #s' #value' #addr_refl <addr_refl
764  @relevant
765qed.
766
767lemma p1_latch_status_of_pseudo_status:
768    ∀M.
769    ∀sigma.
770    ∀policy.
771    ∀code_memory: pseudo_assembly_program.
772    ∀s: PreStatus … code_memory.
773    ∀s'.
774    s' = status_of_pseudo_status M code_memory s sigma policy →
775    (p1_latch (BitVectorTrie Byte 16)
776      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
777      s' =
778    (p1_latch pseudo_assembly_program code_memory s)).
779  #M #sigma #policy #code_memory #s #s' #s_refl >s_refl //
780qed.
781
782lemma p3_latch_status_of_pseudo_status:
783    ∀M.
784    ∀sigma.
785    ∀policy.
786    ∀code_memory: pseudo_assembly_program.
787    ∀s: PreStatus … code_memory.
788    ∀s'.
789    s' = status_of_pseudo_status M code_memory s sigma policy →
790    (p3_latch (BitVectorTrie Byte 16)
791      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
792      (status_of_pseudo_status M code_memory s sigma policy) =
793    (p3_latch pseudo_assembly_program code_memory s)).
794  #M #sigma #policy #code_memory #s #s' #s_refl >s_refl //
795qed.
796
797lemma get_bit_addressable_sfr_status_of_pseudo_status':
798  let M ≝ pseudo_assembly_program in
799    ∀code_memory: M.
800    ∀s: PreStatus M code_memory.
801    ∀d: Byte.
802    ∀l: bool.
803      Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'.
804        s' = status_of_pseudo_status M code_memory s sigma policy →
805        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
806          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
807          s' d l =
808        map_address_Byte_using_internal_pseudo_address_map M sigma
809         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)).
810  whd in match get_bit_addressable_sfr;
811  whd in match map_address_Byte_using_internal_pseudo_address_map;
812  normalize nodelta
813  @(let M ≝ pseudo_assembly_program in
814    λcode_memory:M.
815    λs: PreStatus M code_memory.
816    λb: Byte.
817    λl: bool.
818    match sfr_of_Byte b with
819    [ None ⇒ match not_implemented in False with [ ]
820    | Some sfr8051_8052 ⇒
821    match sfr8051_8052 with
822    [ inl sfr ⇒
823      match sfr with
824      [ SFR_P1 ⇒
825        if l then
826          p1_latch … s
827        else
828          get_8051_sfr … s SFR_P1
829      | SFR_P3 ⇒
830        if l then
831          p3_latch … s
832        else
833          get_8051_sfr … s SFR_P3
834      | _ ⇒ get_8051_sfr … s sfr
835      ]
836    | inr sfr ⇒ get_8052_sfr M code_memory s sfr
837    ]
838    ])
839  #M #sigma #policy #s' #s_refl >s_refl normalize nodelta
840  /2 by get_8051_sfr_status_of_pseudo_status, p1_latch_status_of_pseudo_status, p3_latch_status_of_pseudo_status/
841qed.
842
843lemma get_bit_addressable_sfr_status_of_pseudo_status:
844  let M ≝ pseudo_assembly_program in
845    ∀code_memory: M.
846    ∀s: PreStatus M code_memory.
847    ∀d: Byte.
848    ∀l: bool.
849    ∀M. ∀sigma. ∀policy. ∀s'. ∀s''.
850      map_address_Byte_using_internal_pseudo_address_map M sigma
851         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l) = s'' →
852      s' = status_of_pseudo_status M code_memory s sigma policy →
853        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
854          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
855          s' d l) = s''.
856 #code #s #d #v
857 cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ #relevant
858 #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl >s_refl' @relevant %
859qed.
860
861lemma program_counter_status_of_pseudo_status:
862    ∀M. ∀sigma: Word → Word. ∀policy.
863    ∀code_memory: pseudo_assembly_program.
864    ∀s: PreStatus ? code_memory.
865    ∀s'.
866    ∀s''.
867    sigma (program_counter … s) = s'' →
868    s' = status_of_pseudo_status M code_memory s sigma policy →
869      program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy)
870        s' = s''.
871  #M #sigma #policy #code_memory #s #s' #s'' #s_refl #s_refl' <s_refl >s_refl' //
872qed.
873
874lemma get_cy_flag_status_of_pseudo_status:
875  ∀M, cm, sigma, policy, s, s'.
876  s' = status_of_pseudo_status M cm s sigma policy →
877  (get_cy_flag (BitVectorTrie Byte 16)
878    (code_memory_of_pseudo_assembly_program cm sigma policy)
879    s' =
880  get_cy_flag pseudo_assembly_program cm s).
881  #M #cm #sigma #policy #s #s' #s_refl >s_refl
882  whd in match get_cy_flag; normalize nodelta
883  >(get_index_v_status_of_pseudo_status … (refl …)) %
884qed.
885
886lemma get_arg_8_status_of_pseudo_status':
887  ∀cm.
888  ∀ps.
889  ∀l.
890  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
891    Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'.
892      s' = status_of_pseudo_status M cm ps sigma policy →
893      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
894      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
895      s' l addr =
896      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr).
897  whd in match get_arg_8; normalize nodelta
898  @(let m ≝ pseudo_assembly_program in
899    λ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]].
900    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
901      [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
902      | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
903      | DATA d ⇒ λdata: True. d
904      | REGISTER r ⇒ λregister: True. get_register ?? s r
905      | EXT_INDIRECT_DPTR ⇒
906        λext_indirect_dptr: True.
907          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
908            lookup ? 16 address (external_ram ?? s) (zero 8)
909      | EXT_INDIRECT e ⇒
910        λext_indirect: True.
911          let address ≝ get_register ?? s [[ false; false; e ]]  in
912          let padded_address ≝ pad 8 8 address in
913            lookup ? 16 padded_address (external_ram ?? s) (zero 8)
914      | ACC_DPTR ⇒
915        λacc_dptr: True.
916          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
917          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
918          let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
919            lookup ? 16 address (external_ram ?? s) (zero 8)
920      | ACC_PC ⇒
921        λacc_pc: True.
922          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
923          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
924            lookup ? 16 address (external_ram ?? s) (zero 8)
925      | DIRECT d ⇒
926        λdirect: True.
927          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
928            match head' … hd with
929            [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
930            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
931            ]
932      | INDIRECT i ⇒
933        λindirect: True.
934          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
935            match head' … hd with
936            [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)
937            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
938            ]
939      | _ ⇒ λother: False.
940        match other in False with [ ]
941      ] (subaddressing_modein … a)) normalize nodelta
942  #M #sigma #policy #s' #s_refl >s_refl
943  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
944  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
945  [1:
946    #_ >p normalize nodelta >p1 normalize nodelta
947    @(get_bit_addressable_sfr_status_of_pseudo_status … (refl …)) %
948  |2:
949    #_>p normalize nodelta >p1 normalize nodelta
950    @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) %
951  |3,4: cases M -M * #low #high #accA
952    #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …))
953    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
954    whd in match lookup_from_internal_ram; normalize nodelta
955    >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta
956    [1:
957      @(lookup_high_internal_ram_of_pseudo_high_internal_ram … 〈low,high,accA〉 sigma)
958    |2:
959      @(lookup_low_internal_ram_of_pseudo_low_internal_ram … 〈low,high,accA〉 sigma)
960    ]
961    @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
962  |5: cases M -M * #low #high #accA
963    #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …))
964    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
965    whd in match lookup_from_internal_ram; normalize nodelta
966    >assoc_list_assm normalize nodelta %
967  |6,7,8,9:
968    #_ /2 by refl, get_register_status_of_pseudo_status, get_index_v_status_of_pseudo_status/
969  |10: cases M -M * #low #high #accA
970    #acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
971    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
972    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
973    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
974    >acc_a_assm >p normalize nodelta //
975  |11: cases M -M * #low #high #accA
976    * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
977    >(program_counter_status_of_pseudo_status … (refl …) (refl …))
978    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
979    >sigma_assm >map_acc_a_assm >p normalize nodelta //
980  |12:
981    #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
982    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
983    >external_ram_status_of_pseudo_status //
984  ]
985qed.
986
987lemma get_arg_8_status_of_pseudo_status:
988  ∀cm.
989  ∀ps.
990  ∀l.
991  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
992  ∀M. ∀sigma. ∀policy. ∀s', s''.
993      s' = status_of_pseudo_status M cm ps sigma policy →
994      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr) = s'' →
995      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
996      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
997      s' l addr = s''.
998  #cm #ps #l #addr
999  cases (get_arg_8_status_of_pseudo_status' cm ps l addr) #_ #relevant
1000  #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl'
1001  @relevant assumption
1002qed.
1003
1004lemma get_arg_16_status_of_pseudo_status:
1005  ∀cm.
1006  ∀ps.
1007  ∀addr: [[data16]].
1008  ∀M. ∀sigma. ∀policy. ∀s'.
1009    s' = status_of_pseudo_status M cm ps sigma policy →
1010      get_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1011      s' addr =
1012      (get_arg_16 … cm ps addr).
1013  #cm #ps #addr #M #sigma #policy #s' #s_refl <s_refl //
1014qed.
1015
1016lemma set_arg_16_status_of_pseudo_status:
1017  ∀cm.
1018  ∀ps.
1019  ∀addr,addr': [[dptr]].
1020  ∀v,v': Word.
1021  ∀M. ∀sigma. ∀policy. ∀s'.
1022    s' = status_of_pseudo_status M cm ps sigma policy →
1023    v=v' → addr=addr' →
1024      set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1025      s' v' addr' =
1026      status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy.
1027  #cm #ps #addr #addr' #v #v' #M #sigma #policy #s' #s_refl >s_refl #addr_refl
1028  <addr_refl #v_refl <v_refl
1029  @(subaddressing_mode_elim … addr)
1030  whd in match set_arg_16; normalize nodelta
1031  whd in match set_arg_16'; normalize nodelta
1032  @(vsplit_elim bool ???) #bu #bl #bu_bl_refl normalize nodelta
1033  @set_8051_sfr_status_of_pseudo_status try %
1034  @set_8051_sfr_status_of_pseudo_status %
1035qed.
1036
1037definition map_bit_address_mode_using_internal_pseudo_address_map_get ≝
1038 λM:internal_pseudo_address_map.λcm: pseudo_assembly_program.λs:PreStatus ? cm.λsigma: Word → Word. λaddr. λl.
1039  match addr with
1040  [ BIT_ADDR b ⇒
1041    let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1042    match head' … bit_1 with
1043    [ true ⇒
1044      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1045      let trans ≝ true:::four_bits @@ [[false; false; false]] in
1046        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
1047    | false ⇒
1048      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1049      let address' ≝ [[true; false; false]]@@four_bits in
1050      let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1051      map_internal_ram_address_using_pseudo_address_map M sigma
1052          (false:::address') t = t
1053    ]
1054  | N_BIT_ADDR b ⇒
1055    let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1056    match head' … bit_1 with
1057    [ true ⇒
1058      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1059      let trans ≝ true:::four_bits @@ [[false; false; false]] in
1060        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
1061    | false ⇒
1062      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1063      let address' ≝ [[true; false; false]]@@four_bits in
1064      let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1065      map_internal_ram_address_using_pseudo_address_map M sigma
1066          (false:::address') t = t
1067    ]
1068  | _ ⇒ True ].
1069
1070lemma get_arg_1_status_of_pseudo_status':
1071  ∀cm.
1072  ∀ps.
1073  ∀addr: [[bit_addr; n_bit_addr; carry]].
1074  ∀l.
1075    Σb: bool. ∀M. ∀sigma. ∀policy. ∀s'.
1076      s' = status_of_pseudo_status M cm ps sigma policy →
1077      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
1078      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1079      s' addr l =
1080      (get_arg_1 … cm ps addr l).
1081  whd in match get_arg_1; normalize nodelta
1082  @(let m ≝ pseudo_assembly_program in
1083    λcm: m. λs: PseudoStatus cm. λa:[[bit_addr; n_bit_addr; carry]]. λl.
1084    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
1085                                                 n_bit_addr ;
1086                                                 carry ]] x) → Σb: bool. ? with
1087      [ BIT_ADDR b ⇒
1088        λbit_addr: True.
1089        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1090        match head' … bit_1 with
1091        [ true ⇒
1092          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1093          let trans ≝ true:::four_bits @@ [[false; false; false]] in
1094          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
1095            get_index_v … sfr (nat_of_bitvector … three_bits) ?
1096        | false ⇒
1097          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1098          let address' ≝ [[true; false; false]]@@four_bits in
1099          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1100            get_index_v … t (nat_of_bitvector … three_bits) ?
1101        ]
1102      | N_BIT_ADDR n ⇒
1103        λn_bit_addr: True.
1104        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
1105        match head' … bit_1 with
1106        [ true ⇒
1107          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1108          let trans ≝ true:::four_bits @@ [[false; false; false]] in
1109          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
1110            ¬(get_index_v ?? sfr (nat_of_bitvector … three_bits) ?)
1111        | false ⇒
1112          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
1113          let address' ≝ [[true; false; false]]@@four_bits in
1114          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1115            ¬(get_index_v … t (nat_of_bitvector … three_bits) ?)
1116        ]
1117      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
1118      | _ ⇒ λother.
1119        match other in False with [ ]
1120      ] (subaddressing_modein … a)) normalize nodelta
1121  [4,5,8,9: //]
1122  #M #sigma #policy #s' #s_refl >s_refl
1123  [1:
1124    #_ >(get_cy_flag_status_of_pseudo_status … (refl …)) %
1125  |2,4:
1126    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta destruct >p2
1127    normalize nodelta
1128    >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …)) #map_address_assm
1129    >map_address_assm %
1130  |3,5:
1131    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
1132    whd in match status_of_pseudo_status; normalize nodelta destruct >p2 normalize nodelta
1133    >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …))
1134    #map_address_assm >map_address_assm %
1135  ]
1136qed.
1137
1138lemma get_arg_1_status_of_pseudo_status:
1139  ∀cm.
1140  ∀ps.
1141  ∀addr, addr': [[bit_addr; n_bit_addr; carry]].
1142  ∀l.
1143  ∀M. ∀sigma. ∀policy. ∀s'.
1144    addr = addr' →
1145    s' = status_of_pseudo_status M cm ps sigma policy →
1146      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
1147      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1148      s' addr l =
1149      (get_arg_1 … cm ps addr' l).
1150  #cm #ps #addr #addr' #l
1151  cases (get_arg_1_status_of_pseudo_status' cm ps addr l) #_ #assm
1152  #M #sigma #policy #s' #addr_refl <addr_refl
1153  @assm
1154qed.
1155
1156(*CSC: daemon
1157definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝
1158  λM: internal_pseudo_address_map.
1159  λcm: pseudo_assembly_program.
1160  λs: PreStatus ? cm.
1161  λsigma: Word → Word.
1162  λaddr: [[bit_addr; carry]].
1163  λv: Bit.
1164  match addr with
1165  [ BIT_ADDR b ⇒
1166    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
1167    match head' … bit_1 with
1168    [ true ⇒
1169      let address ≝ nat_of_bitvector … seven_bits in
1170      let d ≝ address ÷ 8 in
1171      let m ≝ address mod 8 in
1172      let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1173      let sfr ≝ get_bit_addressable_sfr … s t true in
1174        map_address_Byte_using_internal_pseudo_address_map M sigma t sfr = sfr
1175    | false ⇒
1176      let address ≝ nat_of_bitvector … seven_bits in
1177      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1178      let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1179        map_internal_ram_address_using_pseudo_address_map M sigma
1180          (false:::address') t = t
1181    ]   
1182  | CARRY ⇒ True
1183  | _ ⇒ True
1184  ].
1185
1186definition map_bit_address_mode_using_internal_pseudo_address_map_set_2 ≝
1187  λM: internal_pseudo_address_map.
1188  λcm: pseudo_assembly_program.
1189  λs: PreStatus ? cm.
1190  λsigma: Word → Word.
1191  λaddr: [[bit_addr; carry]].
1192  λv: Bit.
1193  match addr with
1194  [ BIT_ADDR b ⇒
1195    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
1196    match head' … bit_1 with
1197    [ true ⇒
1198      let address ≝ nat_of_bitvector … seven_bits in
1199      let d ≝ address ÷ 8 in
1200      let m ≝ address mod 8 in
1201      let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1202      let sfr ≝ get_bit_addressable_sfr … s t true in
1203      let new_sfr ≝ set_index … sfr m v ? in
1204        map_address_Byte_using_internal_pseudo_address_map M sigma new_sfr t = t
1205    | false ⇒
1206      let address ≝ nat_of_bitvector … seven_bits in
1207      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1208      let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1209      let n_bit ≝ set_index … t (modulus address 8) v ? in
1210      let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
1211        map_internal_ram_address_using_pseudo_address_map M sigma
1212          (false:::address') n_bit = n_bit
1213    ]   
1214  | CARRY ⇒ True
1215  | _ ⇒ True
1216  ].
1217  @modulus_less_than
1218qed.
1219
1220lemma set_arg_1_status_of_pseudo_status':
1221  ∀cm: pseudo_assembly_program.
1222  ∀ps: PreStatus pseudo_assembly_program cm.
1223  ∀addr: [[bit_addr; carry]].
1224  ∀b: Bit.
1225    Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀b'.
1226      b = b' →
1227      status_of_pseudo_status M cm ps sigma policy = s' →
1228      map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
1229      map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b →
1230        set_arg_1 (BitVectorTrie Byte 16)
1231          (code_memory_of_pseudo_assembly_program cm sigma policy)
1232          s' addr b =
1233        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy.
1234  whd in match set_arg_1; normalize nodelta
1235  whd in ⊢ (? → ? → ? → ? → ??(λx.? → ? → ? → ? → ? → ? → ? → %?????? → %?????? → ?));
1236  normalize nodelta
1237  @(let m ≝ pseudo_assembly_program in
1238    λcm.
1239    λs: PreStatus m cm.
1240    λa: [[bit_addr; carry]].
1241    λv: Bit.
1242    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σp. ? with
1243      [ BIT_ADDR b ⇒ λbit_addr: True.
1244        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
1245        match head' … bit_1 with
1246        [ true ⇒
1247          let address ≝ nat_of_bitvector … seven_bits in
1248          let d ≝ address ÷ 8 in
1249          let m ≝ address mod 8 in
1250          let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1251          let sfr ≝ get_bit_addressable_sfr … s t true in
1252          let new_sfr ≝ set_index … sfr m v ? in
1253            set_bit_addressable_sfr … s new_sfr t
1254        | false ⇒
1255          let address ≝ nat_of_bitvector … seven_bits in
1256          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1257          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1258          let n_bit ≝ set_index … t (modulus address 8) v ? in
1259          let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
1260            set_low_internal_ram … s memory
1261        ]
1262      | CARRY ⇒
1263        λcarry: True.
1264        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1265        let new_psw ≝ v:::seven_bits in
1266          set_8051_sfr ?? s SFR_PSW new_psw
1267      | _ ⇒
1268        λother: False.
1269          match other in False with
1270            [ ]
1271      ] (subaddressing_modein … a)) normalize nodelta
1272  try @modulus_less_than #M #sigma #policy #s' #b' #b_refl <b_refl #s_refl <s_refl
1273  [1:
1274    #_ #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
1275    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
1276    >p normalize nodelta @set_8051_sfr_status_of_pseudo_status %
1277  |2,3:
1278    >p normalize nodelta >p1 normalize nodelta
1279    #map_bit_address_assm_1 #map_bit_address_assm_2
1280    [1:
1281      >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …))
1282      >map_bit_address_assm_1
1283      >(set_bit_addressable_sfr_status_of_pseudo_status cm s … map_bit_address_assm_2) %
1284    |2:
1285      whd in match status_of_pseudo_status in ⊢ (??(????%)?); normalize nodelta
1286      >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …))
1287      >map_bit_address_assm_1
1288      >(insert_low_internal_ram_of_pseudo_low_internal_ram … map_bit_address_assm_2)
1289      >set_low_internal_ram_status_of_pseudo_status in ⊢ (??%?); %
1290    ]
1291  ]
1292qed.
1293
1294lemma set_arg_1_status_of_pseudo_status:
1295  ∀cm: pseudo_assembly_program.
1296  ∀ps: PreStatus pseudo_assembly_program cm.
1297  ∀addr: [[bit_addr; carry]].
1298  ∀b: Bit.
1299  ∀M. ∀sigma. ∀policy. ∀s'. ∀b'.
1300      b = b' →
1301      status_of_pseudo_status M cm ps sigma policy = s' →
1302      map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
1303      map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b →
1304        set_arg_1 (BitVectorTrie Byte 16)
1305          (code_memory_of_pseudo_assembly_program cm sigma policy)
1306          s' addr b =
1307        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy.
1308  #cm #ps #addr #b
1309  cases (set_arg_1_status_of_pseudo_status' cm ps addr b) #_ #relevant
1310  @relevant
1311qed.*)
1312
1313lemma clock_status_of_pseudo_status:
1314 ∀M,cm,sigma,policy,s,s'.
1315  s' = status_of_pseudo_status M cm s sigma policy →
1316  clock …
1317   (code_memory_of_pseudo_assembly_program cm sigma policy)
1318   s'
1319  = clock … cm s.
1320  #M #cm #sigma #policy #s #s' #s_refl >s_refl //
1321qed.
1322
1323lemma set_clock_status_of_pseudo_status:
1324 ∀M,cm,sigma,policy,s,s',v,v'.
1325 s' = status_of_pseudo_status M cm s sigma policy →
1326 v = v' →
1327  set_clock …
1328   (code_memory_of_pseudo_assembly_program cm sigma policy)
1329   s' v
1330  = status_of_pseudo_status M cm (set_clock … cm s v') sigma policy.
1331  #M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl >s_refl <v_refl //
1332qed.
1333
1334lemma set_flags_status_of_pseudo_status:
1335  ∀M.
1336  ∀sigma.
1337  ∀policy.
1338  ∀code_memory: pseudo_assembly_program.
1339  ∀s: PreStatus ? code_memory.
1340  ∀s'.
1341  ∀b, b': Bit.
1342  ∀opt, opt': option Bit.
1343  ∀c, c': Bit.
1344    b = b' →
1345    opt = opt' →
1346    c = c' →
1347    s' = status_of_pseudo_status M code_memory s sigma policy →
1348      set_flags … s' b opt c =
1349        status_of_pseudo_status M code_memory (set_flags … code_memory s b' opt' c') sigma policy.
1350  ** #low #high #accA #sigma #policy #code_memory #s #s' #b #b' #opt #opt' #c #c'
1351  #b_refl #opt_refl #c_refl <b_refl <opt_refl <c_refl #s_refl >s_refl
1352  whd in match set_flags; normalize nodelta
1353  @set_8051_sfr_status_of_pseudo_status try %
1354  whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
1355  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
1356  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %] 
1357  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
1358  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
1359  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
1360  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %] 
1361  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
1362  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
1363  %
1364qed.
1365
1366lemma get_ac_flag_status_of_pseudo_status:
1367  ∀M: internal_pseudo_address_map.
1368  ∀sigma: Word → Word.
1369  ∀policy: Word → bool.
1370  ∀code_memory: pseudo_assembly_program.
1371  ∀s: PreStatus ? code_memory.
1372  ∀s'.
1373    s' = status_of_pseudo_status M code_memory s sigma policy →
1374      get_ac_flag ?? s' = get_ac_flag ? code_memory s.
1375  #M #sigma #policy #code_memory #s #s' #s_refl >s_refl
1376  whd in match get_ac_flag; normalize nodelta
1377  whd in match status_of_pseudo_status; normalize nodelta
1378  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
1379  cases (\snd M) try % normalize nodelta ** normalize nodelta
1380  #address
1381  @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
1382  whd in match sfr_8051_index; normalize nodelta
1383  >get_index_v_set_index_miss [2,4: /2/] %
1384qed.
1385
1386lemma get_ov_flag_status_of_pseudo_status:
1387  ∀M: internal_pseudo_address_map.
1388  ∀sigma: Word → Word.
1389  ∀policy: Word → bool.
1390  ∀code_memory: pseudo_assembly_program.
1391  ∀s: PreStatus ? code_memory.
1392  ∀s'.
1393    s' = status_of_pseudo_status M code_memory s sigma policy →
1394      get_ov_flag ?? s' = get_ov_flag ? code_memory s.
1395  #M #sigma #policy #code_memory #s #s' #s_refl >s_refl
1396  whd in match get_ov_flag; normalize nodelta
1397  whd in match status_of_pseudo_status; normalize nodelta
1398  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
1399  cases (\snd M) try %
1400  ** normalize nodelta #address
1401  @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
1402  whd in match sfr_8051_index; normalize nodelta
1403  >get_index_v_set_index_miss [2,4: /2/] %
1404qed.
1405
1406(*CSC: useless?
1407lemma get_arg_8_pseudo_addressing_mode_ok:
1408  ∀M: internal_pseudo_address_map.
1409  ∀cm: pseudo_assembly_program.
1410  ∀ps: PreStatus pseudo_assembly_program cm.
1411  ∀sigma: Word → Word.
1412  ∀policy: Word → bool.
1413  ∀addr1: [[registr; direct]].
1414    assert_data pseudo_assembly_program M cm ps addr1 = true →
1415      get_arg_8 (BitVectorTrie Byte 16)
1416        (code_memory_of_pseudo_assembly_program cm sigma policy)
1417        (status_of_pseudo_status M cm ps sigma policy) true addr1 =
1418      get_arg_8 pseudo_assembly_program cm ps true addr1.
1419  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1420  #M #cm #ps #sigma #policy #addr1
1421  @(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%);
1422  [1:
1423    whd in ⊢ (??%? → ??%?);
1424    whd in match bit_address_of_register; normalize nodelta
1425    @pair_elim #un #ln #un_ln_refl
1426    lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
1427    @(pair_replace ?????????? un_ln_refl)
1428    [1:
1429      whd in match get_8051_sfr; normalize nodelta
1430      whd in match sfr_8051_index; normalize nodelta
1431      @eq_f <get_index_v_special_function_registers_8051_not_acc_a
1432      try % #absurd destruct(absurd)
1433    |2:
1434      #assembly_mode_ok_refl
1435      >low_internal_ram_of_pseudo_internal_ram_miss
1436      [1:
1437        %
1438      |2:
1439        cases (data_or_address ?????) in assembly_mode_ok_refl; normalize nodelta
1440        [1:
1441          #absurd destruct(absurd)
1442        |2:
1443          * normalize nodelta
1444          [1:
1445          |2:
1446            #_ #absurd destruct(absurd)
1447          ]
1448        #absurd try % @sym_eq assumption
1449      ]
1450    ]
1451  |2:
1452    #addressing_mode_ok_refl whd in ⊢ (??%?);
1453    @pair_elim #nu #nl #nu_nl_refl normalize nodelta XXX cases daemon (*
1454    @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
1455    inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
1456    [1:
1457      whd in ⊢ (??%%); normalize nodelta
1458      cases (eqb ??) normalize nodelta [1: % ]
1459      cases (eqb ??) normalize nodelta [1: % ]
1460      cases (eqb ??) normalize nodelta [1: % ]
1461      cases (eqb ??) normalize nodelta [1: % ]
1462      cases (eqb ??) normalize nodelta [1:
1463        @get_8051_sfr_status_of_pseudo_status
1464        #absurd destruct(absurd)
1465      ]
1466      cases (eqb ??) normalize nodelta [1:
1467        @get_8051_sfr_status_of_pseudo_status
1468        #absurd destruct(absurd)
1469      ]
1470      cases (eqb ??) normalize nodelta [1:
1471        @get_8051_sfr_status_of_pseudo_status
1472        #absurd destruct(absurd)
1473      ]
1474      cases (eqb ??) normalize nodelta [1:
1475        @get_8051_sfr_status_of_pseudo_status
1476        #absurd destruct(absurd)
1477      ]
1478      cases (eqb ??) normalize nodelta [1:
1479        @get_8051_sfr_status_of_pseudo_status
1480        #absurd destruct(absurd)
1481      ]
1482      cases (eqb ??) normalize nodelta [1: % ]
1483      cases (eqb ??) normalize nodelta [1: % ]
1484      cases (eqb ??) normalize nodelta [1: % ]
1485      cases (eqb ??) normalize nodelta [1: % ]
1486      cases (eqb ??) normalize nodelta [1: % ]
1487      cases (eqb ??) normalize nodelta [1:
1488        @get_8051_sfr_status_of_pseudo_status
1489        #absurd destruct(absurd)
1490      ]
1491      cases (eqb ??) normalize nodelta [1:
1492        @get_8051_sfr_status_of_pseudo_status
1493        #absurd destruct(absurd)
1494      ]
1495      cases (eqb ??) normalize nodelta [1:
1496        @get_8051_sfr_status_of_pseudo_status
1497        #absurd destruct(absurd)
1498      ]
1499      cases (eqb ??) normalize nodelta [1:
1500        @get_8051_sfr_status_of_pseudo_status
1501        #absurd destruct(absurd)
1502      ]
1503      cases (eqb ??) normalize nodelta [1:
1504        @get_8051_sfr_status_of_pseudo_status
1505        #absurd destruct(absurd)
1506      ]
1507      cases (eqb ??) normalize nodelta [1:
1508        @get_8051_sfr_status_of_pseudo_status
1509        #absurd destruct(absurd)
1510      ]
1511      cases (eqb ??) normalize nodelta [1:
1512        @get_8051_sfr_status_of_pseudo_status
1513        #absurd destruct(absurd)
1514      ]
1515      cases (eqb ??) normalize nodelta [1:
1516        @get_8051_sfr_status_of_pseudo_status
1517        #absurd destruct(absurd)
1518      ]
1519      cases (eqb ??) normalize nodelta [1:
1520        @get_8051_sfr_status_of_pseudo_status
1521        #absurd destruct(absurd)
1522      ]
1523      cases (eqb ??) normalize nodelta [1:
1524        @get_8051_sfr_status_of_pseudo_status
1525        #absurd destruct(absurd)
1526      ]
1527      inversion (eqb ??) #eqb_refl normalize nodelta [1:
1528        @get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl
1529        whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl)
1530        >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
1531        #assoc_list_assm cases (conjunction_true … assoc_list_assm) #_
1532        #relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) %
1533      ]
1534      cases (eqb ??) normalize nodelta [1:
1535        @get_8051_sfr_status_of_pseudo_status
1536        #absurd destruct(absurd)
1537      ] %
1538    |2:
1539      lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant
1540      whd in match status_of_pseudo_status; normalize nodelta
1541      >low_internal_ram_of_pseudo_internal_ram_miss try %
1542      cut(arg = false:::(three_bits@@nl))
1543      [1:
1544        <get_index_v_refl
1545        cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits)
1546        [1:
1547          cut(ignore = [[get_index_v bool 4 nu 0 ?]])
1548          [1:
1549            @le_S_S @le_O_n
1550          |2:
1551            cut(ignore = \fst (vsplit bool 1 3 nu))
1552            [1:
1553              >ignore_three_bits_refl %
1554            |2:
1555              #ignore_refl >ignore_refl
1556              cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl
1557              >nu_refl %
1558            ]
1559          |3:
1560            #ignore_refl >ignore_refl in ignore_three_bits_refl;
1561            #relevant lapply (vsplit_ok ?????? (sym_eq … relevant))
1562            #nu_refl <nu_refl %
1563          ]
1564        |2:
1565          #nu_refl change with (? = (?:::three_bits)@@?) <nu_refl
1566          @sym_eq @vsplit_ok >nu_nl_refl %
1567        ]
1568      |2:
1569        #arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant;
1570        normalize nodelta
1571        [1:
1572          cases (eq_bv ???) normalize #absurd destruct(absurd)
1573        |2:
1574          #_ %
1575        ]
1576      ]
1577    ]
1578  ]
1579qed.*)*)
1580
1581lemma addressing_mode_ok_to_map_address_using_internal_pseudo_address_map:
1582  ∀M, cm, ps, sigma, x.
1583  ∀addr1: [[acc_a]].
1584    assert_data pseudo_assembly_program M cm ps addr1=true →
1585      map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A x = x.
1586  #M #cm #ps #sigma #x #addr1
1587  @(subaddressing_mode_elim … addr1)
1588  whd in ⊢ (??%? → ??%?); cases M -M * #low #high * [//]
1589  * #upper_lower #address normalize nodelta #absurd destruct(absurd)
1590qed.
1591
1592lemma addressing_mode_ok_to_snd_M_data:
1593  ∀M, cm, ps.
1594  ∀addr: [[acc_a]].
1595  assert_data pseudo_assembly_program M cm ps addr = true →
1596    \snd M = None ….
1597  #M #cm #ps #addr
1598  @(subaddressing_mode_elim … addr)
1599  whd in ⊢ (??%? → ?); cases M * #low #high * normalize nodelta
1600  [ #_ %
1601  | #addr #abs destruct(abs) ]
1602qed.
1603
1604(*(*CSC: move elsewhere*)
1605lemma assoc_list_exists_true_to_assoc_list_lookup_Some:
1606  ∀A, B: Type[0].
1607  ∀e: A.
1608  ∀the_list: list (A × B).
1609  ∀eq_f: A → A → bool.
1610    assoc_list_exists A B e eq_f the_list = true →
1611      ∃e'. assoc_list_lookup A B e eq_f the_list = Some … e'.
1612  #A #B #e #the_list #eq_f elim the_list
1613  [1:
1614    whd in ⊢ (??%? → ?); #absurd destruct(absurd)
1615  |2:
1616    #hd #tl #inductive_hypothesis
1617    whd in ⊢ (??%? → ?); whd in match (assoc_list_lookup ?????);
1618    cases (eq_f (\fst hd) e) normalize nodelta
1619    [1:
1620      #_ %{(\snd hd)} %
1621    |2:
1622      @inductive_hypothesis
1623    ]
1624  ]
1625qed.
1626
1627(*CSC: move elsewhere*)
1628lemma assoc_list_exists_false_to_assoc_list_lookup_None:
1629  ∀A, B: Type[0].
1630  ∀e, e': A.
1631  ∀the_list, the_list': list (A × B).
1632  ∀eq_f: A → A → bool.
1633    e = e' →
1634    the_list = the_list' →
1635      assoc_list_exists A B e eq_f the_list = false →
1636        assoc_list_lookup A B e' eq_f the_list' = None ….
1637  #A #B #e #e' #the_list elim the_list
1638  [1:
1639    #the_list' #eq_f #e_refl <e_refl #the_list_refl <the_list_refl #_ %
1640  |2:
1641    #hd #tl #inductive_hypothesis #the_list' #eq_f #e_refl #the_list_refl <the_list_refl
1642    whd in ⊢ (??%? → ??%?); <e_refl
1643    cases (eq_f (\fst hd) e) normalize nodelta
1644    [1:
1645      #absurd destruct(absurd)
1646    |2:
1647      >e_refl in ⊢ (? → %); @inductive_hypothesis try % assumption
1648    ]
1649  ]
1650qed.*)
1651
1652lemma sfr_psw_eq_to_bit_address_of_register_eq:
1653  ∀A: Type[0].
1654  ∀code_memory: A.
1655  ∀status, status', register_address.
1656    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
1657      bit_address_of_register A code_memory status register_address = bit_address_of_register A code_memory status' register_address.
1658  #A #code_memory #status #status' #register_address #sfr_psw_refl
1659  whd in match bit_address_of_register; normalize nodelta
1660  <sfr_psw_refl %
1661qed.
1662
1663lemma sfr_psw_and_low_internal_ram_eq_to_get_register_eq:
1664  ∀A: Type[0].
1665  ∀code_memory: A.
1666  ∀status, status', register_address.
1667    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
1668      low_internal_ram A code_memory status = low_internal_ram A code_memory status' →
1669        get_register A code_memory status register_address = get_register A code_memory status' register_address.
1670  #A #code_memory #status #status' #register_address #sfr_psw_refl #low_internal_ram_refl
1671  whd in match get_register; normalize nodelta <low_internal_ram_refl
1672  >(sfr_psw_eq_to_bit_address_of_register_eq … status status') //
1673qed.
1674
1675lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr:
1676  ∀M, cm, status, status', sigma.
1677  ∀addr1: [[acc_a; registr; direct; indirect; data; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)
1678    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
1679    assert_data pseudo_assembly_program M cm status addr1 = true →
1680    map_address_mode_using_internal_pseudo_address_map_ok1 M cm status' sigma addr1.
1681  * * #low #high #accA #cm #status #status' #sigma #addr1 #sfr_refl
1682  @(subaddressing_mode_elim … addr1) try (#w #_ @I) [1,4: #_ @I ] #w
1683  whd in ⊢ (??%? → %); whd in match (data_or_address ?????);
1684  whd in match exists; normalize nodelta
1685  <(sfr_psw_eq_to_bit_address_of_register_eq … status status') try assumption
1686  cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs)
1687qed.
1688
1689lemma sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map:
1690  ∀M.
1691  ∀sigma.
1692  ∀sfr8051.
1693  ∀b.
1694    sfr8051 ≠ SFR_ACC_A →
1695      map_address_using_internal_pseudo_address_map M sigma sfr8051 b = b.
1696  #M #sigma * #b
1697  [18:
1698    #relevant cases (absurd … (refl ??) relevant)
1699  ]
1700  #_ %
1701qed.
1702
1703lemma w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map:
1704  ∀M.
1705  ∀sigma: Word → Word.
1706  ∀w: BitVector 8.
1707  ∀b.
1708    w ≠ bitvector_of_nat … 224 →
1709      map_address_Byte_using_internal_pseudo_address_map M sigma w b = b.
1710  #M #sigma #w #b #w_neq_assm
1711  whd in ⊢ (??%?); inversion (sfr_of_Byte ?)
1712  [1:
1713    #sfr_of_Byte_refl %
1714  |2:
1715    * #sfr8051 #sfr_of_Byte_refl normalize nodelta try %
1716    @sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map %
1717    #relevant >relevant in sfr_of_Byte_refl; #sfr_of_Byte_refl
1718    @(absurd ?? w_neq_assm)
1719    lapply sfr_of_Byte_refl -b -sfr_of_Byte_refl -relevant -w_neq_assm -sfr8051 -sigma
1720    whd in match sfr_of_Byte; normalize nodelta
1721    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1722    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1723    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1724    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1725    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1726    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1727    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1728    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1729    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1730    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1731    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1732    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1733    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1734    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1735    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1736    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1737    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1738    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1739    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1740    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1741    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1742    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1743    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1744    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1745    @eqb_elim #eqb_refl normalize nodelta [1: #_ <eqb_refl >bitvector_of_nat_inverse_nat_of_bitvector % ]
1746    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
1747    #absurd destruct(absurd)
1748qed.
1749
1750(*lemma assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map:
1751  ∀M, sigma, w, b.
1752    assoc_list_exists Byte (upper_lower×Word) w (eq_bv 8) (\fst  M) = false →
1753      map_internal_ram_address_using_pseudo_address_map M sigma w b = b.
1754  #M #sigma #w #b #assoc_list_exists_assm
1755  whd in ⊢ (??%?);
1756  >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm) %
1757qed.*)
1758   
1759lemma addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2:
1760  ∀M', cm.
1761  ∀sigma, status, status', b, b'.
1762  ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)
1763    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
1764    low_internal_ram pseudo_assembly_program cm status = low_internal_ram pseudo_assembly_program cm status' →
1765    b = b' →
1766    assert_data pseudo_assembly_program M' cm status addr1 = true →
1767      map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status' addr1 b = b'.
1768  #M' #cm #sigma #status #status' #b #b' #addr1 #sfr_refl #low_internal_ram_refl #b_refl <b_refl
1769  @(subaddressing_mode_elim … addr1)
1770  [1:
1771    whd in ⊢ (??%? → ??%?); cases M' -M' * #low #high *
1772    [1:
1773      normalize nodelta #_ %
1774    |2:
1775      * #upper_lower #address normalize nodelta #absurd destruct(absurd)
1776    ]
1777  |2: cases M' -M' * #low #high #accA
1778    #w whd in ⊢ (??%? → ??%?); whd in match (lookup_from_internal_ram ??);
1779    <(sfr_psw_eq_to_bit_address_of_register_eq … status status' w … sfr_refl)
1780    cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs)
1781  |4: cases M' -M' * #low #high #accA
1782    #w whd in ⊢ (??%? → ??%?); whd in match lookup_from_internal_ram;
1783    whd in match data_or_address; normalize nodelta whd in match exists; normalize nodelta
1784    whd in match get_register; normalize nodelta
1785    <(sfr_psw_eq_to_bit_address_of_register_eq … status status' … sfr_refl)
1786    cases (lookup_opt ????) normalize nodelta [2: #_ #abs destruct(abs)]
1787    <low_internal_ram_refl @vsplit_elim #one #seven #EQone_seven normalize nodelta
1788    cases (head' bool ??) normalize nodelta cases (lookup_opt ????) normalize nodelta
1789    #x try % #abs destruct(abs)
1790  |3: cases M' -M' * #low #high #accA
1791    #w whd in ⊢ (??%? → ??%?); whd in match data_or_address; normalize nodelta
1792    @vsplit_elim #hd #tl #w_refl normalize nodelta
1793    lapply (eq_head' ?? … hd) >(Vector_O … (tail … hd))
1794    cases (head' bool ??) normalize nodelta
1795    [2: #_ whd in match (map_internal_ram_address_using_pseudo_address_map ????);
1796        whd in match (lookup_from_internal_ram ??); cases (lookup_opt ????);
1797        normalize nodelta // #x #abs destruct(abs) ] #EQhd
1798    >w_refl >EQhd @eq_bv_elim #eq_bv_refl normalize nodelta
1799    [1: cases accA normalize nodelta try (#x #abs destruct(abs)) #_
1800        normalize in eq_bv_refl; >eq_bv_refl %
1801    |2: #_ @w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map assumption ]
1802  |5,6,7,8:
1803    #w try #w' %
1804  ]
1805qed.
1806
1807(*CSC: move elsewhere*)
1808lemma bv_append_eq_to_eq:
1809 ∀A,n. ∀v1,v2: Vector A n. ∀m. ∀v3,v4: Vector A m.
1810  v1@@v3 = v2@@v4 → v1=v2 ∧ v3=v4.
1811 #A #n #v1 elim v1
1812 [ #v2 >(Vector_O … v2) #m #v3 #v4 normalize * %%
1813 | #n' #hd1 #tl1 #IH #v2 cases (Vector_Sn … v2) #hd2 * #tl2 #EQ2 >EQ2
1814   #m #v3 #v4 #EQ normalize in EQ; destruct(EQ) cases (IH … e0) * * %% ]
1815qed.
1816
1817lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get:
1818  ∀M: internal_pseudo_address_map.
1819  ∀cm: pseudo_assembly_program.
1820  ∀s: PreStatus pseudo_assembly_program cm.
1821  ∀sigma: Word → Word.
1822  ∀addr: [[bit_addr]]. (* XXX: expand as needed *)
1823  ∀f: bool.
1824  assert_data pseudo_assembly_program M cm s addr = true →
1825    map_bit_address_mode_using_internal_pseudo_address_map_get M cm s sigma addr f.
1826  ** #low #high #accA #cm #s #sigma #addr #f
1827  @(subaddressing_mode_elim … addr) #w
1828  whd in ⊢ (??%? → %); whd in match data_or_address; normalize nodelta
1829  @vsplit_elim #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
1830  @vsplit_elim #four #three #four_three_refl normalize nodelta
1831  cases (head' bool ??) normalize nodelta
1832  [1: @eq_bv_elim normalize nodelta
1833      [1: #EQfour cases accA normalize nodelta #x [2: #abs destruct(abs)] >EQfour %
1834      |2: #NEQ #_ >w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map
1835          try % normalize #EQ @(absurd ?? NEQ)
1836          cases (bv_append_eq_to_eq … [[true]] [[true]] … EQ) #_ #EQ1
1837          cases (bv_append_eq_to_eq … four [[true;true;false;false]] … EQ1) // ]
1838  |2: whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
1839      whd in match lookup_from_internal_ram; normalize nodelta
1840      cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs) ]
1841qed.
1842
1843lemma special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051:
1844  ∀M: internal_pseudo_address_map.
1845  ∀cm: pseudo_assembly_program.
1846  ∀ps.
1847  ∀sigma: Word → Word.
1848  ∀policy: Word → bool.
1849  ∀sfr.
1850  ∀result: Byte.
1851    eqb (sfr_8051_index sfr) (sfr_8051_index SFR_ACC_A) = false →
1852      special_function_registers_8051 (BitVectorTrie Byte 16)
1853        (code_memory_of_pseudo_assembly_program cm sigma policy)
1854        (set_8051_sfr (BitVectorTrie Byte 16)
1855        (code_memory_of_pseudo_assembly_program cm sigma policy)
1856        (status_of_pseudo_status M cm ps sigma policy) sfr result) =
1857      sfr_8051_of_pseudo_sfr_8051 M
1858        (special_function_registers_8051 pseudo_assembly_program cm
1859        (set_8051_sfr pseudo_assembly_program cm ps sfr result)) sigma.
1860  ** #low #high * [2: * #upper_lower #addr] #cm #ps #sigma #policy #sfr #result #sfr_neq_assm
1861  whd in match (set_8051_sfr ?????);
1862  whd in match (special_function_registers_8051 ???);
1863  whd in match (sfr_8051_of_pseudo_sfr_8051 ???); normalize nodelta try %
1864  cases upper_lower normalize nodelta whd in match (set_8051_sfr ?????);
1865  >get_index_v_set_index_miss [2,4: @eqb_false_to_not_eq assumption]
1866  @vsplit_elim #h #l #h_l_refl normalize nodelta
1867  @set_index_set_index_commutation @eqb_false_to_not_eq assumption
1868qed.
1869
1870(*
1871lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1:
1872  ∀M: internal_pseudo_address_map.
1873  ∀cm: pseudo_assembly_program.
1874  ∀s, s': PreStatus pseudo_assembly_program cm.
1875  ∀sigma: Word → Word.
1876  ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *)
1877  ∀f: bool.
1878  s = s' →
1879  addressing_mode_ok pseudo_assembly_program M cm s addr = true →
1880    map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm s' sigma addr f.
1881  #M #cm #s #s' #sigma #addr #f #s_refl <s_refl
1882  @(subaddressing_mode_elim … addr) [1: #w ]
1883  whd in ⊢ (??%? → %); [2: #_ @I ]
1884  inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
1885  cases (head' bool ??) normalize nodelta
1886  [1:
1887    #eq_accumulator_assm whd in ⊢ (??%?);
1888    cases (sfr_of_Byte ?) try % * * try % normalize nodelta
1889    whd in ⊢ (??%?);
1890    >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %
1891  |2:
1892    #assoc_list_exists_assm whd in ⊢ (??%?);
1893    lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm
1894    whd in assoc_list_exists_assm:(???%);
1895    >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) %
1896  ]
1897qed.
1898
1899lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2:
1900  ∀M: internal_pseudo_address_map.
1901  ∀cm: pseudo_assembly_program.
1902  ∀s, s': PreStatus pseudo_assembly_program cm.
1903  ∀sigma: Word → Word.
1904  ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *)
1905  ∀f: bool.
1906  s = s' →
1907  addressing_mode_ok pseudo_assembly_program M cm s addr = true →
1908    map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm s' sigma addr f.
1909  #M #cm #s #s' #sigma #addr #f #s_refl <s_refl
1910  @(subaddressing_mode_elim … addr) [1: #w ]
1911  whd in ⊢ (??%? → %); [2: #_ @I ]
1912  inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
1913  cases (head' bool ??) normalize nodelta
1914  [1:
1915    #eq_accumulator_assm whd in ⊢ (??%?);
1916    cases (sfr_of_Byte ?) try % * * try % normalize nodelta
1917    whd in ⊢ (??%?);
1918    >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %
1919  |2:
1920    #assoc_list_exists_assm whd in ⊢ (??%?);
1921    lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm
1922    whd in assoc_list_exists_assm:(???%);
1923    >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) %
1924  ]
1925qed.*)
1926
1927(*
1928axiom insert_low_internal_ram_of_pseudo_low_internal_ram':
1929  ∀M, M', sigma,cm,s,addr,v,v'.
1930    (∀addr'.
1931      ((false:::addr) = addr' →
1932        map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v =
1933        map_internal_ram_address_using_pseudo_address_map M' sigma (false:::addr) v') ∧
1934      ((false:::addr) ≠ addr' →
1935        let 〈callM, accM〉 ≝ M in
1936        let 〈callM', accM'〉 ≝ M' in
1937          accM = accM' ∧
1938            assoc_list_lookup … addr' (eq_bv 8) … callM =
1939              assoc_list_lookup … addr' (eq_bv 8) … callM')) →
1940    insert Byte 7 addr v'
1941      (low_internal_ram_of_pseudo_low_internal_ram M'
1942      (low_internal_ram pseudo_assembly_program cm s)) =
1943    low_internal_ram_of_pseudo_low_internal_ram M
1944      (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
1945*)
1946
1947(*
1948lemma write_at_stack_pointer_status_of_pseudo_status:
1949  ∀M, M'.
1950  ∀cm.
1951  ∀sigma.
1952  ∀policy.
1953  ∀s, s'.
1954  ∀new_b, new_b'.
1955    map_internal_ram_address_using_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_SP) new_b = new_b' →
1956    status_of_pseudo_status M cm s sigma policy = s' →
1957    write_at_stack_pointer ?? s' new_b' =
1958    status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s new_b) sigma policy.
1959  #M #M' #cm #sigma #policy #s #s' #new_b #new_b'
1960  #new_b_refl #s_refl <new_b_refl <s_refl
1961  whd in match write_at_stack_pointer; normalize nodelta
1962  @pair_elim #nu #nl #nu_nl_refl normalize nodelta
1963  @(pair_replace ?????????? (eq_to_jmeq … nu_nl_refl))
1964  [1:
1965    @eq_f
1966    whd in match get_8051_sfr; normalize nodelta
1967    whd in match sfr_8051_index; normalize nodelta
1968    whd in match status_of_pseudo_status; normalize nodelta
1969    whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
1970    cases (\snd M) [2: * #address ] normalize nodelta
1971    [1,2:
1972      cases (vsplit bool ???) #high #low normalize nodelta
1973      whd in match sfr_8051_index; normalize nodelta
1974      >get_index_v_set_index_miss %
1975      #absurd destruct(absurd)
1976    |3:
1977      %
1978    ]
1979  |2:
1980    @if_then_else_status_of_pseudo_status try %
1981    [2:
1982      @sym_eq <set_low_internal_ram_status_of_pseudo_status
1983      [1:
1984        @eq_f2
1985        [2:
1986          @insert_low_internal_ram_of_pseudo_low_internal_ram'
1987    @sym_eq
1988    [2:
1989      <set_low_internal_ram_status_of_pseudo_status
1990      [1:
1991        @eq_f2
1992        [2:
1993          @sym_eq
1994          >(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma … new_b')
1995          [2:
1996            >new_b_refl
1997    ]
1998  ]
1999qed.*)
Note: See TracBrowser for help on using the repository browser.