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 ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
218 rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
219 (* instruction ADDd *)
222 (mk_status (byte_of_nat (x*n)) 12
223 O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n)))
224 (plusbytec (byte_of_nat (x*pred n)) x)
226 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
227 32 (byte_of_nat (x*n))) 31
228 (byte_of_nat (y-S n))) O)
230 normalize in K:(? ? (? ? %) ?);
231 apply transitive_eq; [2: apply K | skip | ]; clear K;
232 whd in ⊢ (? ? (? % ?) ?);
233 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
234 (plusbytenc (byte_of_nat (x*n)) x);
235 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
236 (plusbytenc (byte_of_nat (x*n)) x);
237 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
238 change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
239 with (plusbytec (byte_of_nat (x*n)) x);
240 rewrite > plusbytenc_S;
241 (* instruction STAd *)
244 (mk_status (byte_of_nat (x*S n)) 14 O
245 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n)))
246 (plusbytec (byte_of_nat (x*n)) x)
248 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
249 32 (byte_of_nat (x*n))) 31
250 (byte_of_nat (y-S n))) O)
252 normalize in K:(? ? (? ? %) ?);
253 apply transitive_eq; [2: apply K | skip | ]; clear K;
254 whd in ⊢ (? ? (? % ?) ?);
255 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
256 (* instruction BRA *)
258 normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
261 [1,2,3,4,7: normalize; reflexivity
262 | change with (plusbytec (byte_of_nat (x*n)) x =
263 plusbytec (byte_of_nat (x*n)) x);
266 simplify in ⊢ (? ? ? %);
267 change in ⊢ (? ? % ?) with
271 (update (update (mult_memory x y) 30 x) 31
272 (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
273 (byte_of_nat (nat_of_byte y-S n)))
277 (update (update (mult_memory x y) 30 x) 31
278 (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
279 (byte_of_nat (nat_of_byte y-S n)) 15))
280 (byte_of_nat (nat_of_byte x*S n)) a);
281 normalize in ⊢ (? ? (? ? % ? ?) ?);
286 rewrite > not_eq_a_b_to_eq_update_a_b in ⊢ (? ? % ?); [2: apply H | ];
287 rewrite > not_eq_a_b_to_eq_update_a_b in ⊢ (? ? % ?);
295 [ rewrite < (minus_S_S y n);
297 | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
298 letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
304 | rewrite > associative_plus;
305 rewrite < times_n_Sm;
306 rewrite > sym_plus in ⊢ (? ? ? (? ? %));
314 let i ≝ 14 + 23 * y in
315 execute (mult_status x y) i =
316 mk_status (byte_of_nat (x*y)) 20 0
317 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*y)))
318 (plusbytec (byte_of_nat (x*pred y)) x)
320 (update (mult_memory x y) 31 (mk_byte x0 x0))
321 32 (byte_of_nat (x*y)))
324 cut (14 + 23 * y = 5 + 23*y + 9);
325 [2: autobatch paramodulation;
326 | rewrite > Hcut; (* clear Hcut; *)
327 rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
328 rewrite > loop_invariant';
330 | rewrite < minus_n_n;
332 [1,2,3,4,5,7: normalize; reflexivity
334 change with (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat O)) 32
335 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a =
336 update (update (mult_memory x y) 31 (mk_byte x0 x0)) 32
337 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a);
338 apply inj_update; intro;
339 apply inj_update; intro;
340 change in ⊢ (? ? (? ? ? % ?) ?) with (mult_memory x y 30);
341 apply eq_update_s_a_sa