source: src/ASM/Test.ma @ 2163

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

Steady progress.

File size: 19.3 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
80definition map_address_using_internal_pseudo_address_map:
81    ∀M: internal_pseudo_address_map. (Word → Word) → SFR8051 → Byte → Byte ≝
82  λM, sigma, sfr, v.
83  match sfr with
84  [ SFR_ACC_A ⇒ map_acc_a_using_internal_pseudo_address_map M sigma v
85  | _         ⇒ v
86  ].
87
88lemma set_index_set_index_overwrite:
89  ∀A: Type[0].
90  ∀n: nat.
91  ∀v: Vector A n.
92  ∀index: nat.
93  ∀e, e': A.
94  ∀proof.
95  ∀proof'.
96    set_index A n v index e proof =
97      set_index A n (set_index A n v index e' proof') index e proof.
98  #A #n #v elim v normalize
99  [1:
100    #index #e #e' #absurd cases (lt_to_not_zero … absurd)
101  |2:
102    #n' #hd #tl #inductive_hypothesis #index #e #e' cases index #proof #proof'
103    normalize //
104  ]
105qed.
106
107lemma set_index_set_index_commutation:
108  ∀A: Type[0].
109  ∀n: nat.
110  ∀v: Vector A n.
111  ∀m, o: nat.
112  ∀m_lt_proof: m < n.
113  ∀o_lt_proof: o < n.
114  ∀e, f: A.
115    m ≠ o →
116      set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof =
117        set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof.
118  #A #n #v elim v
119  [1:
120    #m #o #m_lt_proof
121    normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof)
122  |2:
123    #n' #hd #tl #inductive_hypothesis
124    #m #o
125    cases m cases o
126    [1:
127      #m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant
128      @relevant %
129    |2,3:
130      #o' normalize //
131    |4:
132      #m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm
133      normalize @eq_f @inductive_hypothesis @nmk #relevant
134      >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) %
135    ]
136  ]
137qed.
138
139lemma set_index_status_of_pseudo_status:
140  ∀M, code_memory, sigma, policy, s, sfr, v, v'.
141    map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
142(set_index Byte 19
143  (special_function_registers_8051 (BitVectorTrie Byte 16)
144   (code_memory_of_pseudo_assembly_program code_memory sigma policy)
145   (status_of_pseudo_status M code_memory s sigma policy))
146  (sfr_8051_index sfr) v' (sfr8051_index_19 sfr)
147  =sfr_8051_of_pseudo_sfr_8051 M
148   (special_function_registers_8051 pseudo_assembly_program code_memory
149    (set_8051_sfr pseudo_assembly_program code_memory s sfr v)) sigma).
150  #M #code_memory #sigma #policy #s #sfr #v #v' #sfr_neq_acc_a_assm
151  whd in match status_of_pseudo_status; normalize nodelta
152  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
153  inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta
154  [1:
155    <sfr_neq_acc_a_assm cases sfr
156    [18:
157      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
158      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
159      >sndM_refl %
160    ]
161    %
162  |2:
163    @pair_elim #high #low #high_low_refl normalize nodelta
164    inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
165    <sfr_neq_acc_a_assm cases sfr
166    [18,37:
167      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
168      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
169      >sndM_refl normalize nodelta >high_low_refl normalize nodelta
170      >eq_upper_lower_refl normalize nodelta
171      whd in match (set_8051_sfr ?????);
172      [1:
173        <set_index_set_index_overwrite in ⊢ (??%?);
174        <set_index_set_index_overwrite in ⊢ (???%); %
175      |2:
176        <set_index_set_index_overwrite in ⊢ (??%?);
177        <set_index_set_index_overwrite in ⊢ (???%); %
178      ]
179    ]
180    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
181    whd in match (set_8051_sfr ?????); @set_index_set_index_commutation normalize
182    @nmk #absurd destruct(absurd)
183  ]
184qed.
185
186lemma set_8051_sfr_status_of_pseudo_status:
187  ∀M, code_memory, sigma, policy, s, sfr, v,v'.
188  map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
189(set_8051_sfr (BitVectorTrie Byte 16)
190  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
191  (status_of_pseudo_status M code_memory s sigma policy) sfr v'
192  =status_of_pseudo_status M code_memory
193   (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
194  #M #code_memory #sigma #policy #s #sfr #v #v' #v_ok
195  whd in ⊢ (??%%); @split_eq_status try % /2/
196qed.
197
198lemma set_8052_sfr_status_of_pseudo_status:
199  ∀M, code_memory, sigma, policy, s, sfr, v.
200(set_8052_sfr (BitVectorTrie Byte 16)
201  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
202  (status_of_pseudo_status M code_memory s sigma policy) sfr v
203  =status_of_pseudo_status M code_memory
204   (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
205 //
206qed.
207
208definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝
209  λb: Byte.
210    let address ≝ nat_of_bitvector … b in
211      if (eqb address 128) then None ?
212      else if (eqb address 144) then Some … (inl … SFR_P1)
213      else if (eqb address 160) then None ?
214      else if (eqb address 176) then Some … (inl … SFR_P3)
215      else if (eqb address 153) then Some … (inl … SFR_SBUF)
216      else if (eqb address 138) then Some … (inl … SFR_TL0)
217      else if (eqb address 139) then Some … (inl … SFR_TL1)
218      else if (eqb address 140) then Some … (inl … SFR_TH0)
219      else if (eqb address 141) then Some … (inl … SFR_TH1)
220      else if (eqb address 200) then Some … (inr … SFR_T2CON)
221      else if (eqb address 202) then Some … (inr … SFR_RCAP2L)
222      else if (eqb address 203) then Some … (inr … SFR_RCAP2H)
223      else if (eqb address 204) then Some … (inr … SFR_TL2)
224      else if (eqb address 205) then Some … (inr … SFR_TH2)
225      else if (eqb address 135) then Some … (inl … SFR_PCON)
226      else if (eqb address 136) then Some … (inl … SFR_TCON)
227      else if (eqb address 137) then Some … (inl … SFR_TMOD)
228      else if (eqb address 152) then Some … (inl … SFR_SCON)
229      else if (eqb address 168) then Some … (inl … SFR_IE)
230      else if (eqb address 184) then Some … (inl … SFR_IP)
231      else if (eqb address 129) then Some … (inl … SFR_SP)
232      else if (eqb address 130) then Some … (inl … SFR_DPL)
233      else if (eqb address 131) then Some … (inl … SFR_DPH)
234      else if (eqb address 208) then Some … (inl … SFR_PSW)
235      else if (eqb address 224) then Some … (inl … SFR_ACC_A)
236      else if (eqb address 240) then Some … (inl … SFR_ACC_B)
237      else None ?.
238
239definition set_bit_addressable_sfr:
240    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte →
241      PreStatus M code_memory ≝
242  λM: Type[0].
243  λcode_memory:M.
244  λs: PreStatus M code_memory.
245  λb: Byte.
246  λv: Byte.
247   match sfr_of_Byte b with
248   [ None ⇒ match not_implemented in False with [ ]
249   | Some sfr8051_8052 ⇒
250      match sfr8051_8052 with
251      [ inl sfr ⇒
252         match sfr with
253         [ SFR_P1 ⇒
254           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
255           set_p1_latch ?? s v
256         | SFR_P3 ⇒
257           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
258           set_p3_latch ?? s v
259         | _ ⇒ set_8051_sfr ?? s sfr v ]
260      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]].
261
262definition map_address_Byte_using_internal_pseudo_address_map ≝
263 λM,sigma,d,v.
264  match sfr_of_Byte d with
265  [ None ⇒ v
266  | Some sfr8051_8052 ⇒
267     match sfr8051_8052 with
268     [ inl sfr ⇒
269        map_address_using_internal_pseudo_address_map M sigma sfr v
270     | inr _ ⇒ v ]].
271
272lemma set_bit_addressable_sfr_status_of_pseudo_status':
273      let M ≝ pseudo_assembly_program in ∀code_memory: M. ∀s: PreStatus M code_memory. ∀d: Byte. ∀v: Byte.
274        Σp: PreStatus M code_memory. ∀M. ∀sigma. ∀policy. ∀v'.
275  map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
276 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
277  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
278  (status_of_pseudo_status M code_memory s sigma policy) d v'
279  =status_of_pseudo_status M code_memory
280   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
281  whd in match set_bit_addressable_sfr;
282  whd in match map_address_Byte_using_internal_pseudo_address_map;
283  normalize nodelta
284  @(let M ≝ pseudo_assembly_program in
285  λcode_memory:M.
286  λs: PreStatus M code_memory.
287  λb: Byte.
288  λv: Byte.
289   match sfr_of_Byte b with
290   [ None ⇒ match not_implemented in False with [ ]
291   | Some sfr8051_8052 ⇒
292      match sfr8051_8052 with
293      [ inl sfr ⇒
294         match sfr with
295         [ SFR_P1 ⇒
296           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
297           set_p1_latch ?? s v
298         | SFR_P3 ⇒
299           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
300           set_p3_latch ?? s v
301         | _ ⇒ set_8051_sfr ?? s sfr v ]
302      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]])
303 normalize nodelta
304 /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/
305 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta //
306qed.
307
308lemma set_bit_addressable_sfr_status_of_pseudo_status:
309 ∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte.
310  ∀M. ∀sigma. ∀policy. ∀v'.
311  map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
312 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
313  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
314  (status_of_pseudo_status M code_memory s sigma policy) d v'
315  =status_of_pseudo_status M code_memory
316   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
317 #code #s #d #v cases (set_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_
318 #H @H
319qed.
320
321check status_of_pseudo_status
322
323lemma set_low_internal_fram_status_of_pseudo_status:
324 ∀cm,sigma,policy,M,s,ram.
325  set_low_internal_ram (BitVectorTrie Byte 16)
326  (code_memory_of_pseudo_assembly_program cm sigma policy)
327  (status_of_pseudo_status M cm s sigma policy)
328  (low_internal_ram_of_pseudo_low_internal_ram M ram)
329  = status_of_pseudo_status M cm
330    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
331 //
332qed.
333               
334lemma set_low_internal_fram_status_of_pseudo_status:
335 ∀M,cm,sigma,policy,s,addr,v.
336  insert Byte 7 addr v
337   (low_internal_ram (BitVectorTrie Byte 16)
338    (code_memory_of_pseudo_assembly_program cm sigma policy)
339    (status_of_pseudo_status M cm s sigma policy))
340  = low_internal_ram_of_pseudo_low_internal_ram M
341     (insert Byte 7 addr v
342      (low_internal_ram pseudo_assembly_program cm s)).
343 #M #cm #sigma #policy #s #addr #v
344 
345
346definition map_address_mode_using_internal_pseudo_address_map ≝
347 λM,sigma,addr,v.
348  match addr with
349  [ DIRECT d ⇒
350     let 〈 nu, nl 〉 as vsplit_refl ≝ vsplit … 4 4 d in
351     match get_index_v ? ? nu 0 ? with
352     [ true ⇒
353      map_address_Byte_using_internal_pseudo_address_map M sigma d v
354     | false ⇒ v ]
355  | _ ⇒ v ].
356//
357qed.
358
359definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
360                                   acc_a ; acc_b ; ext_indirect ;
361                                   ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝
362  λm, cm, s, a, v.
363    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
364                                                acc_a ; acc_b ; ext_indirect ;
365                                                ext_indirect_dptr ]] x) →
366                   PreStatus m cm
367            with
368      [ DIRECT d ⇒
369        λdirect: True.
370          let 〈 nu, nl 〉 ≝ vsplit … 4 4 d in
371          let bit_one ≝ get_index_v ? ? nu 0 ? in
372          let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
373            match bit_one with
374              [ true ⇒ set_bit_addressable_sfr ?? s d v
375              | false ⇒
376                let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ?? s) in
377                  set_low_internal_ram ?? s memory
378              ]
379      | INDIRECT i ⇒
380        λindirect: True.
381          let register ≝ get_register ?? s [[ false; false; i ]] in
382          let 〈nu, nl〉 ≝ vsplit ? 4 4 register in
383          let bit_1 ≝ get_index_v … nu 0 ? in
384          let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in
385            match bit_1 with
386              [ false ⇒
387                let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ?? s) in
388                  set_low_internal_ram ?? s memory
389              | true ⇒
390                let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ?? s) in
391                  set_high_internal_ram ?? s memory
392              ]
393      | REGISTER r ⇒ λregister: True. set_register ?? s r v
394      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
395      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
396      | EXT_INDIRECT e ⇒
397        λext_indirect: True.
398          let address ≝ get_register ?? s [[ false; false; e ]] in
399          let padded_address ≝ pad 8 8 address in
400          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
401            set_external_ram ?? s memory
402      | EXT_INDIRECT_DPTR ⇒
403        λext_indirect_dptr: True.
404          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
405          let memory ≝ insert ? 16 address v (external_ram ?? s) in
406            set_external_ram ?? s memory
407      | _ ⇒
408        λother: False.
409          match other in False with [ ]
410      ] (subaddressing_modein … a).
411  //
412qed.
413
414lemma set_arg_8_status_of_pseudo_status:
415  ∀cm.
416  ∀ps.
417  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
418  ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'.
419   map_address_mode_using_internal_pseudo_address_map M sigma addr value = value' →
420    set_arg_8 (BitVectorTrie Byte 16)
421      (code_memory_of_pseudo_assembly_program cm sigma policy)
422      (status_of_pseudo_status M cm ps sigma policy)
423      addr value' =
424    status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
425  whd in match set_arg_8; normalize nodelta
426  @(let m ≝ pseudo_assembly_program in λcm, s. λa: [[ direct ; indirect ; registr ;
427                                   acc_a ; acc_b ; ext_indirect ;
428                                   ext_indirect_dptr ]]. λv.
429    match a return λaddr. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
430                                                acc_a ; acc_b ; ext_indirect ;
431                                                ext_indirect_dptr ]] addr) →
432                   Σp.?
433            with
434      [ DIRECT d ⇒
435        λdirect: True.
436          deplet 〈 nu, nl 〉 as vsplit_refl ≝ vsplit … 4 4 d in
437          let bit_one ≝ get_index_v ? ? nu 0 ? in
438          let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
439            match bit_one with
440              [ true ⇒ set_bit_addressable_sfr ?? s d v
441              | false ⇒
442                let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ?? s) in
443                  set_low_internal_ram ?? s memory
444              ]
445      | INDIRECT i ⇒
446        λindirect: True.
447          let register ≝ get_register ?? s [[ false; false; i ]] in
448          let 〈nu, nl〉 ≝ vsplit ? 4 4 register in
449          let bit_1 ≝ get_index_v … nu 0 ? in
450          let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in
451            match bit_1 with
452              [ false ⇒
453                let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ?? s) in
454                  set_low_internal_ram ?? s memory
455              | true ⇒
456                let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ?? s) in
457                  set_high_internal_ram ?? s memory
458              ]
459      | REGISTER r ⇒ λregister: True. set_register ?? s r v
460      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
461      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
462      | EXT_INDIRECT e ⇒
463        λext_indirect: True.
464          let address ≝ get_register ?? s [[ false; false; e ]] in
465          let padded_address ≝ pad 8 8 address in
466          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
467            set_external_ram ?? s memory
468      | EXT_INDIRECT_DPTR ⇒
469        λext_indirect_dptr: True.
470          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
471          let memory ≝ insert ? 16 address v (external_ram ?? s) in
472            set_external_ram ?? s memory
473      | _ ⇒
474        λother: False.
475          match other in False with [ ]
476      ] (subaddressing_modein … a)) normalize nodelta
477  [3,6: // ] #M #sigma #policy #v' whd in ⊢ (??%? → ?);
478  [1,2:
479    <vsplit_refl normalize nodelta >p normalize nodelta
480    normalize nodelta in p1; >p1 normalize nodelta
481    [ @set_bit_addressable_sfr_status_of_pseudo_status
482    | #v_ok <v_ok @set_low_internal_ram_status_of_pseudo_status
483    ]
484  |2:   
485qed.
Note: See TracBrowser for help on using the repository browser.