source: src/ASM/Test.ma @ 2165

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

Only three daemons left.

File size: 26.3 KB
RevLine 
[2160]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
[2164]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
[2160]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:
[2163]205  ∀M, code_memory, sigma, policy, s, sfr, v,v'.
206  map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
[2160]207(set_8051_sfr (BitVectorTrie Byte 16)
208  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
[2163]209  (status_of_pseudo_status M code_memory s sigma policy) sfr v'
[2160]210  =status_of_pseudo_status M code_memory
211   (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
[2163]212  #M #code_memory #sigma #policy #s #sfr #v #v' #v_ok
213  whd in ⊢ (??%%); @split_eq_status try % /2/
214qed.
[2160]215
[2163]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
[2160]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.
[2163]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 ]].
[2160]279
[2163]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':
[2160]291      let M ≝ pseudo_assembly_program in ∀code_memory: M. ∀s: PreStatus M code_memory. ∀d: Byte. ∀v: Byte.
[2163]292        Σp: PreStatus M code_memory. ∀M. ∀sigma. ∀policy. ∀v'.
293  map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
[2160]294 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
295  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
[2163]296  (status_of_pseudo_status M code_memory s sigma policy) d v'
[2160]297  =status_of_pseudo_status M code_memory
298   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
[2163]299  whd in match set_bit_addressable_sfr;
300  whd in match map_address_Byte_using_internal_pseudo_address_map;
301  normalize nodelta
[2160]302  @(let M ≝ pseudo_assembly_program in
303  λcode_memory:M.
304  λs: PreStatus M code_memory.
305  λb: Byte.
306  λv: Byte.
[2163]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.
[2160]325
[2163]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
[2164]339lemma set_low_internal_ram_status_of_pseudo_status:
[2163]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.
[2164]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)).
[2163]359               
[2164]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'
[2163]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)).
[2164]370 /2 by insert_low_internal_ram_of_pseudo_low_internal_ram/
371qed.
[2163]372
[2164]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
[2165]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
[2164]488definition map_address_mode_using_internal_pseudo_address_map_ok ≝
489 λM,sigma,cm.λs:PreStatus ? cm.λaddr,v,v'.
[2163]490  match addr with
491  [ DIRECT d ⇒
[2164]492     let 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit … 1 7 d in
493     match head' … bit_one with
[2163]494     [ true ⇒
[2164]495      map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v
496     | false ⇒
497      map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ] = v'
498  | INDIRECT i ⇒
499     assoc_list_lookup ??
500      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None … ∧
501     let register ≝ get_register ?? s [[ false; false; i ]] in
502     map_internal_ram_address_using_pseudo_address_map M sigma register v = v'
[2165]503  | EXT_INDIRECT e ⇒
504     assoc_list_lookup ??
505      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None … ∧
506     v = v'
[2164]507  | _ ⇒ v = v'].
[2163]508
[2160]509definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
510                                   acc_a ; acc_b ; ext_indirect ;
511                                   ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝
512  λm, cm, s, a, v.
513    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
514                                                acc_a ; acc_b ; ext_indirect ;
515                                                ext_indirect_dptr ]] x) →
516                   PreStatus m cm
517            with
518      [ DIRECT d ⇒
519        λdirect: True.
[2164]520          let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
521            match head' … bit_one with
522              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
[2160]523              | false ⇒
[2164]524                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
[2160]525                  set_low_internal_ram ?? s memory
526              ]
527      | INDIRECT i ⇒
528        λindirect: True.
529          let register ≝ get_register ?? s [[ false; false; i ]] in
[2164]530          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
531            match head' … bit_one with
[2160]532              [ false ⇒
[2164]533                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
[2160]534                  set_low_internal_ram ?? s memory
535              | true ⇒
[2164]536                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
[2160]537                  set_high_internal_ram ?? s memory
538              ]
539      | REGISTER r ⇒ λregister: True. set_register ?? s r v
540      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
541      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
542      | EXT_INDIRECT e ⇒
543        λext_indirect: True.
544          let address ≝ get_register ?? s [[ false; false; e ]] in
545          let padded_address ≝ pad 8 8 address in
546          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
547            set_external_ram ?? s memory
548      | EXT_INDIRECT_DPTR ⇒
549        λext_indirect_dptr: True.
550          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
551          let memory ≝ insert ? 16 address v (external_ram ?? s) in
552            set_external_ram ?? s memory
553      | _ ⇒
554        λother: False.
555          match other in False with [ ]
556      ] (subaddressing_modein … a).
[2164]557
558(*CSC: move elsewhere*)
559lemma eq_head': ∀A,n,v. v = head' A n v ::: tail … v.
560 #A #n #v inversion v in ⊢ ?;
561 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) /2/
562 | #m #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ' >EQ' % ]
[2160]563qed.
564
[2164]565(*CSC: move elsewhere*)
566lemma tail_singleton: ∀A,v. tail A 0 v = [[]].
567 #A #v inversion v in ⊢ ?;
568 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) #H destruct(H)
569 | #n #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ1 >EQ1 normalize
570   /2 by jmeq_to_eq/
571 ]
572qed.
573
574(*CSC: move elsewhere*)
575lemma eq_cons_head_append:
576 ∀A,n.∀hd: Vector A 1. ∀tl: Vector A n.
577  head' A 0 hd:::tl = hd@@tl.
578 #A #n #hd #tl >(eq_head' … hd) >tail_singleton %
579qed.
580
[2160]581lemma set_arg_8_status_of_pseudo_status:
582  ∀cm.
583  ∀ps.
[2163]584  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
585  ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'.
[2164]586   map_address_mode_using_internal_pseudo_address_map_ok … M sigma cm ps addr value value' →
[2160]587    set_arg_8 (BitVectorTrie Byte 16)
588      (code_memory_of_pseudo_assembly_program cm sigma policy)
589      (status_of_pseudo_status M cm ps sigma policy)
[2163]590      addr value' =
[2160]591    status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
[2163]592  whd in match set_arg_8; normalize nodelta
[2160]593  @(let m ≝ pseudo_assembly_program in λcm, s. λa: [[ direct ; indirect ; registr ;
594                                   acc_a ; acc_b ; ext_indirect ;
595                                   ext_indirect_dptr ]]. λv.
596    match a return λaddr. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
597                                                acc_a ; acc_b ; ext_indirect ;
598                                                ext_indirect_dptr ]] addr) →
[2163]599                   Σp.?
[2160]600            with
601      [ DIRECT d ⇒
602        λdirect: True.
[2164]603          deplet 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit ? 1 7 d in
604            match head' … bit_one with
605              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
[2160]606              | false ⇒
[2164]607                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
[2160]608                  set_low_internal_ram ?? s memory
609              ]
610      | INDIRECT i ⇒
611        λindirect: True.
612          let register ≝ get_register ?? s [[ false; false; i ]] in
[2164]613          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
614            match head' … bit_one with
[2160]615              [ false ⇒
[2164]616                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
[2160]617                  set_low_internal_ram ?? s memory
618              | true ⇒
[2164]619                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
[2160]620                  set_high_internal_ram ?? s memory
621              ]
622      | REGISTER r ⇒ λregister: True. set_register ?? s r v
623      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
624      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
625      | EXT_INDIRECT e ⇒
626        λext_indirect: True.
627          let address ≝ get_register ?? s [[ false; false; e ]] in
628          let padded_address ≝ pad 8 8 address in
629          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
630            set_external_ram ?? s memory
631      | EXT_INDIRECT_DPTR ⇒
632        λext_indirect_dptr: True.
633          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
634          let memory ≝ insert ? 16 address v (external_ram ?? s) in
635            set_external_ram ?? s memory
636      | _ ⇒
637        λother: False.
638          match other in False with [ ]
[2163]639      ] (subaddressing_modein … a)) normalize nodelta
[2164]640  #M #sigma #policy #v' whd in match map_address_mode_using_internal_pseudo_address_map_ok; normalize nodelta
[2163]641  [1,2:
642    <vsplit_refl normalize nodelta >p normalize nodelta
[2164]643    [ >(vsplit_ok … vsplit_refl) @set_bit_addressable_sfr_status_of_pseudo_status
644    | #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
645  |3,4: * #EQ1 #EQ2 change with (get_register ????) in match register in p;
646      >get_register_status_of_pseudo_status
647      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
648      >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
[2165]649      [ cases daemon (*CSC*)
[2164]650      | >(insert_low_internal_ram_status_of_pseudo_status … v) // <EQ2
651        @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % ]
[2165]652  |5: * #EQ1 #EQ2 <EQ2 >get_register_status_of_pseudo_status
653      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
654      >EQ1 normalize nodelta
655      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status
656  |6: #EQ <EQ cases daemon (*CSC*)
657  |7: #EQ <EQ @set_8051_sfr_status_of_pseudo_status cases daemon (*CSC*)
658  |8: #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
659  |9: #EQ <EQ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status
660      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ]
661qed.
Note: See TracBrowser for help on using the repository browser.