source: src/ASM/Test.ma @ 2167

Last change on this file since 2167 was 2167, checked in by sacerdot, 7 years ago

Only one daemon left.

File size: 27.6 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "ASM/Assembly.ma".
16include "ASM/Interpret.ma".
17include "ASM/StatusProofs.ma".
18include alias "arithmetics/nat.ma".
19include "ASM/AssemblyProof.ma".
20
21lemma set_program_counter_status_of_pseudo_status:
22  ∀M.
23  ∀cm.
24  ∀ps.
25  ∀sigma.
26  ∀policy.
27  ∀new_ppc.
28    set_program_counter (BitVectorTrie Byte 16)
29      (code_memory_of_pseudo_assembly_program cm sigma policy)
30      (status_of_pseudo_status M cm ps sigma policy)
31      (sigma new_ppc) =
32    status_of_pseudo_status M cm (set_program_counter … cm ps new_ppc) sigma policy.
33  //
34qed.
35
36lemma set_p1_latch_status_of_pseudo_status:
37  ∀M.
38  ∀code_memory.
39  ∀sigma.
40  ∀policy.
41  ∀s.
42  ∀v.
43    set_p1_latch (BitVectorTrie Byte 16)
44      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
45      (status_of_pseudo_status M code_memory s sigma policy) v =
46    status_of_pseudo_status M code_memory
47      (set_p1_latch pseudo_assembly_program code_memory s v) sigma policy.
48  //
49qed.
50
51lemma set_p3_latch_status_of_pseudo_status:
52  ∀M.
53  ∀code_memory.
54  ∀sigma.
55  ∀policy.
56  ∀s.
57  ∀v.
58    set_p3_latch (BitVectorTrie Byte 16)
59      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
60      (status_of_pseudo_status M code_memory s sigma policy) v =
61    status_of_pseudo_status M code_memory
62      (set_p3_latch pseudo_assembly_program code_memory s v) sigma policy.
63  //
64qed.
65
66definition map_acc_a_using_internal_pseudo_address_map:
67    ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte ≝
68  λM, sigma, v.
69  match \snd M with
70  [ data ⇒ v
71  | address upper_lower word ⇒
72    let mapped ≝ sigma word in
73    let 〈high, low〉 ≝ vsplit bool 8 8 mapped in
74      if eq_upper_lower upper_lower upper then
75        high
76      else
77        low
78  ].
79
80(*CSC: Taken from AssemblyProofSplit.ma; there named map_lower_internal... *)
81definition map_internal_ram_address_using_pseudo_address_map:
82  ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝
83  λM: internal_pseudo_address_map.
84  λsigma: Word → Word.
85  λaddress: Byte.
86  λvalue: Byte.
87  match assoc_list_lookup ?? address (eq_bv …) (\fst M) with
88  [ None ⇒ value
89  | Some upper_lower_word ⇒
90    let 〈upper_lower, word〉 ≝ upper_lower_word in
91    let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in
92      if eq_upper_lower upper_lower upper then
93        high
94      else
95        low
96  ].
97
98definition map_address_using_internal_pseudo_address_map:
99    ∀M: internal_pseudo_address_map. (Word → Word) → SFR8051 → Byte → Byte ≝
100  λM, sigma, sfr, v.
101  match sfr with
102  [ SFR_ACC_A ⇒ map_acc_a_using_internal_pseudo_address_map M sigma v
103  | _         ⇒ v
104  ].
105
106lemma set_index_set_index_overwrite:
107  ∀A: Type[0].
108  ∀n: nat.
109  ∀v: Vector A n.
110  ∀index: nat.
111  ∀e, e': A.
112  ∀proof.
113  ∀proof'.
114    set_index A n v index e proof =
115      set_index A n (set_index A n v index e' proof') index e proof.
116  #A #n #v elim v normalize
117  [1:
118    #index #e #e' #absurd cases (lt_to_not_zero … absurd)
119  |2:
120    #n' #hd #tl #inductive_hypothesis #index #e #e' cases index #proof #proof'
121    normalize //
122  ]
123qed.
124
125lemma set_index_set_index_commutation:
126  ∀A: Type[0].
127  ∀n: nat.
128  ∀v: Vector A n.
129  ∀m, o: nat.
130  ∀m_lt_proof: m < n.
131  ∀o_lt_proof: o < n.
132  ∀e, f: A.
133    m ≠ o →
134      set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof =
135        set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof.
136  #A #n #v elim v
137  [1:
138    #m #o #m_lt_proof
139    normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof)
140  |2:
141    #n' #hd #tl #inductive_hypothesis
142    #m #o
143    cases m cases o
144    [1:
145      #m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant
146      @relevant %
147    |2,3:
148      #o' normalize //
149    |4:
150      #m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm
151      normalize @eq_f @inductive_hypothesis @nmk #relevant
152      >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) %
153    ]
154  ]
155qed.
156
157lemma set_index_status_of_pseudo_status:
158  ∀M, code_memory, sigma, policy, s, sfr, v, v'.
159    map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
160(set_index Byte 19
161  (special_function_registers_8051 (BitVectorTrie Byte 16)
162   (code_memory_of_pseudo_assembly_program code_memory sigma policy)
163   (status_of_pseudo_status M code_memory s sigma policy))
164  (sfr_8051_index sfr) v' (sfr8051_index_19 sfr)
165  =sfr_8051_of_pseudo_sfr_8051 M
166   (special_function_registers_8051 pseudo_assembly_program code_memory
167    (set_8051_sfr pseudo_assembly_program code_memory s sfr v)) sigma).
168  #M #code_memory #sigma #policy #s #sfr #v #v' #sfr_neq_acc_a_assm
169  whd in match status_of_pseudo_status; normalize nodelta
170  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
171  inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta
172  [1:
173    <sfr_neq_acc_a_assm cases sfr
174    [18:
175      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
176      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
177      >sndM_refl %
178    ]
179    %
180  |2:
181    @pair_elim #high #low #high_low_refl normalize nodelta
182    inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
183    <sfr_neq_acc_a_assm cases sfr
184    [18,37:
185      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
186      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
187      >sndM_refl normalize nodelta >high_low_refl normalize nodelta
188      >eq_upper_lower_refl normalize nodelta
189      whd in match (set_8051_sfr ?????);
190      [1:
191        <set_index_set_index_overwrite in ⊢ (??%?);
192        <set_index_set_index_overwrite in ⊢ (???%); %
193      |2:
194        <set_index_set_index_overwrite in ⊢ (??%?);
195        <set_index_set_index_overwrite in ⊢ (???%); %
196      ]
197    ]
198    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
199    whd in match (set_8051_sfr ?????); @set_index_set_index_commutation normalize
200    @nmk #absurd destruct(absurd)
201  ]
202qed.
203
204lemma set_8051_sfr_status_of_pseudo_status:
205  ∀M, code_memory, sigma, policy, s, sfr, v,v'.
206  map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
207(set_8051_sfr (BitVectorTrie Byte 16)
208  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
209  (status_of_pseudo_status M code_memory s sigma policy) sfr v'
210  =status_of_pseudo_status M code_memory
211   (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
212  #M #code_memory #sigma #policy #s #sfr #v #v' #v_ok
213  whd in ⊢ (??%%); @split_eq_status try % /2/
214qed.
215
216lemma set_8052_sfr_status_of_pseudo_status:
217  ∀M, code_memory, sigma, policy, s, sfr, v.
218(set_8052_sfr (BitVectorTrie Byte 16)
219  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
220  (status_of_pseudo_status M code_memory s sigma policy) sfr v
221  =status_of_pseudo_status M code_memory
222   (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
223 //
224qed.
225
226definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝
227  λb: Byte.
228    let address ≝ nat_of_bitvector … b in
229      if (eqb address 128) then None ?
230      else if (eqb address 144) then Some … (inl … SFR_P1)
231      else if (eqb address 160) then None ?
232      else if (eqb address 176) then Some … (inl … SFR_P3)
233      else if (eqb address 153) then Some … (inl … SFR_SBUF)
234      else if (eqb address 138) then Some … (inl … SFR_TL0)
235      else if (eqb address 139) then Some … (inl … SFR_TL1)
236      else if (eqb address 140) then Some … (inl … SFR_TH0)
237      else if (eqb address 141) then Some … (inl … SFR_TH1)
238      else if (eqb address 200) then Some … (inr … SFR_T2CON)
239      else if (eqb address 202) then Some … (inr … SFR_RCAP2L)
240      else if (eqb address 203) then Some … (inr … SFR_RCAP2H)
241      else if (eqb address 204) then Some … (inr … SFR_TL2)
242      else if (eqb address 205) then Some … (inr … SFR_TH2)
243      else if (eqb address 135) then Some … (inl … SFR_PCON)
244      else if (eqb address 136) then Some … (inl … SFR_TCON)
245      else if (eqb address 137) then Some … (inl … SFR_TMOD)
246      else if (eqb address 152) then Some … (inl … SFR_SCON)
247      else if (eqb address 168) then Some … (inl … SFR_IE)
248      else if (eqb address 184) then Some … (inl … SFR_IP)
249      else if (eqb address 129) then Some … (inl … SFR_SP)
250      else if (eqb address 130) then Some … (inl … SFR_DPL)
251      else if (eqb address 131) then Some … (inl … SFR_DPH)
252      else if (eqb address 208) then Some … (inl … SFR_PSW)
253      else if (eqb address 224) then Some … (inl … SFR_ACC_A)
254      else if (eqb address 240) then Some … (inl … SFR_ACC_B)
255      else None ?.
256
257definition set_bit_addressable_sfr:
258    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte →
259      PreStatus M code_memory ≝
260  λM: Type[0].
261  λcode_memory:M.
262  λs: PreStatus M code_memory.
263  λb: Byte.
264  λv: Byte.
265   match sfr_of_Byte b with
266   [ None ⇒ match not_implemented in False with [ ]
267   | Some sfr8051_8052 ⇒
268      match sfr8051_8052 with
269      [ inl sfr ⇒
270         match sfr with
271         [ SFR_P1 ⇒
272           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
273           set_p1_latch ?? s v
274         | SFR_P3 ⇒
275           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
276           set_p3_latch ?? s v
277         | _ ⇒ set_8051_sfr ?? s sfr v ]
278      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]].
279
280definition map_address_Byte_using_internal_pseudo_address_map ≝
281 λM,sigma,d,v.
282  match sfr_of_Byte d with
283  [ None ⇒ v
284  | Some sfr8051_8052 ⇒
285     match sfr8051_8052 with
286     [ inl sfr ⇒
287        map_address_using_internal_pseudo_address_map M sigma sfr v
288     | inr _ ⇒ v ]].
289
290lemma set_bit_addressable_sfr_status_of_pseudo_status':
291      let M ≝ pseudo_assembly_program in ∀code_memory: M. ∀s: PreStatus M code_memory. ∀d: Byte. ∀v: Byte.
292        Σp: PreStatus M code_memory. ∀M. ∀sigma. ∀policy. ∀v'.
293  map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
294 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
295  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
296  (status_of_pseudo_status M code_memory s sigma policy) d v'
297  =status_of_pseudo_status M code_memory
298   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
299  whd in match set_bit_addressable_sfr;
300  whd in match map_address_Byte_using_internal_pseudo_address_map;
301  normalize nodelta
302  @(let M ≝ pseudo_assembly_program in
303  λcode_memory:M.
304  λs: PreStatus M code_memory.
305  λb: Byte.
306  λv: Byte.
307   match sfr_of_Byte b with
308   [ None ⇒ match not_implemented in False with [ ]
309   | Some sfr8051_8052 ⇒
310      match sfr8051_8052 with
311      [ inl sfr ⇒
312         match sfr with
313         [ SFR_P1 ⇒
314           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
315           set_p1_latch ?? s v
316         | SFR_P3 ⇒
317           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
318           set_p3_latch ?? s v
319         | _ ⇒ set_8051_sfr ?? s sfr v ]
320      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]])
321 normalize nodelta
322 /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/
323 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta //
324qed.
325
326lemma set_bit_addressable_sfr_status_of_pseudo_status:
327 ∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte.
328  ∀M. ∀sigma. ∀policy. ∀v'.
329  map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
330 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
331  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
332  (status_of_pseudo_status M code_memory s sigma policy) d v'
333  =status_of_pseudo_status M code_memory
334   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
335 #code #s #d #v cases (set_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_
336 #H @H
337qed.
338
339lemma set_low_internal_ram_status_of_pseudo_status:
340 ∀cm,sigma,policy,M,s,ram.
341  set_low_internal_ram (BitVectorTrie Byte 16)
342  (code_memory_of_pseudo_assembly_program cm sigma policy)
343  (status_of_pseudo_status M cm s sigma policy)
344  (low_internal_ram_of_pseudo_low_internal_ram M ram)
345  = status_of_pseudo_status M cm
346    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
347 //
348qed.
349
350(* Real axiom ATM *)
351axiom insert_low_internal_ram_of_pseudo_low_internal_ram:
352 ∀M,sigma,cm,s,addr,v,v'.
353 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
354  insert Byte 7 addr v'
355  (low_internal_ram_of_pseudo_low_internal_ram M
356   (low_internal_ram pseudo_assembly_program cm s))
357  =low_internal_ram_of_pseudo_low_internal_ram M
358   (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
359               
360lemma insert_low_internal_ram_status_of_pseudo_status:
361 ∀M,cm,sigma,policy,s,addr,v,v'.
362 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
363  insert Byte 7 addr v'
364   (low_internal_ram (BitVectorTrie Byte 16)
365    (code_memory_of_pseudo_assembly_program cm sigma policy)
366    (status_of_pseudo_status M cm s sigma policy))
367  = low_internal_ram_of_pseudo_low_internal_ram M
368     (insert Byte 7 addr v
369      (low_internal_ram pseudo_assembly_program cm s)).
370 /2 by insert_low_internal_ram_of_pseudo_low_internal_ram/
371qed.
372
373(*CSC: Taken from AssemblyProofSplit *)
374lemma get_index_v_set_index_miss:
375  ∀T: Type[0].
376  ∀n, i, j: nat.
377  ∀v: Vector T n.
378  ∀b: T.
379  ∀i_proof: i < n.
380  ∀j_proof: j < n.
381  i ≠ j →
382    get_index_v T n (set_index T n v i b i_proof) j j_proof =
383      get_index_v T n v j j_proof.
384  #T #n #i #j #v lapply i lapply j elim v #i #j
385  [1:
386    #b #i_proof
387    cases (lt_to_not_zero … i_proof)
388  |2:
389    #tl #inductive_hypothesis #j' #i' #b #i_proof #j_proof #i_neq_j
390    lapply i_proof lapply i_neq_j cases i'
391    [1:
392      -i_neq_j #i_neq_j -i_proof #i_proof
393      whd in match (set_index ??????);
394      lapply j_proof lapply i_neq_j cases j'
395      [1:
396        #relevant @⊥ cases relevant -relevant #absurd @absurd %
397      |2:
398        #j' #_ -j_proof #j_proof %
399      ]
400    |2:
401      #i' -i_neq_j #i_neq_j -i_proof #i_proof
402      lapply j_proof lapply i_neq_j cases j'
403      [1:
404        #_ #j_proof %
405      |2:
406        #j' #i_neq_j #j_proof
407        @inductive_hypothesis @nmk #relevant
408        cases i_neq_j #absurd @absurd >relevant %
409      ]
410    ]
411  ]
412qed.
413
414lemma get_8051_sfr_status_of_pseudo_status:
415 ∀M,cm,s,sigma,policy,sfr.
416  get_8051_sfr …
417   (code_memory_of_pseudo_assembly_program cm sigma policy)
418   (status_of_pseudo_status M cm s sigma policy) sfr =
419  map_address_using_internal_pseudo_address_map M sigma sfr
420   (get_8051_sfr … cm s sfr).
421 #M #cm #s #sigma #policy #sfr whd in ⊢ (??%%);
422 whd in match status_of_pseudo_status; normalize nodelta
423 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
424 whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
425 cases (\snd M) normalize nodelta [cases sfr %]
426 #map_mem #map_acc @pair_elim #high #low #_ normalize nodelta
427 cases (eq_upper_lower ??) normalize nodelta cases sfr normalize nodelta
428 [18,37: @get_index_v_set_index
429 |*: >get_index_v_set_index_miss % normalize #abs destruct]
430qed.
431
432lemma bit_address_of_register_status_of_pseudo_status:
433 ∀M,cm,s,sigma,policy,r.
434  bit_address_of_register …
435  (code_memory_of_pseudo_assembly_program cm sigma policy)
436  (status_of_pseudo_status M cm s sigma policy) r =
437  bit_address_of_register … cm s r.
438 #M #cm #s #sigma #policy #r whd in ⊢ (??%%);
439 >get_8051_sfr_status_of_pseudo_status
440 @pair_elim #un #ln #_
441 @pair_elim #r1 #r0 #_ %
442qed.
443
444(*CSC: provable using the axiom in AssemblyProof, but this one seems more
445  primitive *)
446axiom lookup_low_internal_ram_of_pseudo_low_internal_ram:
447 ∀M,sigma,cm,s,addr.
448  lookup Byte 7 addr
449  (low_internal_ram_of_pseudo_low_internal_ram M
450   (low_internal_ram pseudo_assembly_program cm s)) (zero 8)
451  =
452  map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr)
453  (lookup Byte 7 addr
454   (low_internal_ram pseudo_assembly_program cm s) (zero 8)).
455
456lemma get_register_status_of_pseudo_status:
457 ∀M,cm,sigma,policy,s,r.
458  get_register …
459   (code_memory_of_pseudo_assembly_program cm sigma policy)
460   (status_of_pseudo_status M cm s sigma policy) r =
461  map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r)
462   (get_register … cm s r).
463 #M #cm #sigma #policy #s #r whd in match get_register; normalize nodelta
464 whd in match status_of_pseudo_status; normalize nodelta
465 >bit_address_of_register_status_of_pseudo_status
466 @lookup_low_internal_ram_of_pseudo_low_internal_ram
467qed.
468
469lemma external_ram_status_of_pseudo_status:
470 ∀M,cm,s,sigma,policy.
471  external_ram …
472   (code_memory_of_pseudo_assembly_program cm sigma policy)
473   (status_of_pseudo_status M cm s sigma policy) =
474  external_ram … cm s.
475 //
476qed.
477
478lemma set_external_ram_status_of_pseudo_status:
479  ∀M,cm,ps,sigma,policy,ram.
480    set_external_ram …
481      (code_memory_of_pseudo_assembly_program cm sigma policy)
482      (status_of_pseudo_status M cm ps sigma policy)
483      ram =
484    status_of_pseudo_status M cm (set_external_ram … cm ps ram) sigma policy.
485  //
486qed.
487
488lemma set_register_status_of_pseudo_status:
489 ∀M,cm,s,sigma,policy,r,v,v'.
490  map_internal_ram_address_using_pseudo_address_map M sigma
491   (false:::bit_address_of_register pseudo_assembly_program cm s r) v =v' →
492  set_register (BitVectorTrie Byte 16)
493   (code_memory_of_pseudo_assembly_program cm sigma policy)
494   (status_of_pseudo_status M cm s sigma policy) r v'
495  = status_of_pseudo_status M cm (set_register pseudo_assembly_program cm s r v)
496    sigma policy.
497 #M #cm #s #sigma #policy #r #v #v' #v_ok
498 whd in match set_register; normalize nodelta
499 >bit_address_of_register_status_of_pseudo_status
500 >(insert_low_internal_ram_status_of_pseudo_status … v_ok)
501 @set_low_internal_ram_status_of_pseudo_status
502qed.
503
504definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝
505 λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λaddr.
506  match addr with
507  [ INDIRECT i ⇒
508     assoc_list_lookup ??
509      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None …
510  | EXT_INDIRECT e ⇒
511     assoc_list_lookup ??
512      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None …
513  | _ ⇒ True ].
514
515definition map_address_mode_using_internal_pseudo_address_map_ok2 ≝
516 λT,M,sigma,cm.λs:PreStatus T cm.λaddr,v.
517  match addr with
518  [ DIRECT d ⇒
519     let 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit … 1 7 d in
520     match head' … bit_one with
521     [ true ⇒
522      map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v
523     | false ⇒
524      map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ]
525  | INDIRECT i ⇒
526     let register ≝ get_register ?? s [[ false; false; i ]] in
527     map_internal_ram_address_using_pseudo_address_map M sigma register v
528  | REGISTER r ⇒
529     map_internal_ram_address_using_pseudo_address_map M sigma
530      (false:::bit_address_of_register … s r) v
531  | ACC_A ⇒
532     map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v
533  | _ ⇒ v ].
534
535definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
536                                   acc_a ; acc_b ; ext_indirect ;
537                                   ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝
538  λm, cm, s, a, v.
539    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
540                                                acc_a ; acc_b ; ext_indirect ;
541                                                ext_indirect_dptr ]] x) →
542                   PreStatus m cm
543            with
544      [ DIRECT d ⇒
545        λdirect: True.
546          let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
547            match head' … bit_one with
548              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
549              | false ⇒
550                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
551                  set_low_internal_ram ?? s memory
552              ]
553      | INDIRECT i ⇒
554        λindirect: True.
555          let register ≝ get_register ?? s [[ false; false; i ]] in
556          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
557            match head' … bit_one with
558              [ false ⇒
559                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
560                  set_low_internal_ram ?? s memory
561              | true ⇒
562                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
563                  set_high_internal_ram ?? s memory
564              ]
565      | REGISTER r ⇒ λregister: True. set_register ?? s r v
566      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
567      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
568      | EXT_INDIRECT e ⇒
569        λext_indirect: True.
570          let address ≝ get_register ?? s [[ false; false; e ]] in
571          let padded_address ≝ pad 8 8 address in
572          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
573            set_external_ram ?? s memory
574      | EXT_INDIRECT_DPTR ⇒
575        λext_indirect_dptr: True.
576          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
577          let memory ≝ insert ? 16 address v (external_ram ?? s) in
578            set_external_ram ?? s memory
579      | _ ⇒
580        λother: False.
581          match other in False with [ ]
582      ] (subaddressing_modein … a).
583
584(*CSC: move elsewhere*)
585lemma eq_head': ∀A,n,v. v = head' A n v ::: tail … v.
586 #A #n #v inversion v in ⊢ ?;
587 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) /2/
588 | #m #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ' >EQ' % ]
589qed.
590
591(*CSC: move elsewhere*)
592lemma tail_singleton: ∀A,v. tail A 0 v = [[]].
593 #A #v inversion v in ⊢ ?;
594 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) #H destruct(H)
595 | #n #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ1 >EQ1 normalize
596   /2 by jmeq_to_eq/
597 ]
598qed.
599
600(*CSC: move elsewhere*)
601lemma eq_cons_head_append:
602 ∀A,n.∀hd: Vector A 1. ∀tl: Vector A n.
603  head' A 0 hd:::tl = hd@@tl.
604 #A #n #hd #tl >(eq_head' … hd) >tail_singleton %
605qed.
606
607lemma set_arg_8_status_of_pseudo_status:
608  ∀cm.
609  ∀ps.
610  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
611  ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'.
612   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps addr →
613   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
614    set_arg_8 (BitVectorTrie Byte 16)
615      (code_memory_of_pseudo_assembly_program cm sigma policy)
616      (status_of_pseudo_status M cm ps sigma policy)
617      addr value' =
618    status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
619  whd in match set_arg_8; normalize nodelta
620  @(let m ≝ pseudo_assembly_program in λcm, s. λa: [[ direct ; indirect ; registr ;
621                                   acc_a ; acc_b ; ext_indirect ;
622                                   ext_indirect_dptr ]]. λv.
623    match a return λaddr. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
624                                                acc_a ; acc_b ; ext_indirect ;
625                                                ext_indirect_dptr ]] addr) →
626                   Σp.?
627            with
628      [ DIRECT d ⇒
629        λdirect: True.
630          deplet 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit ? 1 7 d in
631            match head' … bit_one with
632              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
633              | false ⇒
634                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
635                  set_low_internal_ram ?? s memory
636              ]
637      | INDIRECT i ⇒
638        λindirect: True.
639          let register ≝ get_register ?? s [[ false; false; i ]] in
640          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
641            match head' … bit_one with
642              [ false ⇒
643                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
644                  set_low_internal_ram ?? s memory
645              | true ⇒
646                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
647                  set_high_internal_ram ?? s memory
648              ]
649      | REGISTER r ⇒ λregister: True. set_register ?? s r v
650      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
651      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
652      | EXT_INDIRECT e ⇒
653        λext_indirect: True.
654          let address ≝ get_register ?? s [[ false; false; e ]] in
655          let padded_address ≝ pad 8 8 address in
656          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
657            set_external_ram ?? s memory
658      | EXT_INDIRECT_DPTR ⇒
659        λext_indirect_dptr: True.
660          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
661          let memory ≝ insert ? 16 address v (external_ram ?? s) in
662            set_external_ram ?? s memory
663      | _ ⇒
664        λother: False.
665          match other in False with [ ]
666      ] (subaddressing_modein … a)) normalize nodelta
667  #M #sigma #policy #v'
668  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
669  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
670  [1,2:
671    <vsplit_refl normalize nodelta >p normalize nodelta
672    [ >(vsplit_ok … vsplit_refl) #_ @set_bit_addressable_sfr_status_of_pseudo_status
673    | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
674  |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p;
675      >get_register_status_of_pseudo_status
676      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
677      >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
678      [ cases daemon (*CSC*)
679      | >(insert_low_internal_ram_status_of_pseudo_status … v) // <EQ2
680        @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % ]
681  |5: #EQ1 #EQ2 <EQ2 >get_register_status_of_pseudo_status
682      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
683      >EQ1 normalize nodelta
684      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status
685  |6: #EQ1 #EQ2 <EQ2 /2 by set_register_status_of_pseudo_status/
686  |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/
687  |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
688  |9: #_ #EQ <EQ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status
689      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ]
690qed.
Note: See TracBrowser for help on using the repository browser.