source: src/ASM/Test.ma @ 2244

Last change on this file since 2244 was 2207, checked in by mulligan, 9 years ago

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