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/".
19 notation "hvbox(# break a)"
20 non associative with precedence 80
21 for @{ 'byte_of_opcode $a }.
22 interpretation "byte_of_opcode" 'byte_of_opcode a =
23 (cic:/matita/assembly/vm/byte_of_opcode.con a).
25 definition mult_source : list byte ≝
26 [#LDAi; mk_byte x0 x0; (* A := 0 *)
27 #STAd; mk_byte x2 x0; (* Z := A *)
28 #LDAd; mk_byte x1 xF; (* (l1) A := Y *)
29 #BEQ; mk_byte x0 xA; (* if A == 0 then goto l2 *)
30 #LDAd; mk_byte x2 x0; (* A := Z *)
31 #DECd; mk_byte x1 xF; (* Y := Y - 1 *)
32 #ADDd; mk_byte x1 xE; (* A += X *)
33 #STAd; mk_byte x2 x0; (* Z := A *)
34 #BRA; mk_byte xF x2; (* goto l1 *)
35 #LDAd; mk_byte x2 x0].(* (l2) *)
37 definition mult_memory ≝
40 [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
48 definition mult_status ≝
50 mk_status (mk_byte x0 x0) 0 0 false false (mult_memory x y) 0.
54 let s ≝ execute (mult_status (mk_byte x0 x0) (mk_byte x0 x0)) i in
55 pc s = 20 ∧ mem s 32 = byte_of_nat 0.
62 let x ≝ mk_byte x0 x0 in
63 let y ≝ mk_byte x0 x2 in
64 let i ≝ 14 + 23 * nat_of_byte y in
65 let s ≝ execute (mult_status x y) i in
66 pc s = 20 ∧ mem s 32 = plusbytenc x x.
74 let y ≝ mk_byte x0 x1 in
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 = x.
81 | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x);
82 rewrite > plusbytenc_O_x;
89 let y ≝ mk_byte x0 x2 in
90 let i ≝ 14 + 23 * nat_of_byte y in
91 let s ≝ execute (mult_status x y) i in
92 pc s = 20 ∧ mem s 32 = plusbytenc x x.
96 | change in ⊢ (? ? % ?) with
97 (plusbytenc (plusbytenc (mk_byte x0 x0) x) x);
98 rewrite > plusbytenc_O_x;
103 lemma loop_invariant':
104 ∀x,y:byte.∀j:nat. j ≤ y →
105 execute (mult_status x y) (5 + 23*j)
107 mk_status (byte_of_nat (x * j)) 4 0 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*j)))
108 (plusbytec (byte_of_nat (x*pred j)) x)
109 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
110 (byte_of_nat (x * j)))
114 [ do 2 (rewrite < times_n_O);
116 [1,2,3,4,7: normalize; reflexivity
117 | rewrite > eq_plusbytec_x0_x0_x_false;
122 normalize in ⊢ (? ? (? (? ? %) ?) ?);
124 change in ⊢ (? ? % ?) with (update (mult_memory x y) 32 (mk_byte x0 x0) a);
125 change in ⊢ (? ? ? %) with (update (update (update (mult_memory x y) 30 x) 31
126 (byte_of_nat y)) 32 (byte_of_nat 0) a);
127 change in ⊢ (? ? ? (? (? (? ? ? %) ? ?) ? ? ?)) with (mult_memory x y 30);
128 rewrite > byte_of_nat_nat_of_byte;
129 change in ⊢ (? ? ? (? (? ? ? %) ? ? ?)) with (mult_memory x y 31);
132 rewrite > (eq_update_s_a_sa (update (mult_memory x y) 30 (mult_memory x y 30))
133 31 a) in ⊢ (? ? ? %);
134 rewrite > eq_update_s_a_sa;
137 | cut (5 + 23 * S n = 5 + 23 * n + 23);
138 [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K;
139 letin H' ≝ (H ?); clearbody H'; clear H;
141 | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx;
145 apply (transitive_eq ? ? ? ? K);
149 cut (∃z.y-n=S z ∧ z < 255);
150 [ elim Hcut; clear Hcut;
153 (* instruction LDAd *)
156 (mk_status (byte_of_nat (x*n)) 4 O
157 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
158 (plusbytec (byte_of_nat (x*pred n)) x)
159 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
160 (byte_of_nat (x*n))) O)
162 normalize in K:(? ? (? ? %) ?);
163 apply transitive_eq; [2: apply K | skip | ]; clear K;
164 whd in ⊢ (? ? (? % ?) ?);
165 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
166 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
167 with (byte_of_nat (S a));
168 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
170 (* instruction BEQ *)
173 (mk_status (byte_of_nat (S a)) 6 O
174 (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
175 (plusbytec (byte_of_nat (x*pred n)) x)
176 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
177 (byte_of_nat (x*n))) O)
179 normalize in K:(? ? (? ? %) ?);
180 apply transitive_eq; [2: apply K | skip | ]; clear K;
181 whd in ⊢ (? ? (? % ?) ?);
182 letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
183 rewrite > K; clear K;
184 simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
185 (* instruction LDAd *)
188 (mk_status (byte_of_nat (S a)) 8 O
189 (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
190 (plusbytec (byte_of_nat (x*pred n)) x)
191 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
192 (byte_of_nat (x*n))) O)
194 normalize in K:(? ? (? ? %) ?);
195 apply transitive_eq; [2: apply K | skip | ]; clear K;
196 whd in ⊢ (? ? (? % ?) ?);
197 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
198 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
199 change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)));
200 (* instruction DECd *)
203 (mk_status (byte_of_nat (x*n)) 10 O
204 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
205 (plusbytec (byte_of_nat (x*pred n)) x)
206 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
207 (byte_of_nat (x*n))) O)
209 normalize in K:(? ? (? ? %) ?);
210 apply transitive_eq; [2: apply K | skip | ]; clear K;
211 whd in ⊢ (? ? (? % ?) ?);
212 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
213 rewrite > (eq_bpred_S_a_a ? H3);
214 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
215 normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
217 [2: rewrite > eq_minus_S_pred;
220 rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
221 (* instruction ADDd *)
224 (mk_status (byte_of_nat (x*n)) 12
225 O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n)))
226 (plusbytec (byte_of_nat (x*pred n)) x)
228 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
229 32 (byte_of_nat (x*n))) 31
230 (byte_of_nat (y-S n))) O)
232 normalize in K:(? ? (? ? %) ?);
233 apply transitive_eq; [2: apply K | skip | ]; clear K;
234 whd in ⊢ (? ? (? % ?) ?);
235 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
236 (plusbytenc (byte_of_nat (x*n)) x);
237 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
238 (plusbytenc (byte_of_nat (x*n)) x);
239 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
240 change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
241 with (plusbytec (byte_of_nat (x*n)) x);
242 rewrite > plusbytenc_S;
243 (* instruction STAd *)
246 (mk_status (byte_of_nat (x*S n)) 14 O
247 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n)))
248 (plusbytec (byte_of_nat (x*n)) x)
250 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
251 32 (byte_of_nat (x*n))) 31
252 (byte_of_nat (y-S n))) O)
254 normalize in K:(? ? (? ? %) ?);
255 apply transitive_eq; [2: apply K | skip | ]; clear K;
256 whd in ⊢ (? ? (? % ?) ?);
257 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
258 (* instruction BRA *)
260 normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
263 [1,2,3,4,7: normalize; reflexivity
264 | change with (plusbytec (byte_of_nat (x*n)) x =
265 plusbytec (byte_of_nat (x*n)) x);
268 simplify in ⊢ (? ? ? %);
269 change in ⊢ (? ? % ?) with
273 (update (update (mult_memory x y) 30 x) 31
274 (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
275 (byte_of_nat (nat_of_byte y-S n)))
279 (update (update (mult_memory x y) 30 x) 31
280 (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
281 (byte_of_nat (nat_of_byte y-S n)) 15))
282 (byte_of_nat (nat_of_byte x*S n)) a);
283 normalize in ⊢ (? ? (? ? % ? ?) ?);
288 rewrite > not_eq_a_b_to_eq_update_a_b in ⊢ (? ? % ?); [2: apply H | ];
289 rewrite > not_eq_a_b_to_eq_update_a_b in ⊢ (? ? % ?);
297 [ rewrite < (minus_S_S y n);
299 | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
300 letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
306 | rewrite > associative_plus;
307 rewrite < times_n_Sm;
308 rewrite > sym_plus in ⊢ (? ? ? (? ? %));
316 let i ≝ 14 + 23 * y in
317 execute (mult_status x y) i =
318 mk_status (byte_of_nat (x*y)) 20 0
319 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*y)))
320 (plusbytec (byte_of_nat (x*pred y)) x)
322 (update (mult_memory x y) 31 (mk_byte x0 x0))
323 32 (byte_of_nat (x*y)))
326 cut (14 + 23 * y = 5 + 23*y + 9);
327 [2: autobatch paramodulation;
328 | rewrite > Hcut; (* clear Hcut; *)
329 rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
330 rewrite > loop_invariant';
332 | rewrite < minus_n_n;
334 [1,2,3,4,5,7: normalize; reflexivity
336 change with (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat O)) 32
337 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a =
338 update (update (mult_memory x y) 31 (mk_byte x0 x0)) 32
339 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a);
340 apply inj_update; intro;
341 apply inj_update; intro;
342 change in ⊢ (? ? (? ? ? % ?) ?) with (mult_memory x y 30);
343 apply eq_update_s_a_sa