source: src/ASM/Test.ma @ 2272

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

Changed proof strategy for main lemma after noticed that the current approach would not work with POP, RET, etc. Ported throughout the assembly proof and all the way up to Test.ma.

File size: 63.2 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
303(*
304lemma get_index_v_status_of_pseudo_status:
305  ∀M, code_memory, sigma, policy, s, s', sfr.
306    map_address_using_internal_pseudo_address_map M sigma sfr
307      (get_index_v Byte 19
308        (special_function_registers_8051 pseudo_assembly_program code_memory s)
309        (sfr_8051_index sfr) (sfr8051_index_19 sfr)) = s' →
310    get_index_v Byte 19
311      (special_function_registers_8051 (BitVectorTrie Byte 16)
312      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
313      (status_of_pseudo_status M code_memory s sigma policy))
314      (sfr_8051_index sfr) (sfr8051_index_19 sfr) = s'.
315  #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl
316  whd in match status_of_pseudo_status; normalize nodelta
317  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
318  inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta
319 [1:
320    cases sfr
321    [18:
322      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
323      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
324      >sndM_refl %
325    ]
326    %
327  |2:
328    @pair_elim #high #low #high_low_refl normalize nodelta
329    inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
330    cases sfr
331    [18,37:
332      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
333      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
334      >sndM_refl normalize nodelta >high_low_refl normalize nodelta
335      >eq_upper_lower_refl normalize nodelta
336      whd in match (set_8051_sfr ?????); //
337    ]
338    @get_index_v_set_index_miss whd in ⊢ (?(??%%));
339    @nmk #absurd destruct(absurd)
340  ]
341qed.
342*)
343
344lemma set_8051_sfr_status_of_pseudo_status:
345  ∀M, code_memory, sigma, policy, s, s', sfr, v,v'.
346    status_of_pseudo_status M code_memory s sigma policy = s' →
347    map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
348      set_8051_sfr ? (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v' =
349      status_of_pseudo_status M code_memory
350        (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy.
351  #M #code_memory #sigma #policy #s #s' #sfr #v #v' #s_ok #v_ok
352  <s_ok whd in ⊢ (??%%); @split_eq_status try % /2/
353qed.
354
355(*
356lemma get_8051_sfr_status_of_pseudo_status:
357  ∀M, code_memory, sigma, policy, s, s', s'', sfr.
358    status_of_pseudo_status M code_memory s sigma policy = s' →
359    map_address_using_internal_pseudo_address_map M sigma sfr
360     (get_8051_sfr pseudo_assembly_program code_memory s sfr) = s'' →
361  get_8051_sfr (BitVectorTrie Byte 16)
362    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
363     s' sfr = s''.
364  #M #code_memory #sigma #policy #s #s' #s'' #sfr #s_refl #s_refl' <s_refl <s_refl'
365  whd in match get_8051_sfr; normalize nodelta
366  @get_index_v_status_of_pseudo_status %
367qed.*)
368
369lemma get_8052_sfr_status_of_pseudo_status:
370  ∀M, code_memory, sigma, policy, s, s', sfr.
371  status_of_pseudo_status M code_memory s sigma policy = s' →
372  (get_8052_sfr (BitVectorTrie Byte 16)
373    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
374    s' sfr =
375   (get_8052_sfr pseudo_assembly_program code_memory s sfr)).
376  #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl //
377qed.
378
379lemma set_8052_sfr_status_of_pseudo_status:
380  ∀M, code_memory, sigma, policy, s, s', sfr, v.
381  status_of_pseudo_status M code_memory s sigma policy = s' →
382    (set_8052_sfr (BitVectorTrie Byte 16)
383      (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v =
384    status_of_pseudo_status M code_memory
385     (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
386  #M #code_memory #sigma #policy #s #s' #sfr #v #s_refl <s_refl //
387qed.
388 
389definition map_address_Byte_using_internal_pseudo_address_map ≝
390 λM,sigma,d,v.
391  match sfr_of_Byte d with
392  [ None ⇒ v
393  | Some sfr8051_8052 ⇒
394    match sfr8051_8052 with
395    [ inl sfr ⇒
396      map_address_using_internal_pseudo_address_map M sigma sfr v
397    | inr _ ⇒ v
398    ]
399  ].
400
401lemma set_bit_addressable_sfr_status_of_pseudo_status':
402  let M ≝ pseudo_assembly_program in
403    ∀code_memory: M.
404    ∀s: PreStatus M code_memory.
405    ∀d: Byte.
406    ∀v: Byte.
407      Σp: PreStatus M code_memory.
408        ∀M.
409        ∀sigma.
410        ∀policy.
411        ∀s'.
412        ∀v'.
413          status_of_pseudo_status M code_memory s sigma policy = s' →
414            map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
415              (set_bit_addressable_sfr (BitVectorTrie Byte 16)
416                (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' d v' =
417              status_of_pseudo_status M code_memory
418                (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
419  whd in match map_address_Byte_using_internal_pseudo_address_map;
420  whd in match set_bit_addressable_sfr;
421  normalize nodelta
422  @(let M ≝ pseudo_assembly_program in
423  λcode_memory:M.
424  λs: PreStatus M code_memory.
425  λb: Byte.
426  λv: Byte.
427   match sfr_of_Byte b with
428   [ None ⇒ match not_implemented in False with [ ]
429   | Some sfr8051_8052 ⇒
430      match sfr8051_8052 with
431      [ inl sfr ⇒
432         match sfr with
433         [ SFR_P1 ⇒
434           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
435           set_p1_latch ?? s v
436         | SFR_P3 ⇒
437           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
438           set_p3_latch ?? s v
439         | _ ⇒ set_8051_sfr ?? s sfr v ]
440      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]])
441  normalize nodelta #M #sigma #policy #s' #v' #s_refl <s_refl
442  /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/
443  whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
444  #v_refl >v_refl //
445qed.
446
447lemma set_bit_addressable_sfr_status_of_pseudo_status:
448 ∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte.
449  ∀M. ∀sigma. ∀policy. ∀s': Status ?. ∀v'.
450  status_of_pseudo_status M code_memory s sigma policy = s' →
451  map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
452 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
453  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
454  s' d v'
455  =status_of_pseudo_status M code_memory
456   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
457 #code #s #d #v cases (set_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_
458 #H @H
459qed.
460
461lemma set_low_internal_ram_status_of_pseudo_status:
462 ∀cm,sigma,policy,M,s,s',ram.
463  status_of_pseudo_status M cm s sigma policy = s' →
464  set_low_internal_ram (BitVectorTrie Byte 16)
465  (code_memory_of_pseudo_assembly_program cm sigma policy)
466  s'
467  (low_internal_ram_of_pseudo_low_internal_ram M sigma ram)
468  = status_of_pseudo_status M cm
469    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
470  #cm #sigma #policy #M #s #s' #ram #s_refl <s_refl //
471qed.
472
473(* Real axiom ATM *)
474axiom insert_low_internal_ram_of_pseudo_low_internal_ram:
475 ∀M,sigma,cm,s,addr,v,v'.
476 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
477  insert Byte 7 addr v'
478  (low_internal_ram_of_pseudo_low_internal_ram M sigma
479   (low_internal_ram pseudo_assembly_program cm s))
480  =low_internal_ram_of_pseudo_low_internal_ram M sigma
481   (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
482               
483lemma insert_low_internal_ram_status_of_pseudo_status:
484 ∀M,cm,sigma,policy,s,addr,v,v'.
485 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
486  insert Byte 7 addr v'
487   (low_internal_ram (BitVectorTrie Byte 16)
488    (code_memory_of_pseudo_assembly_program cm sigma policy)
489    (status_of_pseudo_status M cm s sigma policy))
490  = low_internal_ram_of_pseudo_low_internal_ram M sigma
491     (insert Byte 7 addr v
492      (low_internal_ram pseudo_assembly_program cm s)).
493 /2 by insert_low_internal_ram_of_pseudo_low_internal_ram/
494qed.
495
496(* Real axiom ATM *)
497axiom insert_high_internal_ram_of_pseudo_high_internal_ram:
498 ∀M,sigma,cm,s,addr,v,v'.
499 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
500  insert Byte 7 addr v'
501  (high_internal_ram_of_pseudo_high_internal_ram M sigma
502   (high_internal_ram pseudo_assembly_program cm s))
503  =high_internal_ram_of_pseudo_high_internal_ram M sigma
504   (insert Byte 7 addr v (high_internal_ram pseudo_assembly_program cm s)).
505
506lemma insert_high_internal_ram_status_of_pseudo_status:
507 ∀M,cm,sigma,policy,s,addr,v,v'.
508 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
509  insert Byte 7 addr v'
510   (high_internal_ram (BitVectorTrie Byte 16)
511    (code_memory_of_pseudo_assembly_program cm sigma policy)
512    (status_of_pseudo_status M cm s sigma policy))
513  = high_internal_ram_of_pseudo_high_internal_ram M sigma
514     (insert Byte 7 addr v
515      (high_internal_ram pseudo_assembly_program cm s)).
516 /2 by insert_high_internal_ram_of_pseudo_high_internal_ram/
517qed.
518
519lemma bit_address_of_register_status_of_pseudo_status:
520 ∀M,cm,s,sigma,policy,r.
521  bit_address_of_register …
522  (code_memory_of_pseudo_assembly_program cm sigma policy)
523  (status_of_pseudo_status M cm s sigma policy) r =
524  bit_address_of_register … cm s r.
525 #M #cm #s #sigma #policy #r whd in ⊢ (??%%);
526 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
527 @pair_elim #un #ln #_
528 @pair_elim #r1 #r0 #_ %
529qed.
530
531(*CSC: provable using the axiom in AssemblyProof, but this one seems more
532  primitive *)
533axiom lookup_low_internal_ram_of_pseudo_low_internal_ram:
534 ∀M,sigma,cm,s,s',addr.
535  map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr)
536  (lookup Byte 7 addr
537   (low_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' →
538  lookup Byte 7 addr
539  (low_internal_ram_of_pseudo_low_internal_ram M
540   (low_internal_ram pseudo_assembly_program cm s)) (zero 8)
541  = s'.
542
543(*CSC: provable using the axiom in AssemblyProof, but this one seems more
544  primitive *)
545axiom lookup_high_internal_ram_of_pseudo_high_internal_ram:
546 ∀M,sigma,cm,s,s',addr.
547  map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr)
548  (lookup Byte 7 addr
549   (high_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' →
550  lookup Byte 7 addr
551  (high_internal_ram_of_pseudo_high_internal_ram M
552   (high_internal_ram pseudo_assembly_program cm s)) (zero 8)
553  = s'.
554
555lemma get_register_status_of_pseudo_status:
556 ∀M,cm,sigma,policy,s,s',s'',r.
557  status_of_pseudo_status M cm s sigma policy = s' →
558  map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r)
559   (get_register … cm s r) = s'' →
560  get_register …
561   (code_memory_of_pseudo_assembly_program cm sigma policy)
562   s' r = s''.
563 #M #cm #sigma #policy #s #s' #s'' #r #s_refl #s_refl' <s_refl <s_refl'
564 whd in match get_register; normalize nodelta
565 whd in match status_of_pseudo_status; normalize nodelta
566 >bit_address_of_register_status_of_pseudo_status
567 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … (refl …))
568qed.
569
570lemma external_ram_status_of_pseudo_status:
571 ∀M,cm,s,sigma,policy.
572  external_ram …
573   (code_memory_of_pseudo_assembly_program cm sigma policy)
574   (status_of_pseudo_status M cm s sigma policy) =
575  external_ram … cm s.
576 //
577qed.
578
579lemma set_external_ram_status_of_pseudo_status:
580  ∀M,cm,ps,sigma,policy,ram.
581    set_external_ram …
582      (code_memory_of_pseudo_assembly_program cm sigma policy)
583      (status_of_pseudo_status M cm ps sigma policy)
584      ram =
585    status_of_pseudo_status M cm (set_external_ram … cm ps ram) sigma policy.
586  //
587qed.
588
589lemma set_register_status_of_pseudo_status:
590 ∀M,sigma,policy,cm,s,s',r,v,v'.
591  status_of_pseudo_status M cm s sigma policy = s' →
592  map_internal_ram_address_using_pseudo_address_map M sigma
593   (false:::bit_address_of_register pseudo_assembly_program cm s r) v =v' →
594  set_register (BitVectorTrie Byte 16)
595   (code_memory_of_pseudo_assembly_program cm sigma policy)
596   s' r v'
597  = status_of_pseudo_status M cm (set_register pseudo_assembly_program cm s r v)
598    sigma policy.
599  #M #sigma #policy #cm #s #s' #r #v #v' #s_refl <s_refl #v_ok
600 whd in match set_register; normalize nodelta
601 >bit_address_of_register_status_of_pseudo_status
602 >(insert_low_internal_ram_status_of_pseudo_status … v_ok)
603 @set_low_internal_ram_status_of_pseudo_status %
604qed.
605
606definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝
607 λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λsigma. λaddr.
608  match addr with
609  [ INDIRECT i ⇒
610     assoc_list_lookup ??
611      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None …
612  | EXT_INDIRECT e ⇒
613     assoc_list_lookup ??
614      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None …
615  | ACC_DPTR ⇒
616    (* XXX: \snd M = None plus in the very rare case when we are trying to dereference a null (O) pointer
617            in the ACC_A *)
618      map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) =
619        get_8051_sfr … cm s SFR_ACC_A
620  | ACC_PC ⇒
621      (* XXX: as above *)
622      map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) =
623        get_8051_sfr … cm s SFR_ACC_A ∧ sigma (program_counter … s) = program_counter … s
624  | _ ⇒ True ].
625
626definition map_address_mode_using_internal_pseudo_address_map_ok2 ≝
627 λT,M,sigma,cm.λs:PreStatus T cm.λaddr,v.
628  match addr with
629  [ DIRECT d ⇒
630     let 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit … 1 7 d in
631     match head' … bit_one with
632     [ true ⇒
633      map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v
634     | false ⇒
635      map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ]
636  | INDIRECT i ⇒
637     let register ≝ get_register ?? s [[ false; false; i ]] in
638     map_internal_ram_address_using_pseudo_address_map M sigma register v
639  | REGISTER r ⇒
640     map_internal_ram_address_using_pseudo_address_map M sigma
641      (false:::bit_address_of_register … s r) v
642  | ACC_A ⇒
643     map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v
644  | _ ⇒ v ].
645
646(*CSC: move elsewhere*)
647lemma eq_head': ∀A,n,v. v = head' A n v ::: tail … v.
648 #A #n #v inversion v in ⊢ ?;
649 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) /2/
650 | #m #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ' >EQ' % ]
651qed.
652
653(*CSC: move elsewhere*)
654lemma tail_singleton: ∀A,v. tail A 0 v = [[]].
655 #A #v inversion v in ⊢ ?;
656 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) #H destruct(H)
657 | #n #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ1 >EQ1 normalize
658   /2 by jmeq_to_eq/
659 ]
660qed.
661
662(*CSC: move elsewhere*)
663lemma eq_cons_head_append:
664 ∀A,n.∀hd: Vector A 1. ∀tl: Vector A n.
665  head' A 0 hd:::tl = hd@@tl.
666 #A #n #hd #tl >(eq_head' … hd) >tail_singleton %
667qed.
668
669lemma set_arg_8_status_of_pseudo_status':
670  ∀cm.
671  ∀ps.
672  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
673  ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
674   status_of_pseudo_status M cm ps sigma policy = s' →
675   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
676   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
677    set_arg_8 (BitVectorTrie Byte 16)
678      (code_memory_of_pseudo_assembly_program cm sigma policy)
679      s' addr value' =
680    status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
681  whd in match set_arg_8; normalize nodelta
682  @(let m ≝ pseudo_assembly_program in λcm, s. λa: [[ direct ; indirect ; registr ;
683                                   acc_a ; acc_b ; ext_indirect ;
684                                   ext_indirect_dptr ]]. λv.
685    match a return λaddr. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
686                                                acc_a ; acc_b ; ext_indirect ;
687                                                ext_indirect_dptr ]] addr) →
688                   Σp.?
689            with
690      [ DIRECT d ⇒
691        λdirect: True.
692          deplet 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit ? 1 7 d in
693            match head' … bit_one with
694              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
695              | false ⇒
696                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
697                  set_low_internal_ram ?? s memory
698              ]
699      | INDIRECT i ⇒
700        λindirect: True.
701          let register ≝ get_register ?? s [[ false; false; i ]] in
702          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
703            match head' … bit_one with
704              [ false ⇒
705                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
706                  set_low_internal_ram ?? s memory
707              | true ⇒
708                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
709                  set_high_internal_ram ?? s memory
710              ]
711      | REGISTER r ⇒ λregister: True. set_register ?? s r v
712      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
713      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
714      | EXT_INDIRECT e ⇒
715        λext_indirect: True.
716          let address ≝ get_register ?? s [[ false; false; e ]] in
717          let padded_address ≝ pad 8 8 address in
718          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
719            set_external_ram ?? s memory
720      | EXT_INDIRECT_DPTR ⇒
721        λext_indirect_dptr: True.
722          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
723          let memory ≝ insert ? 16 address v (external_ram ?? s) in
724            set_external_ram ?? s memory
725      | _ ⇒
726        λother: False.
727          match other in False with [ ]
728      ] (subaddressing_modein … a)) normalize nodelta
729  #M #sigma #policy #s' #v' #s_refl <s_refl
730  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
731  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
732  [1,2:
733    <vsplit_refl normalize nodelta >p normalize nodelta
734    [ >(vsplit_ok … vsplit_refl) #_ @set_bit_addressable_sfr_status_of_pseudo_status
735    | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
736  |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p;
737      >(get_register_status_of_pseudo_status … (refl …) (refl …))
738      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
739      >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
740      [ >(insert_high_internal_ram_status_of_pseudo_status … v)
741      | >(insert_low_internal_ram_status_of_pseudo_status … v) ]
742      // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
743  |5: #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) (refl …))
744      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
745      >EQ1 normalize nodelta
746      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status
747  |6: #EQ1 #EQ2 <EQ2 /2 by set_register_status_of_pseudo_status/
748  |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/
749  |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
750  |9: #_ #EQ <EQ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
751      >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
752      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] %
753qed.
754
755lemma set_arg_8_status_of_pseudo_status:
756  ∀cm.
757  ∀ps.
758  ∀addr, addr':[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
759  ∀value.
760  ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
761   addr = addr' →
762   status_of_pseudo_status M cm ps sigma policy = s' →
763   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
764   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
765    set_arg_8 (BitVectorTrie Byte 16)
766      (code_memory_of_pseudo_assembly_program cm sigma policy)
767      s' addr value' =
768    status_of_pseudo_status M cm (set_arg_8 … cm ps addr' value) sigma policy.
769  #cm #ps #addr #addr' #value
770  cases (set_arg_8_status_of_pseudo_status' cm ps addr value) #_ #relevant
771  #M #sigma #policy #s' #value' #addr_refl <addr_refl
772  @relevant
773qed.
774
775lemma p1_latch_status_of_pseudo_status:
776    ∀M.
777    ∀sigma.
778    ∀policy.
779    ∀code_memory: pseudo_assembly_program.
780    ∀s: PreStatus … code_memory.
781    ∀s'.
782    (status_of_pseudo_status M code_memory s sigma policy) = s' →
783    (p1_latch (BitVectorTrie Byte 16)
784      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
785      s' =
786    (p1_latch pseudo_assembly_program code_memory s)).
787  #M #sigma #policy #code_memory #s #s' #s_refl <s_refl //
788qed.
789
790lemma p3_latch_status_of_pseudo_status:
791    ∀M.
792    ∀sigma.
793    ∀policy.
794    ∀code_memory: pseudo_assembly_program.
795    ∀s: PreStatus … code_memory.
796    ∀s'.
797    (status_of_pseudo_status M code_memory s sigma policy) = s' →
798    (p3_latch (BitVectorTrie Byte 16)
799      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
800      (status_of_pseudo_status M code_memory s sigma policy) =
801    (p3_latch pseudo_assembly_program code_memory s)).
802  #M #sigma #policy #code_memory #s #s' #s_refl <s_refl //
803qed.
804
805lemma get_bit_addressable_sfr_status_of_pseudo_status':
806  let M ≝ pseudo_assembly_program in
807    ∀code_memory: M.
808    ∀s: PreStatus M code_memory.
809    ∀d: Byte.
810    ∀l: bool.
811      Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'.
812        status_of_pseudo_status M code_memory s sigma policy = s' →
813        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
814          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
815          s' d l =
816        map_address_Byte_using_internal_pseudo_address_map M sigma
817         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)).
818  whd in match get_bit_addressable_sfr;
819  whd in match map_address_Byte_using_internal_pseudo_address_map;
820  normalize nodelta
821  @(let M ≝ pseudo_assembly_program in
822    λcode_memory:M.
823    λs: PreStatus M code_memory.
824    λb: Byte.
825    λl: bool.
826    match sfr_of_Byte b with
827    [ None ⇒ match not_implemented in False with [ ]
828    | Some sfr8051_8052 ⇒
829    match sfr8051_8052 with
830    [ inl sfr ⇒
831      match sfr with
832      [ SFR_P1 ⇒
833        if l then
834          p1_latch … s
835        else
836          get_8051_sfr … s SFR_P1
837      | SFR_P3 ⇒
838        if l then
839          p3_latch … s
840        else
841          get_8051_sfr … s SFR_P3
842      | _ ⇒ get_8051_sfr … s sfr
843      ]
844    | inr sfr ⇒ get_8052_sfr M code_memory s sfr
845    ]
846    ])
847  #M #sigma #policy #s' #s_refl <s_refl normalize nodelta
848  /2 by get_8051_sfr_status_of_pseudo_status, p1_latch_status_of_pseudo_status, p3_latch_status_of_pseudo_status/
849qed.
850
851lemma get_bit_addressable_sfr_status_of_pseudo_status:
852  let M ≝ pseudo_assembly_program in
853    ∀code_memory: M.
854    ∀s: PreStatus M code_memory.
855    ∀d: Byte.
856    ∀l: bool.
857    ∀M. ∀sigma. ∀policy. ∀s'. ∀s''.
858      map_address_Byte_using_internal_pseudo_address_map M sigma
859         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l) = s'' →
860      (status_of_pseudo_status M code_memory s sigma policy) = s' →
861        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
862          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
863          s' d l) = s''.
864 #code #s #d #v
865 cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ #relevant
866 #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl <s_refl' @relevant %
867qed.
868
869lemma program_counter_status_of_pseudo_status:
870    ∀M. ∀sigma: Word → Word. ∀policy.
871    ∀code_memory: pseudo_assembly_program.
872    ∀s: PreStatus ? code_memory.
873    ∀s'.
874    ∀s''.
875    sigma (program_counter … s) = s'' →
876    (status_of_pseudo_status M code_memory s sigma policy) = s' →
877      program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy)
878        s' = s''.
879  #M #sigma #policy #code_memory #s #s' #s'' #s_refl #s_refl' <s_refl <s_refl' //
880qed.
881
882lemma get_cy_flag_status_of_pseudo_status:
883  ∀M, cm, sigma, policy, s, s'.
884  (status_of_pseudo_status M cm s sigma policy) = s' →
885  (get_cy_flag (BitVectorTrie Byte 16)
886    (code_memory_of_pseudo_assembly_program cm sigma policy)
887    s' =
888  get_cy_flag pseudo_assembly_program cm s).
889  #M #cm #sigma #policy #s #s' #s_refl <s_refl
890  whd in match get_cy_flag; normalize nodelta
891  >(get_index_v_status_of_pseudo_status … (refl …)) %
892qed.
893
894lemma get_arg_8_status_of_pseudo_status':
895  ∀cm.
896  ∀ps.
897  ∀l.
898  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
899    Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'.
900      (status_of_pseudo_status M cm ps sigma policy) = s' →
901      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
902      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
903      s' l addr =
904      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr).
905  whd in match get_arg_8; normalize nodelta
906  @(let m ≝ pseudo_assembly_program in
907    λ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]].
908    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
909      [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
910      | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
911      | DATA d ⇒ λdata: True. d
912      | REGISTER r ⇒ λregister: True. get_register ?? s r
913      | EXT_INDIRECT_DPTR ⇒
914        λext_indirect_dptr: True.
915          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
916            lookup ? 16 address (external_ram ?? s) (zero 8)
917      | EXT_INDIRECT e ⇒
918        λext_indirect: True.
919          let address ≝ get_register ?? s [[ false; false; e ]]  in
920          let padded_address ≝ pad 8 8 address in
921            lookup ? 16 padded_address (external_ram ?? s) (zero 8)
922      | ACC_DPTR ⇒
923        λacc_dptr: True.
924          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
925          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
926          let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
927            lookup ? 16 address (external_ram ?? s) (zero 8)
928      | ACC_PC ⇒
929        λacc_pc: True.
930          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
931          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
932            lookup ? 16 address (external_ram ?? s) (zero 8)
933      | DIRECT d ⇒
934        λdirect: True.
935          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
936            match head' … hd with
937            [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
938            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
939            ]
940      | INDIRECT i ⇒
941        λindirect: True.
942          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
943            match head' … hd with
944            [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)
945            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
946            ]
947      | _ ⇒ λother: False.
948        match other in False with [ ]
949      ] (subaddressing_modein … a)) normalize nodelta
950  #M #sigma #policy #s' #s_refl <s_refl
951  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
952  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
953  [1:
954    #_ >p normalize nodelta >p1 normalize nodelta
955    @(get_bit_addressable_sfr_status_of_pseudo_status … (refl …)) %
956  |2:
957    #_>p normalize nodelta >p1 normalize nodelta
958    @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) %
959  |3,4:
960    #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …))
961    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
962    >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta
963    [1:
964      @(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma)
965    |2:
966      @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
967    ]
968    @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
969  |5:
970    #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …))
971    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
972    >assoc_list_assm normalize nodelta %
973  |6,7,8,9:
974    #_ /2 by refl, get_register_status_of_pseudo_status, get_index_v_status_of_pseudo_status/
975  |10:
976    #acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
977    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
978    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
979    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
980    >acc_a_assm >p normalize nodelta //
981  |11:
982    * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
983    >(program_counter_status_of_pseudo_status … (refl …) (refl …))
984    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
985    >sigma_assm >map_acc_a_assm >p normalize nodelta //
986  |12:
987    #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
988    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
989    >external_ram_status_of_pseudo_status //
990  ]
991qed.
992
993lemma get_arg_8_status_of_pseudo_status:
994  ∀cm.
995  ∀ps.
996  ∀l.
997  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
998  ∀M. ∀sigma. ∀policy. ∀s', s''.
999      (status_of_pseudo_status M cm ps sigma policy) = s' →
1000      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr) = s'' →
1001      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
1002      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1003      s' l addr = s''.
1004  #cm #ps #l #addr
1005  cases (get_arg_8_status_of_pseudo_status' cm ps l addr) #_ #relevant
1006  #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl'
1007  @relevant assumption
1008qed.
1009
1010lemma get_arg_16_status_of_pseudo_status:
1011  ∀cm.
1012  ∀ps.
1013  ∀addr: [[data16]].
1014  ∀M. ∀sigma. ∀policy. ∀s'.
1015    status_of_pseudo_status M cm ps sigma policy = s' →
1016      get_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1017      s' addr =
1018      (get_arg_16 … cm ps addr).
1019  #cm #ps #addr #M #sigma #policy #s' #s_refl <s_refl //
1020qed.
1021
1022lemma set_arg_16_status_of_pseudo_status:
1023  ∀cm.
1024  ∀ps.
1025  ∀addr,addr': [[dptr]].
1026  ∀v,v': Word.
1027  ∀M. ∀sigma. ∀policy. ∀s'.
1028    status_of_pseudo_status M cm ps sigma policy = s' →
1029    v=v' → addr=addr' →
1030      set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1031      s' v' addr' =
1032      status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy.
1033  #cm #ps #addr #addr' #v #v' #M #sigma #policy #s' #s_refl <s_refl #addr_refl
1034  <addr_refl #v_refl <v_refl
1035  @(subaddressing_mode_elim … addr)
1036  whd in match set_arg_16; normalize nodelta
1037  whd in match set_arg_16'; normalize nodelta
1038  @(vsplit_elim bool ???) #bu #bl #bu_bl_refl normalize nodelta
1039  @set_8051_sfr_status_of_pseudo_status try % @sym_eq
1040  @set_8051_sfr_status_of_pseudo_status %
1041qed.
1042
1043definition map_bit_address_mode_using_internal_pseudo_address_map_get ≝
1044 λM:internal_pseudo_address_map.λcm: pseudo_assembly_program.λs:PreStatus ? cm.λsigma: Word → Word. λaddr. λl.
1045  match addr with
1046  [ BIT_ADDR b ⇒
1047    let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1048    match head' … bit_1 with
1049    [ true ⇒
1050      let address ≝ nat_of_bitvector … seven_bits in
1051      let d ≝ address ÷ 8 in
1052      let m ≝ address mod 8 in
1053      let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1054        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
1055    | false ⇒
1056      let address ≝ nat_of_bitvector … seven_bits in
1057      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1058      let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1059        map_internal_ram_address_using_pseudo_address_map M sigma
1060          (false:::address') t = t
1061    ]
1062  | N_BIT_ADDR b ⇒
1063    let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1064    match head' … bit_1 with
1065    [ true ⇒
1066      let address ≝ nat_of_bitvector … seven_bits in
1067      let d ≝ address ÷ 8 in
1068      let m ≝ address mod 8 in
1069      let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1070        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
1071    | false ⇒
1072      let address ≝ nat_of_bitvector … seven_bits in
1073      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1074      let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1075        map_internal_ram_address_using_pseudo_address_map M sigma
1076          (false:::address') t = t
1077    ]
1078  | _ ⇒ True ].
1079
1080lemma get_arg_1_status_of_pseudo_status':
1081  ∀cm.
1082  ∀ps.
1083  ∀addr: [[bit_addr; n_bit_addr; carry]].
1084  ∀l.
1085    Σb: bool. ∀M. ∀sigma. ∀policy. ∀s'.
1086      status_of_pseudo_status M cm ps sigma policy = s' →
1087      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
1088      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1089      s' addr l =
1090      (get_arg_1 … cm ps addr l).
1091  whd in match get_arg_1; normalize nodelta
1092  @(let m ≝ pseudo_assembly_program in
1093    λcm: m. λs: PseudoStatus cm. λa:[[bit_addr; n_bit_addr; carry]]. λl.
1094    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
1095                                                 n_bit_addr ;
1096                                                 carry ]] x) → Σb: bool. ? with
1097      [ BIT_ADDR b ⇒
1098        λbit_addr: True.
1099        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
1100        match head' … bit_1 with
1101        [ true ⇒
1102          let address ≝ nat_of_bitvector … seven_bits in
1103          let d ≝ address ÷ 8 in
1104          let m ≝ address mod 8 in
1105          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1106          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
1107            get_index_v … sfr m ?
1108        | false ⇒
1109          let address ≝ nat_of_bitvector … seven_bits in
1110          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1111          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1112            get_index_v … t (modulus address 8) ?
1113        ]
1114      | N_BIT_ADDR n ⇒
1115        λn_bit_addr: True.
1116        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
1117        match head' … bit_1 with
1118        [ true ⇒
1119          let address ≝ nat_of_bitvector … seven_bits in
1120          let d ≝ address ÷ 8 in
1121          let m ≝ address mod 8 in
1122          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1123          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
1124            ¬(get_index_v … sfr m ?)
1125        | false ⇒
1126          let address ≝ nat_of_bitvector … seven_bits in
1127          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1128          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
1129            ¬(get_index_v … t (modulus address 8) ?)
1130        ]
1131      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
1132      | _ ⇒ λother.
1133        match other in False with [ ]
1134      ] (subaddressing_modein … a)) normalize nodelta
1135  try @modulus_less_than
1136  #M #sigma #policy #s' #s_refl <s_refl
1137  [1:
1138    #_ >(get_cy_flag_status_of_pseudo_status … (refl …)) %
1139  |2,4:
1140    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
1141    >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …)) #map_address_assm
1142    >map_address_assm %
1143  |3,5:
1144    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
1145    whd in match status_of_pseudo_status; normalize nodelta
1146    >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …))
1147    #map_address_assm >map_address_assm %
1148  ]
1149qed.
1150
1151lemma get_arg_1_status_of_pseudo_status:
1152  ∀cm.
1153  ∀ps.
1154  ∀addr, addr': [[bit_addr; n_bit_addr; carry]].
1155  ∀l.
1156  ∀M. ∀sigma. ∀policy. ∀s'.
1157    addr = addr' →
1158    status_of_pseudo_status M cm ps sigma policy = s' →
1159      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
1160      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
1161      s' addr l =
1162      (get_arg_1 … cm ps addr' l).
1163  #cm #ps #addr #addr' #l
1164  cases (get_arg_1_status_of_pseudo_status' cm ps addr l) #_ #assm
1165  #M #sigma #policy #s' #addr_refl <addr_refl
1166  @assm
1167qed.
1168
1169definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝
1170  λM: internal_pseudo_address_map.
1171  λcm: pseudo_assembly_program.
1172  λs: PreStatus ? cm.
1173  λsigma: Word → Word.
1174  λaddr: [[bit_addr; carry]].
1175  λv: Bit.
1176  match addr with
1177  [ BIT_ADDR b ⇒
1178    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
1179    match head' … bit_1 with
1180    [ true ⇒
1181      let address ≝ nat_of_bitvector … seven_bits in
1182      let d ≝ address ÷ 8 in
1183      let m ≝ address mod 8 in
1184      let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1185      let sfr ≝ get_bit_addressable_sfr … s t true in
1186        map_address_Byte_using_internal_pseudo_address_map M sigma t sfr = sfr
1187    | false ⇒
1188      let address ≝ nat_of_bitvector … seven_bits in
1189      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1190      let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1191        map_internal_ram_address_using_pseudo_address_map M sigma
1192          (false:::address') t = t
1193    ]   
1194  | CARRY ⇒ True
1195  | _ ⇒ True
1196  ].
1197
1198definition map_bit_address_mode_using_internal_pseudo_address_map_set_2 ≝
1199  λM: internal_pseudo_address_map.
1200  λcm: pseudo_assembly_program.
1201  λs: PreStatus ? cm.
1202  λsigma: Word → Word.
1203  λaddr: [[bit_addr; carry]].
1204  λv: Bit.
1205  match addr with
1206  [ BIT_ADDR b ⇒
1207    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
1208    match head' … bit_1 with
1209    [ true ⇒
1210      let address ≝ nat_of_bitvector … seven_bits in
1211      let d ≝ address ÷ 8 in
1212      let m ≝ address mod 8 in
1213      let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1214      let sfr ≝ get_bit_addressable_sfr … s t true in
1215      let new_sfr ≝ set_index … sfr m v ? in
1216        map_address_Byte_using_internal_pseudo_address_map M sigma new_sfr t = t
1217    | false ⇒
1218      let address ≝ nat_of_bitvector … seven_bits in
1219      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1220      let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1221      let n_bit ≝ set_index … t (modulus address 8) v ? in
1222      let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
1223        map_internal_ram_address_using_pseudo_address_map M sigma
1224          (false:::address') n_bit = n_bit
1225    ]   
1226  | CARRY ⇒ True
1227  | _ ⇒ True
1228  ].
1229  @modulus_less_than
1230qed.
1231
1232lemma set_arg_1_status_of_pseudo_status':
1233  ∀cm: pseudo_assembly_program.
1234  ∀ps: PreStatus pseudo_assembly_program cm.
1235  ∀addr: [[bit_addr; carry]].
1236  ∀b: Bit.
1237    Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀b'.
1238      b = b' →
1239      status_of_pseudo_status M cm ps sigma policy = s' →
1240      map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
1241      map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b →
1242        set_arg_1 (BitVectorTrie Byte 16)
1243          (code_memory_of_pseudo_assembly_program cm sigma policy)
1244          s' addr b =
1245        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy.
1246  whd in match set_arg_1; normalize nodelta
1247  whd in ⊢ (? → ? → ? → ? → ??(λx.? → ? → ? → ? → ? → ? → ? → %?????? → %?????? → ?));
1248  normalize nodelta
1249  @(let m ≝ pseudo_assembly_program in
1250    λcm.
1251    λs: PreStatus m cm.
1252    λa: [[bit_addr; carry]].
1253    λv: Bit.
1254    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σp. ? with
1255      [ BIT_ADDR b ⇒ λbit_addr: True.
1256        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
1257        match head' … bit_1 with
1258        [ true ⇒
1259          let address ≝ nat_of_bitvector … seven_bits in
1260          let d ≝ address ÷ 8 in
1261          let m ≝ address mod 8 in
1262          let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1263          let sfr ≝ get_bit_addressable_sfr … s t true in
1264          let new_sfr ≝ set_index … sfr m v ? in
1265            set_bit_addressable_sfr … s new_sfr t
1266        | false ⇒
1267          let address ≝ nat_of_bitvector … seven_bits in
1268          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1269          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
1270          let n_bit ≝ set_index … t (modulus address 8) v ? in
1271          let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
1272            set_low_internal_ram … s memory
1273        ]
1274      | CARRY ⇒
1275        λcarry: True.
1276        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
1277        let new_psw ≝ v:::seven_bits in
1278          set_8051_sfr ?? s SFR_PSW new_psw
1279      | _ ⇒
1280        λother: False.
1281          match other in False with
1282            [ ]
1283      ] (subaddressing_modein … a)) normalize nodelta
1284  try @modulus_less_than #M #sigma #policy #s' #b' #b_refl <b_refl #s_refl <s_refl
1285  [1:
1286    #_ #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
1287    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
1288    >p normalize nodelta @set_8051_sfr_status_of_pseudo_status %
1289  |2,3:
1290    >p normalize nodelta >p1 normalize nodelta
1291    #map_bit_address_assm_1 #map_bit_address_assm_2
1292    [1:
1293      >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …))
1294      >map_bit_address_assm_1
1295      >(set_bit_addressable_sfr_status_of_pseudo_status cm s … map_bit_address_assm_2) %
1296    |2:
1297      whd in match status_of_pseudo_status in ⊢ (??(????%)?); normalize nodelta
1298      >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …))
1299      >map_bit_address_assm_1
1300      >(insert_low_internal_ram_of_pseudo_low_internal_ram … map_bit_address_assm_2)
1301      >set_low_internal_ram_status_of_pseudo_status in ⊢ (??%?); %
1302    ]
1303  ]
1304qed.
1305
1306lemma set_arg_1_status_of_pseudo_status:
1307  ∀cm: pseudo_assembly_program.
1308  ∀ps: PreStatus pseudo_assembly_program cm.
1309  ∀addr: [[bit_addr; carry]].
1310  ∀b: Bit.
1311  ∀M. ∀sigma. ∀policy. ∀s'. ∀b'.
1312      b = b' →
1313      status_of_pseudo_status M cm ps sigma policy = s' →
1314      map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
1315      map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b →
1316        set_arg_1 (BitVectorTrie Byte 16)
1317          (code_memory_of_pseudo_assembly_program cm sigma policy)
1318          s' addr b =
1319        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy.
1320  #cm #ps #addr #b
1321  cases (set_arg_1_status_of_pseudo_status' cm ps addr b) #_ #relevant
1322  @relevant
1323qed.
1324
1325lemma clock_status_of_pseudo_status:
1326 ∀M,cm,sigma,policy,s,s'.
1327  (status_of_pseudo_status M cm s sigma policy) = s' →
1328  clock …
1329   (code_memory_of_pseudo_assembly_program cm sigma policy)
1330   s'
1331  = clock … cm s.
1332  #M #cm #sigma #policy #s #s' #s_refl <s_refl //
1333qed.
1334
1335lemma set_clock_status_of_pseudo_status:
1336 ∀M,cm,sigma,policy,s,s',v,v'.
1337 status_of_pseudo_status M cm s sigma policy = s' →
1338 v = v' →
1339  set_clock …
1340   (code_memory_of_pseudo_assembly_program cm sigma policy)
1341   s' v
1342  = status_of_pseudo_status M cm (set_clock … cm s v') sigma policy.
1343  #M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl <s_refl <v_refl //
1344qed.
1345
1346lemma set_flags_status_of_pseudo_status:
1347  ∀M.
1348  ∀sigma.
1349  ∀policy.
1350  ∀code_memory: pseudo_assembly_program.
1351  ∀s: PreStatus ? code_memory.
1352  ∀s'.
1353  ∀b, b': Bit.
1354  ∀opt, opt': option Bit.
1355  ∀c, c': Bit.
1356    b = b' →
1357    opt = opt' →
1358    c = c' →
1359    status_of_pseudo_status M code_memory s sigma policy = s' →
1360      set_flags … s' b opt c =
1361        status_of_pseudo_status M code_memory (set_flags … code_memory s b' opt' c') sigma policy.
1362  #M #sigma #policy #code_memory #s #s' #b #b' #opt #opt' #c #c'
1363  #b_refl #opt_refl #c_refl <b_refl <opt_refl <c_refl #s_refl <s_refl
1364  whd in match status_of_pseudo_status; normalize nodelta
1365  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
1366  cases (\snd M)
1367  [1:
1368    normalize nodelta %
1369  |2:
1370    * #address normalize nodelta
1371    @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
1372    whd in ⊢ (??%%); cases opt try #opt' normalize nodelta
1373    @split_eq_status try % whd in match (sfr_8051_index ?);
1374    cases daemon
1375  ]
1376qed.
1377
1378lemma get_ac_flag_status_of_pseudo_status:
1379  ∀M: internal_pseudo_address_map.
1380  ∀sigma: Word → Word.
1381  ∀policy: Word → bool.
1382  ∀code_memory: pseudo_assembly_program.
1383  ∀s: PreStatus ? code_memory.
1384  ∀s'.
1385    status_of_pseudo_status M code_memory s sigma policy = s' →
1386      get_ac_flag ?? s' = get_ac_flag ? code_memory s.
1387  #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
1388  whd in match get_ac_flag; normalize nodelta
1389  whd in match status_of_pseudo_status; normalize nodelta
1390  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
1391  cases (\snd M) try %
1392  * normalize nodelta #address
1393  @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
1394  whd in match sfr_8051_index; normalize nodelta
1395  >get_index_v_set_index_miss [2,4: /2/] %
1396qed.
1397
1398lemma get_ov_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_ov_flag ?? s' = get_ov_flag ? code_memory s.
1407  #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
1408  whd in match get_ov_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 %
1412  * normalize nodelta #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_8051_sfr_status_of_pseudo_status:
1419  ∀M.
1420  ∀cm, ps, sigma, policy.
1421  ∀sfr.
1422    (sfr = SFR_ACC_A → \snd M = None …) →
1423    get_8051_sfr (BitVectorTrie Byte 16)
1424      (code_memory_of_pseudo_assembly_program cm sigma policy)
1425      (status_of_pseudo_status M cm ps sigma policy) sfr =
1426    get_8051_sfr pseudo_assembly_program cm ps sfr.
1427  #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant
1428  [18:
1429     >relevant %
1430  ]
1431  cases sndM try % * #address
1432  whd in match get_8051_sfr;
1433  whd in match status_of_pseudo_status; normalize nodelta
1434  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta #address
1435  cases (eq_upper_lower ??) normalize nodelta
1436  @pair_elim #upper #lower #upper_lower_refl
1437  @get_index_v_set_index_miss @nmk #relevant
1438  normalize in relevant; destruct(relevant)
1439qed.
1440
1441lemma get_arg_8_pseudo_addressing_mode_ok:
1442  ∀M: internal_pseudo_address_map.
1443  ∀cm: pseudo_assembly_program.
1444  ∀ps: PreStatus pseudo_assembly_program cm.
1445  ∀sigma: Word → Word.
1446  ∀policy: Word → bool.
1447  ∀addr1: [[registr; direct]].
1448    assert_data pseudo_assembly_program M cm ps addr1 = true →
1449      get_arg_8 (BitVectorTrie Byte 16)
1450        (code_memory_of_pseudo_assembly_program cm sigma policy)
1451        (status_of_pseudo_status M cm ps sigma policy) true addr1 =
1452      get_arg_8 pseudo_assembly_program cm ps true addr1.
1453  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1454  #M #cm #ps #sigma #policy #addr1
1455  @(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%);
1456  [1:
1457    whd in ⊢ (??%? → ??%?);
1458    whd in match bit_address_of_register; normalize nodelta
1459    @pair_elim #un #ln #un_ln_refl
1460    lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
1461    @(pair_replace ?????????? un_ln_refl)
1462    [1:
1463      whd in match get_8051_sfr; normalize nodelta
1464      whd in match sfr_8051_index; normalize nodelta
1465      @eq_f <get_index_v_special_function_registers_8051_not_acc_a
1466      try % #absurd destruct(absurd)
1467    |2:
1468      #assembly_mode_ok_refl
1469      >low_internal_ram_of_pseudo_internal_ram_miss
1470      [1:
1471        %
1472      |2:
1473        cases (data_or_address ?????) in assembly_mode_ok_refl; normalize nodelta
1474        [1:
1475          #absurd destruct(absurd)
1476        |2:
1477          * normalize nodelta
1478          [1:
1479          |2:
1480            #_ #absurd destruct(absurd)
1481          ]
1482        #absurd try % @sym_eq assumption
1483      ]
1484    ]
1485  |2:
1486    #addressing_mode_ok_refl whd in ⊢ (??%?);
1487    @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (*
1488    @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
1489    inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
1490    [1:
1491      whd in ⊢ (??%%); normalize nodelta
1492      cases (eqb ??) normalize nodelta [1: % ]
1493      cases (eqb ??) normalize nodelta [1: % ]
1494      cases (eqb ??) normalize nodelta [1: % ]
1495      cases (eqb ??) normalize nodelta [1: % ]
1496      cases (eqb ??) normalize nodelta [1:
1497        @get_8051_sfr_status_of_pseudo_status
1498        #absurd destruct(absurd)
1499      ]
1500      cases (eqb ??) normalize nodelta [1:
1501        @get_8051_sfr_status_of_pseudo_status
1502        #absurd destruct(absurd)
1503      ]
1504      cases (eqb ??) normalize nodelta [1:
1505        @get_8051_sfr_status_of_pseudo_status
1506        #absurd destruct(absurd)
1507      ]
1508      cases (eqb ??) normalize nodelta [1:
1509        @get_8051_sfr_status_of_pseudo_status
1510        #absurd destruct(absurd)
1511      ]
1512      cases (eqb ??) normalize nodelta [1:
1513        @get_8051_sfr_status_of_pseudo_status
1514        #absurd destruct(absurd)
1515      ]
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      cases (eqb ??) normalize nodelta [1: % ]
1521      cases (eqb ??) normalize nodelta [1:
1522        @get_8051_sfr_status_of_pseudo_status
1523        #absurd destruct(absurd)
1524      ]
1525      cases (eqb ??) normalize nodelta [1:
1526        @get_8051_sfr_status_of_pseudo_status
1527        #absurd destruct(absurd)
1528      ]
1529      cases (eqb ??) normalize nodelta [1:
1530        @get_8051_sfr_status_of_pseudo_status
1531        #absurd destruct(absurd)
1532      ]
1533      cases (eqb ??) normalize nodelta [1:
1534        @get_8051_sfr_status_of_pseudo_status
1535        #absurd destruct(absurd)
1536      ]
1537      cases (eqb ??) normalize nodelta [1:
1538        @get_8051_sfr_status_of_pseudo_status
1539        #absurd destruct(absurd)
1540      ]
1541      cases (eqb ??) normalize nodelta [1:
1542        @get_8051_sfr_status_of_pseudo_status
1543        #absurd destruct(absurd)
1544      ]
1545      cases (eqb ??) normalize nodelta [1:
1546        @get_8051_sfr_status_of_pseudo_status
1547        #absurd destruct(absurd)
1548      ]
1549      cases (eqb ??) normalize nodelta [1:
1550        @get_8051_sfr_status_of_pseudo_status
1551        #absurd destruct(absurd)
1552      ]
1553      cases (eqb ??) normalize nodelta [1:
1554        @get_8051_sfr_status_of_pseudo_status
1555        #absurd destruct(absurd)
1556      ]
1557      cases (eqb ??) normalize nodelta [1:
1558        @get_8051_sfr_status_of_pseudo_status
1559        #absurd destruct(absurd)
1560      ]
1561      inversion (eqb ??) #eqb_refl normalize nodelta [1:
1562        @get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl
1563        whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl)
1564        >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
1565        #assoc_list_assm cases (conjunction_true … assoc_list_assm) #_
1566        #relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) %
1567      ]
1568      cases (eqb ??) normalize nodelta [1:
1569        @get_8051_sfr_status_of_pseudo_status
1570        #absurd destruct(absurd)
1571      ] %
1572    |2:
1573      lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant
1574      whd in match status_of_pseudo_status; normalize nodelta
1575      >low_internal_ram_of_pseudo_internal_ram_miss try %
1576      cut(arg = false:::(three_bits@@nl))
1577      [1:
1578        <get_index_v_refl
1579        cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits)
1580        [1:
1581          cut(ignore = [[get_index_v bool 4 nu 0 ?]])
1582          [1:
1583            @le_S_S @le_O_n
1584          |2:
1585            cut(ignore = \fst (vsplit bool 1 3 nu))
1586            [1:
1587              >ignore_three_bits_refl %
1588            |2:
1589              #ignore_refl >ignore_refl
1590              cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl
1591              >nu_refl %
1592            ]
1593          |3:
1594            #ignore_refl >ignore_refl in ignore_three_bits_refl;
1595            #relevant lapply (vsplit_ok ?????? (sym_eq … relevant))
1596            #nu_refl <nu_refl %
1597          ]
1598        |2:
1599          #nu_refl change with (? = (?:::three_bits)@@?) <nu_refl
1600          @sym_eq @vsplit_ok >nu_nl_refl %
1601        ]
1602      |2:
1603        #arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant;
1604        normalize nodelta
1605        [1:
1606          cases (eq_bv ???) normalize #absurd destruct(absurd)
1607        |2:
1608          #_ %
1609        ]
1610      ]
1611    ]
1612  ] *)
1613qed.
Note: See TracBrowser for help on using the repository browser.