source: src/ASM/Test.ma @ 2168

Last change on this file since 2168 was 2168, checked in by sacerdot, 6 years ago

No more daemons left! All axioms are real axioms.

File size: 28.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(* Real axiom ATM *)
374axiom insert_high_internal_ram_of_pseudo_high_internal_ram:
375 ∀M,sigma,cm,s,addr,v,v'.
376 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
377  insert Byte 7 addr v'
378  (high_internal_ram_of_pseudo_high_internal_ram M
379   (high_internal_ram pseudo_assembly_program cm s))
380  =high_internal_ram_of_pseudo_high_internal_ram M
381   (insert Byte 7 addr v (high_internal_ram pseudo_assembly_program cm s)).
382
383lemma insert_high_internal_ram_status_of_pseudo_status:
384 ∀M,cm,sigma,policy,s,addr,v,v'.
385 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
386  insert Byte 7 addr v'
387   (high_internal_ram (BitVectorTrie Byte 16)
388    (code_memory_of_pseudo_assembly_program cm sigma policy)
389    (status_of_pseudo_status M cm s sigma policy))
390  = high_internal_ram_of_pseudo_high_internal_ram M
391     (insert Byte 7 addr v
392      (high_internal_ram pseudo_assembly_program cm s)).
393 /2 by insert_high_internal_ram_of_pseudo_high_internal_ram/
394qed.
395
396(*CSC: Taken from AssemblyProofSplit *)
397lemma get_index_v_set_index_miss:
398  ∀T: Type[0].
399  ∀n, i, j: nat.
400  ∀v: Vector T n.
401  ∀b: T.
402  ∀i_proof: i < n.
403  ∀j_proof: j < n.
404  i ≠ j →
405    get_index_v T n (set_index T n v i b i_proof) j j_proof =
406      get_index_v T n v j j_proof.
407  #T #n #i #j #v lapply i lapply j elim v #i #j
408  [1:
409    #b #i_proof
410    cases (lt_to_not_zero … i_proof)
411  |2:
412    #tl #inductive_hypothesis #j' #i' #b #i_proof #j_proof #i_neq_j
413    lapply i_proof lapply i_neq_j cases i'
414    [1:
415      -i_neq_j #i_neq_j -i_proof #i_proof
416      whd in match (set_index ??????);
417      lapply j_proof lapply i_neq_j cases j'
418      [1:
419        #relevant @⊥ cases relevant -relevant #absurd @absurd %
420      |2:
421        #j' #_ -j_proof #j_proof %
422      ]
423    |2:
424      #i' -i_neq_j #i_neq_j -i_proof #i_proof
425      lapply j_proof lapply i_neq_j cases j'
426      [1:
427        #_ #j_proof %
428      |2:
429        #j' #i_neq_j #j_proof
430        @inductive_hypothesis @nmk #relevant
431        cases i_neq_j #absurd @absurd >relevant %
432      ]
433    ]
434  ]
435qed.
436
437lemma get_8051_sfr_status_of_pseudo_status:
438 ∀M,cm,s,sigma,policy,sfr.
439  get_8051_sfr …
440   (code_memory_of_pseudo_assembly_program cm sigma policy)
441   (status_of_pseudo_status M cm s sigma policy) sfr =
442  map_address_using_internal_pseudo_address_map M sigma sfr
443   (get_8051_sfr … cm s sfr).
444 #M #cm #s #sigma #policy #sfr whd in ⊢ (??%%);
445 whd in match status_of_pseudo_status; normalize nodelta
446 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
447 whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
448 cases (\snd M) normalize nodelta [cases sfr %]
449 #map_mem #map_acc @pair_elim #high #low #_ normalize nodelta
450 cases (eq_upper_lower ??) normalize nodelta cases sfr normalize nodelta
451 [18,37: @get_index_v_set_index
452 |*: >get_index_v_set_index_miss % normalize #abs destruct]
453qed.
454
455lemma bit_address_of_register_status_of_pseudo_status:
456 ∀M,cm,s,sigma,policy,r.
457  bit_address_of_register …
458  (code_memory_of_pseudo_assembly_program cm sigma policy)
459  (status_of_pseudo_status M cm s sigma policy) r =
460  bit_address_of_register … cm s r.
461 #M #cm #s #sigma #policy #r whd in ⊢ (??%%);
462 >get_8051_sfr_status_of_pseudo_status
463 @pair_elim #un #ln #_
464 @pair_elim #r1 #r0 #_ %
465qed.
466
467(*CSC: provable using the axiom in AssemblyProof, but this one seems more
468  primitive *)
469axiom lookup_low_internal_ram_of_pseudo_low_internal_ram:
470 ∀M,sigma,cm,s,addr.
471  lookup Byte 7 addr
472  (low_internal_ram_of_pseudo_low_internal_ram M
473   (low_internal_ram pseudo_assembly_program cm s)) (zero 8)
474  =
475  map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr)
476  (lookup Byte 7 addr
477   (low_internal_ram pseudo_assembly_program cm s) (zero 8)).
478
479lemma get_register_status_of_pseudo_status:
480 ∀M,cm,sigma,policy,s,r.
481  get_register …
482   (code_memory_of_pseudo_assembly_program cm sigma policy)
483   (status_of_pseudo_status M cm s sigma policy) r =
484  map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r)
485   (get_register … cm s r).
486 #M #cm #sigma #policy #s #r whd in match get_register; normalize nodelta
487 whd in match status_of_pseudo_status; normalize nodelta
488 >bit_address_of_register_status_of_pseudo_status
489 @lookup_low_internal_ram_of_pseudo_low_internal_ram
490qed.
491
492lemma external_ram_status_of_pseudo_status:
493 ∀M,cm,s,sigma,policy.
494  external_ram …
495   (code_memory_of_pseudo_assembly_program cm sigma policy)
496   (status_of_pseudo_status M cm s sigma policy) =
497  external_ram … cm s.
498 //
499qed.
500
501lemma set_external_ram_status_of_pseudo_status:
502  ∀M,cm,ps,sigma,policy,ram.
503    set_external_ram …
504      (code_memory_of_pseudo_assembly_program cm sigma policy)
505      (status_of_pseudo_status M cm ps sigma policy)
506      ram =
507    status_of_pseudo_status M cm (set_external_ram … cm ps ram) sigma policy.
508  //
509qed.
510
511lemma set_register_status_of_pseudo_status:
512 ∀M,cm,s,sigma,policy,r,v,v'.
513  map_internal_ram_address_using_pseudo_address_map M sigma
514   (false:::bit_address_of_register pseudo_assembly_program cm s r) v =v' →
515  set_register (BitVectorTrie Byte 16)
516   (code_memory_of_pseudo_assembly_program cm sigma policy)
517   (status_of_pseudo_status M cm s sigma policy) r v'
518  = status_of_pseudo_status M cm (set_register pseudo_assembly_program cm s r v)
519    sigma policy.
520 #M #cm #s #sigma #policy #r #v #v' #v_ok
521 whd in match set_register; normalize nodelta
522 >bit_address_of_register_status_of_pseudo_status
523 >(insert_low_internal_ram_status_of_pseudo_status … v_ok)
524 @set_low_internal_ram_status_of_pseudo_status
525qed.
526
527definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝
528 λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λaddr.
529  match addr with
530  [ INDIRECT i ⇒
531     assoc_list_lookup ??
532      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None …
533  | EXT_INDIRECT e ⇒
534     assoc_list_lookup ??
535      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None …
536  | _ ⇒ True ].
537
538definition map_address_mode_using_internal_pseudo_address_map_ok2 ≝
539 λT,M,sigma,cm.λs:PreStatus T cm.λaddr,v.
540  match addr with
541  [ DIRECT d ⇒
542     let 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit … 1 7 d in
543     match head' … bit_one with
544     [ true ⇒
545      map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v
546     | false ⇒
547      map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ]
548  | INDIRECT i ⇒
549     let register ≝ get_register ?? s [[ false; false; i ]] in
550     map_internal_ram_address_using_pseudo_address_map M sigma register v
551  | REGISTER r ⇒
552     map_internal_ram_address_using_pseudo_address_map M sigma
553      (false:::bit_address_of_register … s r) v
554  | ACC_A ⇒
555     map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v
556  | _ ⇒ v ].
557
558definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
559                                   acc_a ; acc_b ; ext_indirect ;
560                                   ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝
561  λm, cm, s, a, v.
562    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
563                                                acc_a ; acc_b ; ext_indirect ;
564                                                ext_indirect_dptr ]] x) →
565                   PreStatus m cm
566            with
567      [ DIRECT d ⇒
568        λdirect: True.
569          let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
570            match head' … bit_one with
571              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
572              | false ⇒
573                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
574                  set_low_internal_ram ?? s memory
575              ]
576      | INDIRECT i ⇒
577        λindirect: True.
578          let register ≝ get_register ?? s [[ false; false; i ]] in
579          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
580            match head' … bit_one with
581              [ false ⇒
582                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
583                  set_low_internal_ram ?? s memory
584              | true ⇒
585                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
586                  set_high_internal_ram ?? s memory
587              ]
588      | REGISTER r ⇒ λregister: True. set_register ?? s r v
589      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
590      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
591      | EXT_INDIRECT e ⇒
592        λext_indirect: True.
593          let address ≝ get_register ?? s [[ false; false; e ]] in
594          let padded_address ≝ pad 8 8 address in
595          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
596            set_external_ram ?? s memory
597      | EXT_INDIRECT_DPTR ⇒
598        λext_indirect_dptr: True.
599          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
600          let memory ≝ insert ? 16 address v (external_ram ?? s) in
601            set_external_ram ?? s memory
602      | _ ⇒
603        λother: False.
604          match other in False with [ ]
605      ] (subaddressing_modein … a).
606
607(*CSC: move elsewhere*)
608lemma eq_head': ∀A,n,v. v = head' A n v ::: tail … v.
609 #A #n #v inversion v in ⊢ ?;
610 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) /2/
611 | #m #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ' >EQ' % ]
612qed.
613
614(*CSC: move elsewhere*)
615lemma tail_singleton: ∀A,v. tail A 0 v = [[]].
616 #A #v inversion v in ⊢ ?;
617 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) #H destruct(H)
618 | #n #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ1 >EQ1 normalize
619   /2 by jmeq_to_eq/
620 ]
621qed.
622
623(*CSC: move elsewhere*)
624lemma eq_cons_head_append:
625 ∀A,n.∀hd: Vector A 1. ∀tl: Vector A n.
626  head' A 0 hd:::tl = hd@@tl.
627 #A #n #hd #tl >(eq_head' … hd) >tail_singleton %
628qed.
629
630lemma set_arg_8_status_of_pseudo_status:
631  ∀cm.
632  ∀ps.
633  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
634  ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'.
635   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps addr →
636   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
637    set_arg_8 (BitVectorTrie Byte 16)
638      (code_memory_of_pseudo_assembly_program cm sigma policy)
639      (status_of_pseudo_status M cm ps sigma policy)
640      addr value' =
641    status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
642  whd in match set_arg_8; normalize nodelta
643  @(let m ≝ pseudo_assembly_program in λcm, s. λa: [[ direct ; indirect ; registr ;
644                                   acc_a ; acc_b ; ext_indirect ;
645                                   ext_indirect_dptr ]]. λv.
646    match a return λaddr. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
647                                                acc_a ; acc_b ; ext_indirect ;
648                                                ext_indirect_dptr ]] addr) →
649                   Σp.?
650            with
651      [ DIRECT d ⇒
652        λdirect: True.
653          deplet 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit ? 1 7 d in
654            match head' … bit_one with
655              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
656              | false ⇒
657                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
658                  set_low_internal_ram ?? s memory
659              ]
660      | INDIRECT i ⇒
661        λindirect: True.
662          let register ≝ get_register ?? s [[ false; false; i ]] in
663          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
664            match head' … bit_one with
665              [ false ⇒
666                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
667                  set_low_internal_ram ?? s memory
668              | true ⇒
669                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
670                  set_high_internal_ram ?? s memory
671              ]
672      | REGISTER r ⇒ λregister: True. set_register ?? s r v
673      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
674      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
675      | EXT_INDIRECT e ⇒
676        λext_indirect: True.
677          let address ≝ get_register ?? s [[ false; false; e ]] in
678          let padded_address ≝ pad 8 8 address in
679          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
680            set_external_ram ?? s memory
681      | EXT_INDIRECT_DPTR ⇒
682        λext_indirect_dptr: True.
683          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
684          let memory ≝ insert ? 16 address v (external_ram ?? s) in
685            set_external_ram ?? s memory
686      | _ ⇒
687        λother: False.
688          match other in False with [ ]
689      ] (subaddressing_modein … a)) normalize nodelta
690  #M #sigma #policy #v'
691  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
692  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
693  [1,2:
694    <vsplit_refl normalize nodelta >p normalize nodelta
695    [ >(vsplit_ok … vsplit_refl) #_ @set_bit_addressable_sfr_status_of_pseudo_status
696    | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
697  |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p;
698      >get_register_status_of_pseudo_status
699      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
700      >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
701      [ >(insert_high_internal_ram_status_of_pseudo_status … v)
702      | >(insert_low_internal_ram_status_of_pseudo_status … v) ]
703      // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
704  |5: #EQ1 #EQ2 <EQ2 >get_register_status_of_pseudo_status
705      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
706      >EQ1 normalize nodelta
707      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status
708  |6: #EQ1 #EQ2 <EQ2 /2 by set_register_status_of_pseudo_status/
709  |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/
710  |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
711  |9: #_ #EQ <EQ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status
712      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ]
713qed.
Note: See TracBrowser for help on using the repository browser.