1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/assembly/test/".
17 include "assembly/vm.ma".
19 definition mult_source : list byte ≝
20 [#LDAi; 〈x0, x0〉; (* A := 0 *)
21 #STAd; 〈x2, x0〉; (* Z := A *)
22 #LDAd; 〈x1, xF〉; (* (l1) A := Y *)
23 #BEQ; 〈x0, xA〉; (* if A == 0 then goto l2 *)
24 #LDAd; 〈x2, x0〉; (* A := Z *)
25 #DECd; 〈x1, xF〉; (* Y := Y - 1 *)
26 #ADDd; 〈x1, xE〉; (* A += X *)
27 #STAd; 〈x2, x0〉; (* Z := A *)
28 #BRA; 〈xF, x2〉; (* goto l1 *)
29 #LDAd; 〈x2, x0〉].(* (l2) *)
31 definition mult_memory ≝
34 [ true ⇒ nth ? mult_source 〈x0, x0〉 a
42 definition mult_status ≝
44 mk_status 〈x0, x0〉 0 0 false false (mult_memory x y) 0.
46 notation " 'M' \sub (x y)" non associative with precedence 80 for
49 interpretation "mult_memory" 'memory x y =
50 (cic:/matita/assembly/test/mult_memory.con x y).
52 notation " 'M' \sub (x y) \nbsp a" non associative with precedence 80 for
53 @{ 'memory4 $x $y $a }.
55 interpretation "mult_memory4" 'memory4 x y a =
56 (cic:/matita/assembly/test/mult_memory.con x y a).
58 notation " \Sigma \sub (x y)" non associative with precedence 80 for
61 interpretation "mult_status" 'status x y =
62 (cic:/matita/assembly/test/mult_status.con x y).
66 let s ≝ execute (mult_status 〈x0, x0〉 〈x0, x0〉) i in
67 pc s = 20 ∧ mem s 32 = byte_of_nat 0.
75 let i ≝ 14 + 23 * nat_of_byte y in
76 let s ≝ execute (mult_status x y) i in
77 pc s = 20 ∧ mem s 32 = plusbytenc x x.
86 let i ≝ 14 + 23 * nat_of_byte y in
87 let s ≝ execute (mult_status x y) i in
88 pc s = 20 ∧ mem s 32 = x.
92 | change in ⊢ (? ? % ?) with (plusbytenc 〈x0, x0〉 x);
93 rewrite > plusbytenc_O_x;
101 let i ≝ 14 + 23 * nat_of_byte y in
102 let s ≝ execute (mult_status x y) i in
103 pc s = 20 ∧ mem s 32 = plusbytenc x x.
107 | change in ⊢ (? ? % ?) with
108 (plusbytenc (plusbytenc 〈x0, x0〉 x) x);
109 rewrite > plusbytenc_O_x;
114 lemma loop_invariant':
115 ∀x,y:byte.∀j:nat. j ≤ y →
116 execute (mult_status x y) (5 + 23*j)
118 mk_status (byte_of_nat (x * j)) 4 0 (eqbyte 〈x0, x0〉 (byte_of_nat (x*j)))
119 (plusbytec (byte_of_nat (x*pred j)) x)
120 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
121 (byte_of_nat (x * j)))
125 [ do 2 (rewrite < times_n_O);
127 [1,2,3,4,7: normalize; reflexivity
128 | rewrite > eq_plusbytec_x0_x0_x_false;
133 normalize in ⊢ (? ? (? (? ? %) ?) ?);
134 change in ⊢ (? ? % ?) with (update (mult_memory x y) 32 〈x0, x0〉 a);
135 change in ⊢ (? ? ? %) with (update (update (update (mult_memory x y) 30 x) 31
136 (byte_of_nat y)) 32 (byte_of_nat 0) a);
137 change in ⊢ (? ? ? (? (? (? ? ? %) ? ?) ? ? ?)) with (mult_memory x y 30);
138 rewrite > byte_of_nat_nat_of_byte;
139 change in ⊢ (? ? ? (? (? ? ? %) ? ? ?)) with (mult_memory x y 31);
142 rewrite > (eq_update_s_a_sa (update (mult_memory x y) 30 (mult_memory x y 30))
144 rewrite > eq_update_s_a_sa;
147 | cut (5 + 23 * S n = 5 + 23 * n + 23);
148 [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K;
149 letin H' ≝ (H ?); clearbody H'; clear H;
150 [ apply le_S_S_to_le;
153 | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx;
157 apply (transitive_eq ? ? ? ? K);
161 cut (∃z.y-n=S z ∧ z < 255);
162 [ elim Hcut; clear Hcut;
165 (* instruction LDAd *)
168 (mk_status (byte_of_nat (x*n)) 4 O
169 (eqbyte 〈x0, x0〉 (byte_of_nat (x*n)))
170 (plusbytec (byte_of_nat (x*pred n)) x)
171 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
172 (byte_of_nat (x*n))) O)
174 normalize in K:(? ? (? ? %) ?);
175 rewrite > K; clear K;
176 whd in ⊢ (? ? (? % ?) ?);
177 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
178 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
179 with (byte_of_nat (S a));
180 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
182 (* instruction BEQ *)
185 (mk_status (byte_of_nat (S a)) 6 O
186 (eqbyte 〈x0, x0〉 (byte_of_nat (S a)))
187 (plusbytec (byte_of_nat (x*pred n)) x)
188 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
189 (byte_of_nat (x*n))) O)
191 normalize in K:(? ? (? ? %) ?);
192 rewrite > K; clear K;
193 whd in ⊢ (? ? (? % ?) ?);
194 letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
195 rewrite > K; clear K;
196 simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
197 (* instruction LDAd *)
198 rewrite > (breakpoint ? 3 14);
199 whd in ⊢ (? ? (? % ?) ?);
200 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
201 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
202 change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte 〈x0, x0〉 (byte_of_nat (x*n)));
203 (* instruction DECd *)
204 rewrite > (breakpoint ? 5 9);
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 ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
211 [2: rewrite > eq_minus_S_pred;
214 rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
215 (* instruction ADDd *)
216 rewrite > (breakpoint ? 3 6);
217 whd in ⊢ (? ? (? % ?) ?);
218 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
219 (plusbytenc (byte_of_nat (x*n)) x);
220 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
221 (plusbytenc (byte_of_nat (x*n)) x);
222 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
223 change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
224 with (plusbytec (byte_of_nat (x*n)) x);
225 rewrite > plusbytenc_S;
226 (* instruction STAd *)
227 rewrite > (breakpoint ? 3 3);
228 whd in ⊢ (? ? (? % ?) ?);
229 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
230 (* instruction BRA *)
232 normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
235 [1,2,3,4,7: normalize; reflexivity
236 | change with (plusbytec (byte_of_nat (x*n)) x =
237 plusbytec (byte_of_nat (x*n)) x);
240 simplify in ⊢ (? ? ? %);
241 change in ⊢ (? ? % ?) with
245 (update (update (mult_memory x y) 30 x) 31
246 (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
247 (byte_of_nat (nat_of_byte y-S n)))
251 (update (update (mult_memory x y) 30 x) 31
252 (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
253 (byte_of_nat (nat_of_byte y-S n)) 15))
254 (byte_of_nat (nat_of_byte x*S n)) a);
255 normalize in ⊢ (? ? (? ? % ? ?) ?);
260 rewrite > not_eq_a_b_to_eq_update_a_b; [2: apply H | ];
261 rewrite > not_eq_a_b_to_eq_update_a_b;
269 [ rewrite < (minus_S_S y n);
270 apply (minus_Sn_m (nat_of_byte y) (S n) H1)
271 | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
272 letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
278 | rewrite > associative_plus;
279 rewrite < times_n_Sm;
280 rewrite > sym_plus in ⊢ (? ? ? (? ? %));
289 let i ≝ 14 + 23 * y in
290 execute (mult_status x y) i =
291 mk_status (#(x*y)) 20 0
292 (eqbyte 〈x0, x0〉 (#(x*y)))
293 (plusbytec (byte_of_nat (x*pred y)) x)
295 (update (mult_memory x y) 31 〈x0, x0〉)
296 32 (byte_of_nat (x*y)))
299 cut (14 + 23 * y = 5 + 23*y + 9);
300 [2: autobatch paramodulation;
301 | rewrite > Hcut; (* clear Hcut; *)
302 rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
303 rewrite > loop_invariant';
305 | rewrite < minus_n_n;
307 [1,2,3,4,5,7: normalize; reflexivity
309 letin xxx \def ((mult_memory x y) { a ↦ x }).
310 change with (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat O)) 32
311 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a =
312 update (update (mult_memory x y) 31 〈x0, x0〉) 32
313 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a);
314 apply inj_update; intro;
315 apply inj_update; intro;
316 change in ⊢ (? ? (? ? ? % ?) ?) with (mult_memory x y 30);
317 apply eq_update_s_a_sa