]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/freescale/tests.old
An unimplemented case of clearbody is now implemented.
[helm.git] / helm / software / matita / library / freescale / tests.old
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
15 (* ********************************************************************** *)
16 (*                           Progetto FreeScale                           *)
17 (*                                                                        *)
18 (* Sviluppato da:                                                         *)
19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
20 (*                                                                        *)
21 (* Questo materiale fa parte della tesi:                                  *)
22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
23 (*                                                                        *)
24 (*                    data ultima modifica 15/11/2007                     *)
25 (* ********************************************************************** *)
26
27 set "baseuri" "cic:/matita/freescale/tests/".
28
29 (*include "/media/VIRTUOSO/freescale/micro_tests.ma".*)
30 include "freescale/micro_tests.ma".
31
32 (* 
33    RAM indirizzabile in modalita' diretta da usare per X,Y,Z
34    A=X*Y (parte low) con [0x0020-0x004F] X ≝ [0x0020] Y ≝ [0x0021] Z ≝ [0x0022]
35 *)
36 definition test_mult_source_RS08 : list byte8 ≝
37 let m ≝ RS08 in source_to_byte8 m (
38 (* [0x3800] Z <- 0      3clk *) (compile m ? CLR (maDIR1 〈x2,x2〉) I) @
39 (* [0x3802] (l1) A <- Y 3clk *) (compile m ? LDA (maDIR1 〈x2,x1〉) I) @
40 (* [0x3804] A=0 goto l2 3clk *) (compile m ? BEQ (maIMM1 〈x0,xA〉) I) @
41 (* [0x3806] A <- Z      3clk *) (compile m ? LDA (maDIR1 〈x2,x2〉) I) @
42 (* [0x3808] Y --        5clk *) (compile m ? DEC (maDIR1 〈x2,x1〉) I) @
43 (* [0x380A] A += X      3clk *) (compile m ? ADD (maDIR1 〈x2,x0〉) I) @
44 (* [0x380C] Z <- A      3clk *) (compile m ? STA (maDIR1 〈x2,x2〉) I) @
45 (* [0x380E] goto l1     3clk *) (compile m ? BRA (maIMM1 〈xF,x2〉) I) @
46 (* [0x3810] (l2) A <- Z 3clk *) (compile m ? LDA (maDIR1 〈x2,x2〉) I)
47  ).
48
49 (* ************** *)
50 (* *****TODO***** *)
51 (* ************** *)
52
53 definition mult_memory ≝
54  λx,y.λa:addr.
55      match leb a 29 with
56       [ true ⇒ nth ? mult_source 〈x0, x0〉 a
57       | false ⇒
58          match eqb a 30 with
59           [ true ⇒ x
60           | false ⇒ y
61           ]
62       ].
63
64 definition mult_status ≝
65  λx,y.
66   mk_status 〈x0, x0〉 0 0 false false (mult_memory x y) 0.
67
68 notation " 'M' \sub (x y)" non associative with precedence 80 for 
69  @{ 'memory $x $y }.
70  
71 interpretation "mult_memory" 'memory x y = 
72   (cic:/matita/freescale/test/mult_memory.con x y).
73
74 notation " 'M' \sub (x y) \nbsp a" non associative with precedence 80 for 
75  @{ 'memory4 $x $y $a }.
76  
77 interpretation "mult_memory4" 'memory4 x y a = 
78   (cic:/matita/freescale/test/mult_memory.con x y a).
79   
80 notation " \Sigma \sub (x y)" non associative with precedence 80 for 
81  @{ 'status $x $y }.
82
83 interpretation "mult_status" 'status x y =
84   (cic:/matita/freescale/test/mult_status.con x y).
85
86 lemma test_O_O:
87   let i ≝ 14 in
88   let s ≝ execute (mult_status 〈x0, x0〉 〈x0, x0〉) i in
89    pc s = 20 ∧ mem s 32 = byte_of_nat 0.
90  split;
91  reflexivity.
92 qed.
93
94 lemma test_0_2:
95   let x ≝ 〈x0, x0〉 in
96   let y ≝ 〈x0, x2〉 in
97   let i ≝ 14 + 23 * nat_of_byte y in
98   let s ≝ execute (mult_status x y) i in
99    pc s = 20 ∧ mem s 32 = plusbytenc x x.
100  intros;
101  split;
102  reflexivity.
103 qed.
104
105 lemma test_x_1:
106  ∀x.
107   let y ≝ 〈x0, x1〉 in
108   let i ≝ 14 + 23 * nat_of_byte y in
109   let s ≝ execute (mult_status x y) i in
110    pc s = 20 ∧ mem s 32 = x.
111  intros;
112  split;
113   [ reflexivity
114   | change in ⊢ (? ? % ?) with (plusbytenc 〈x0, x0〉 x);
115     rewrite > plusbytenc_O_x;
116     reflexivity
117   ].
118 qed.
119
120 lemma test_x_2:
121  ∀x.
122   let y ≝ 〈x0, x2〉 in
123   let i ≝ 14 + 23 * nat_of_byte y in
124   let s ≝ execute (mult_status x y) i in
125    pc s = 20 ∧ mem s 32 = plusbytenc x x.
126  intros;
127  split;
128   [ reflexivity
129   | change in ⊢ (? ? % ?) with
130      (plusbytenc (plusbytenc 〈x0, x0〉 x) x);
131     rewrite > plusbytenc_O_x;
132     reflexivity
133   ].
134 qed.
135
136 lemma loop_invariant':
137  ∀x,y:byte.∀j:nat. j ≤ y →
138   execute (mult_status x y) (5 + 23*j)
139    =
140     mk_status (byte_of_nat (x * j)) 4 0 (eqbyte 〈x0, x0〉 (byte_of_nat (x*j)))
141      (plusbytec (byte_of_nat (x*pred j)) x)
142      (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
143       (byte_of_nat (x * j)))
144      0.
145  intros 3;
146  elim j;
147   [ do 2 (rewrite < times_n_O);
148     apply status_eq;
149     [1,2,3,4,7: normalize; reflexivity
150     | rewrite > eq_plusbytec_x0_x0_x_false;
151       normalize;
152       reflexivity 
153     | intro;
154       rewrite < minus_n_O;
155       normalize in ⊢ (? ? (? (? ? %) ?) ?);
156       change in ⊢ (? ? % ?) with (update (mult_memory x y) 32 〈x0, x0〉 a);
157       simplify in ⊢ (? ? ? %);
158       change in ⊢ (? ? ? (? (? (? ? ? %) ? ?) ? ? ?)) with (mult_memory x y 30);
159       rewrite > byte_of_nat_nat_of_byte;
160       change in ⊢ (? ? ? (? (? ? ? %) ? ? ?)) with (mult_memory x y 31);
161       apply inj_update;
162       intro;
163       rewrite > (eq_update_s_a_sa (update (mult_memory x y) 30 (mult_memory x y 30))
164        31 a);
165       rewrite > eq_update_s_a_sa;
166       reflexivity
167     ]
168   | cut (5 + 23 * S n = 5 + 23 * n + 23);
169     [ rewrite > Hcut; clear Hcut;
170       rewrite > breakpoint;
171       rewrite > H; clear H;
172       [2: apply le_S_S_to_le;
173         apply le_S;
174         apply H1
175       | cut (∃z.y-n=S z ∧ z < 255);
176          [ elim Hcut; clear Hcut;
177            elim H; clear H;
178            rewrite > H2;
179            (* instruction LDAd *)
180            change in ⊢ (? ? (? ? %) ?) with (3+20);
181            rewrite > breakpoint in ⊢ (? ? % ?);
182            whd in ⊢ (? ? (? % ?) ?);
183            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
184            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
185             with (byte_of_nat (S a));
186            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
187             (byte_of_nat (S a));
188            (* instruction BEQ *)
189            change in ⊢ (? ? (? ? %) ?) with (3+17);
190            rewrite > breakpoint in ⊢ (? ? % ?);
191            whd in ⊢ (? ? (? % ?) ?);
192            letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
193            rewrite > K; clear K;
194            simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
195            (* instruction LDAd *)
196            change in ⊢ (? ? (? ? %) ?) with (3+14);
197            rewrite > breakpoint in ⊢ (? ? % ?);
198            whd in ⊢ (? ? (? % ?) ?);
199            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
200            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
201            change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte 〈x0, x0〉 (byte_of_nat (x*n)));
202            (* instruction DECd *)
203            change in ⊢ (? ? (? ? %) ?) with (5+9);
204            rewrite > breakpoint in ⊢ (? ? % ?);
205            whd in ⊢ (? ? (? % ?) ?);
206            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
207            rewrite > (eq_bpred_S_a_a ? H3);
208            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
209            normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
210            cut (y - S n = a);
211             [2: rewrite > eq_minus_S_pred;
212                 rewrite > H2;
213                 reflexivity | ];
214            rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;          
215            (* instruction ADDd *)
216            change in ⊢ (? ? (? ? %) ?) with (3+6);
217            rewrite > breakpoint in ⊢ (? ? % ?);
218            whd in ⊢ (? ? (? % ?) ?);
219            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
220             (plusbytenc (byte_of_nat (x*n)) x);
221            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
222             (plusbytenc (byte_of_nat (x*n)) x);
223            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
224            change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
225             with (plusbytec (byte_of_nat (x*n)) x);
226            rewrite > plusbytenc_S;
227            (* instruction STAd *)
228            rewrite > (breakpoint ? 3 3);
229            whd in ⊢ (? ? (? % ?) ?);
230            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
231            (* instruction BRA *)
232            whd in ⊢ (? ? % ?);
233            normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
234            rewrite < pred_Sn;        
235            apply status_eq;
236             [1,2,3,4,7: normalize; reflexivity
237             | change with (plusbytec #(x*n) x = plusbytec #(x*n) x);
238               reflexivity
239             |6: intro;
240               simplify in ⊢ (? ? ? %);
241               normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? (? %) ?) ?) ?) ?);
242               change in ⊢ (? ? % ?) with
243                ((mult_memory x y){30↦x}{31↦#(S (y-S n))}{32↦#(x*n)}{31↦#(y-S n)}
244                 {〈x2,x0〉↦ #(x*S n)} a);
245               apply inj_update;
246               intro;
247               apply inj_update;
248               intro;
249               rewrite > not_eq_a_b_to_eq_update_a_b; [2: apply H | ];
250               rewrite > not_eq_a_b_to_eq_update_a_b;
251                [ reflexivity
252                | assumption
253                ]
254             ]
255          | exists;
256             [ apply (y - S n)
257             | split;
258                [ rewrite < (minus_S_S y n);
259                  apply (minus_Sn_m (nat_of_byte y) (S n) H1)
260                | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
261                  letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
262                  [ apply (lt_to_le_to_lt O (S n) (nat_of_byte y) ? ?);
263                    autobatch
264                  | autobatch
265                  | autobatch
266                  ]
267                ]
268             ]
269          ]
270       ]
271     | rewrite > associative_plus;
272       rewrite < times_n_Sm;
273       rewrite > sym_plus in ⊢ (? ? ? (? ? %));
274       reflexivity
275     ] 
276   ]   
277 qed.
278
279
280 theorem test_x_y:
281  ∀x,y:byte.
282   let i ≝ 14 + 23 * y in
283    execute (mult_status x y) i =
284     mk_status (#(x*y)) 20 0
285      (eqbyte 〈x0, x0〉 (#(x*y)))
286      (plusbytec (byte_of_nat (x*pred y)) x)
287      (update
288        (update (mult_memory x y) 31 〈x0, x0〉)
289        32 (byte_of_nat (x*y)))
290      0.
291  intros;
292  cut (14 + 23 * y = 5 + 23*y + 9);
293   [2: autobatch paramodulation;
294   | rewrite > Hcut; (* clear Hcut; *)
295     rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
296     rewrite > loop_invariant';
297      [2: apply le_n
298      | rewrite < minus_n_n;
299        apply status_eq;
300         [1,2,3,4,5,7: normalize; reflexivity
301         | intro;
302           simplify in ⊢ (? ? ? %);
303           change in ⊢ (? ? % ?) with
304            (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat O)) 32
305 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a);
306           repeat (apply inj_update; intro);
307           apply (eq_update_s_a_sa ? 30)
308         ]
309      ]
310   ].
311 qed.