source: src/ASM/Test.ma @ 2160

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

Added a new scratch file Test.ma for working on lemmas that are needed in the massive proof to avoid having to retypecheck everything. Lots of work from the last week on the AssemblyProofSplit?.ma file, as well as an attempt to use Russell-style types on set_arg_8.

File size: 18.0 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.
188(set_8051_sfr (BitVectorTrie Byte 16)
189  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
190  (status_of_pseudo_status M code_memory s sigma policy) sfr v
191  =status_of_pseudo_status M code_memory
192   (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
193  #M #code_memory #sigma #policy #s #sfr #v
194  whd in ⊢ (??%%); @split_eq_status try %
195
196definition set_bit_addressable_sfr:
197    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte →
198      PreStatus M code_memory ≝
199  λM: Type[0].
200  λcode_memory:M.
201  λs: PreStatus M code_memory.
202  λb: Byte.
203  λv: Byte.
204    let address ≝ nat_of_bitvector … b in
205      if (eqb address 128) then
206        match not_implemented in False with [ ]
207      else if (eqb address 144) then
208        let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
209        let status_2 ≝ set_p1_latch ?? s v in
210          status_2
211      else if (eqb address 160) then
212        match not_implemented in False with [ ]
213      else if (eqb address 176) then
214        let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
215        let status_2 ≝ set_p3_latch ?? s v in
216          status_2
217      else if (eqb address 153) then
218        set_8051_sfr ?? s SFR_SBUF v
219      else if (eqb address 138) then
220        set_8051_sfr ?? s SFR_TL0 v
221      else if (eqb address 139) then
222        set_8051_sfr ?? s SFR_TL1 v
223      else if (eqb address 140) then
224        set_8051_sfr ?? s SFR_TH0 v
225      else if (eqb address 141) then
226        set_8051_sfr ?? s SFR_TH1 v
227      else if (eqb address 200) then
228        set_8052_sfr ?? s SFR_T2CON v
229      else if (eqb address 202) then
230        set_8052_sfr ?? s SFR_RCAP2L v
231      else if (eqb address 203) then
232        set_8052_sfr ?? s SFR_RCAP2H v
233      else if (eqb address 204) then
234        set_8052_sfr ?? s SFR_TL2 v
235      else if (eqb address 205) then
236        set_8052_sfr ?? s SFR_TH2 v
237      else if (eqb address 135) then
238        set_8051_sfr ?? s SFR_PCON v
239      else if (eqb address 136) then
240        set_8051_sfr ?? s SFR_TCON v
241      else if (eqb address 137) then
242        set_8051_sfr ?? s SFR_TMOD v
243      else if (eqb address 152) then
244        set_8051_sfr ?? s SFR_SCON v
245      else if (eqb address 168) then
246        set_8051_sfr ?? s SFR_IE v
247      else if (eqb address 184) then
248        set_8051_sfr ?? s SFR_IP v
249      else if (eqb address 129) then
250        set_8051_sfr ?? s SFR_SP v
251      else if (eqb address 130) then
252        set_8051_sfr ?? s SFR_DPL v
253      else if (eqb address 131) then
254        set_8051_sfr ?? s SFR_DPH v
255      else if (eqb address 208) then
256        set_8051_sfr ?? s SFR_PSW v
257      else if (eqb address 224) then
258        set_8051_sfr ?? s SFR_ACC_A v
259      else if (eqb address 240) then
260        set_8051_sfr ?? s SFR_ACC_B v
261      else
262        match not_implemented in False with [ ].
263
264lemma set_bit_addressable_sfr_status_of_pseudo_status:
265      let M ≝ pseudo_assembly_program in ∀code_memory: M. ∀s: PreStatus M code_memory. ∀d: Byte. ∀v: Byte.
266        Σp: PreStatus M code_memory. ∀M. ∀sigma. ∀policy.
267 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
268  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
269  (status_of_pseudo_status M code_memory s sigma policy) d v
270  =status_of_pseudo_status M code_memory
271   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
272  whd in match set_bit_addressable_sfr; normalize nodelta
273  @(let M ≝ pseudo_assembly_program in
274  λcode_memory:M.
275  λs: PreStatus M code_memory.
276  λb: Byte.
277  λv: Byte.
278    let address ≝ nat_of_bitvector … b in
279      if (eqb address 128) then
280        match not_implemented in False with [ ]
281      else if (eqb address 144) then
282        let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
283        let status_2 ≝ set_p1_latch ?? s v in
284          status_2
285      else if (eqb address 160) then
286        match not_implemented in False with [ ]
287      else if (eqb address 176) then
288        let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
289        let status_2 ≝ set_p3_latch ?? s v in
290          status_2
291      else if (eqb address 153) then
292        set_8051_sfr ?? s SFR_SBUF v
293      else if (eqb address 138) then
294        set_8051_sfr ?? s SFR_TL0 v
295      else if (eqb address 139) then
296        set_8051_sfr ?? s SFR_TL1 v
297      else if (eqb address 140) then
298        set_8051_sfr ?? s SFR_TH0 v
299      else if (eqb address 141) then
300        set_8051_sfr ?? s SFR_TH1 v
301      else if (eqb address 200) then
302        set_8052_sfr ?? s SFR_T2CON v
303      else if (eqb address 202) then
304        set_8052_sfr ?? s SFR_RCAP2L v
305      else if (eqb address 203) then
306        set_8052_sfr ?? s SFR_RCAP2H v
307      else if (eqb address 204) then
308        set_8052_sfr ?? s SFR_TL2 v
309      else if (eqb address 205) then
310        set_8052_sfr ?? s SFR_TH2 v
311      else if (eqb address 135) then
312        set_8051_sfr ?? s SFR_PCON v
313      else if (eqb address 136) then
314        set_8051_sfr ?? s SFR_TCON v
315      else if (eqb address 137) then
316        set_8051_sfr ?? s SFR_TMOD v
317      else if (eqb address 152) then
318        set_8051_sfr ?? s SFR_SCON v
319      else if (eqb address 168) then
320        set_8051_sfr ?? s SFR_IE v
321      else if (eqb address 184) then
322        set_8051_sfr ?? s SFR_IP v
323      else if (eqb address 129) then
324        set_8051_sfr ?? s SFR_SP v
325      else if (eqb address 130) then
326        set_8051_sfr ?? s SFR_DPL v
327      else if (eqb address 131) then
328        set_8051_sfr ?? s SFR_DPH v
329      else if (eqb address 208) then
330        set_8051_sfr ?? s SFR_PSW v
331      else if (eqb address 224) then
332        set_8051_sfr ?? s SFR_ACC_A v
333      else if (eqb address 240) then
334        set_8051_sfr ?? s SFR_ACC_B v
335      else
336        match not_implemented in False with [ ])
337  normalize nodelta
338  #M #sigma #policy
339  [1,2: //
340  |3: //
341
342definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
343                                   acc_a ; acc_b ; ext_indirect ;
344                                   ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝
345  λm, cm, s, a, v.
346    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
347                                                acc_a ; acc_b ; ext_indirect ;
348                                                ext_indirect_dptr ]] x) →
349                   PreStatus m cm
350            with
351      [ DIRECT d ⇒
352        λdirect: True.
353          let 〈 nu, nl 〉 ≝ vsplit … 4 4 d in
354          let bit_one ≝ get_index_v ? ? nu 0 ? in
355          let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
356            match bit_one with
357              [ true ⇒ set_bit_addressable_sfr ?? s d v
358              | false ⇒
359                let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ?? s) in
360                  set_low_internal_ram ?? s memory
361              ]
362      | INDIRECT i ⇒
363        λindirect: True.
364          let register ≝ get_register ?? s [[ false; false; i ]] in
365          let 〈nu, nl〉 ≝ vsplit ? 4 4 register in
366          let bit_1 ≝ get_index_v … nu 0 ? in
367          let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in
368            match bit_1 with
369              [ false ⇒
370                let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ?? s) in
371                  set_low_internal_ram ?? s memory
372              | true ⇒
373                let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ?? s) in
374                  set_high_internal_ram ?? s memory
375              ]
376      | REGISTER r ⇒ λregister: True. set_register ?? s r v
377      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
378      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
379      | EXT_INDIRECT e ⇒
380        λext_indirect: True.
381          let address ≝ get_register ?? s [[ false; false; e ]] in
382          let padded_address ≝ pad 8 8 address in
383          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
384            set_external_ram ?? s memory
385      | EXT_INDIRECT_DPTR ⇒
386        λext_indirect_dptr: True.
387          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
388          let memory ≝ insert ? 16 address v (external_ram ?? s) in
389            set_external_ram ?? s memory
390      | _ ⇒
391        λother: False.
392          match other in False with [ ]
393      ] (subaddressing_modein … a).
394  //
395qed.
396
397lemma set_arg_8_status_of_pseudo_status:
398  ∀cm.
399  ∀ps.
400  ∀addr.
401  ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy.
402    set_arg_8 (BitVectorTrie Byte 16)
403      (code_memory_of_pseudo_assembly_program cm sigma policy)
404      (status_of_pseudo_status M cm ps sigma policy)
405      addr value =
406    status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
407  @(let m ≝ pseudo_assembly_program in λcm, s. λa: [[ direct ; indirect ; registr ;
408                                   acc_a ; acc_b ; ext_indirect ;
409                                   ext_indirect_dptr ]]. λv.
410    match a return λaddr. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
411                                                acc_a ; acc_b ; ext_indirect ;
412                                                ext_indirect_dptr ]] addr) →
413                   Σp: PreStatus m cm. ∀M. ∀sigma. ∀policy.
414    set_arg_8 (BitVectorTrie Byte 16)
415      (code_memory_of_pseudo_assembly_program cm sigma policy)
416      (status_of_pseudo_status M cm s sigma policy)
417      addr v =
418    status_of_pseudo_status M cm (set_arg_8 … cm s addr v) sigma policy
419            with
420      [ DIRECT d ⇒
421        λdirect: True.
422          let 〈 nu, nl 〉 ≝ vsplit … 4 4 d in
423          let bit_one ≝ get_index_v ? ? nu 0 ? in
424          let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
425            match bit_one with
426              [ true ⇒ set_bit_addressable_sfr ?? s d v
427              | false ⇒
428                let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ?? s) in
429                  set_low_internal_ram ?? s memory
430              ]
431      | INDIRECT i ⇒
432        λindirect: True.
433          let register ≝ get_register ?? s [[ false; false; i ]] in
434          let 〈nu, nl〉 ≝ vsplit ? 4 4 register in
435          let bit_1 ≝ get_index_v … nu 0 ? in
436          let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in
437            match bit_1 with
438              [ false ⇒
439                let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ?? s) in
440                  set_low_internal_ram ?? s memory
441              | true ⇒
442                let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ?? s) in
443                  set_high_internal_ram ?? s memory
444              ]
445      | REGISTER r ⇒ λregister: True. set_register ?? s r v
446      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
447      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
448      | EXT_INDIRECT e ⇒
449        λext_indirect: True.
450          let address ≝ get_register ?? s [[ false; false; e ]] in
451          let padded_address ≝ pad 8 8 address in
452          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
453            set_external_ram ?? s memory
454      | EXT_INDIRECT_DPTR ⇒
455        λext_indirect_dptr: True.
456          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
457          let memory ≝ insert ? 16 address v (external_ram ?? s) in
458            set_external_ram ?? s memory
459      | _ ⇒
460        λother: False.
461          match other in False with [ ]
462      ] (subaddressing_modein … a))
463  [3,6: // ]
464  [1:
465    #M #sigma #policy whd in ⊢ (??%(???%??));
466    @pair_elim #nu #nl #nu_nl_refl normalize nodelta
467    @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
468    cases (get_index_v bool ????) normalize nodelta
469qed.
Note: See TracBrowser for help on using the repository browser.