source: src/ASM/Test.ma @ 2274

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

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

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