source: src/ASM/Test.ma @ 2173

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

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