source: src/ASM/Test.ma @ 2672

Last change on this file since 2672 was 2284, checked in by sacerdot, 8 years ago

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