source: src/ASM/Test.ma @ 2187

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

Work from today on the big proof.

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