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 *)
166 change in ⊢ (? ? (? ? %) ?) with (3+20);
167 rewrite > breakpoint in ⊢ (? ? % ?);
168 whd in ⊢ (? ? (? % ?) ?);
169 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
170 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
171 with (byte_of_nat (S a));
172 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
174 (* instruction BEQ *)
175 change in ⊢ (? ? (? ? %) ?) with (3+17);
176 rewrite > breakpoint in ⊢ (? ? % ?);
177 whd in ⊢ (? ? (? % ?) ?);
178 letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
179 rewrite > K; clear K;
180 simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
181 (* instruction LDAd *)
182 change in ⊢ (? ? (? ? %) ?) with (3+14);
183 rewrite > breakpoint in ⊢ (? ? % ?);
184 whd in ⊢ (? ? (? % ?) ?);
185 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
186 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
187 change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte 〈x0, x0〉 (byte_of_nat (x*n)));
188 (* instruction DECd *)
189 change in ⊢ (? ? (? ? %) ?) with (5+9);
190 rewrite > breakpoint in ⊢ (? ? % ?);
191 whd in ⊢ (? ? (? % ?) ?);
192 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
193 rewrite > (eq_bpred_S_a_a ? H3);
194 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
195 normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
197 [2: rewrite > eq_minus_S_pred;
200 rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
201 (* instruction ADDd *)
202 change in ⊢ (? ? (? ? %) ?) with (3+6);
203 rewrite > breakpoint in ⊢ (? ? % ?);
204 whd in ⊢ (? ? (? % ?) ?);
205 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
206 (plusbytenc (byte_of_nat (x*n)) x);
207 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
208 (plusbytenc (byte_of_nat (x*n)) x);
209 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
210 change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
211 with (plusbytec (byte_of_nat (x*n)) x);
212 rewrite > plusbytenc_S;
213 (* instruction STAd *)
214 rewrite > (breakpoint ? 3 3);
215 whd in ⊢ (? ? (? % ?) ?);
216 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
217 (* instruction BRA *)
219 normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
222 [1,2,3,4,7: normalize; reflexivity
223 | change with (plusbytec #(x*n) x = plusbytec #(x*n) x);
226 simplify in ⊢ (? ? ? %);
227 change in ⊢ (? ? % ?) with
231 (update (update (mult_memory x y) 30 x) 31
232 (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
233 (byte_of_nat (nat_of_byte y-S n)))
237 (update (update (mult_memory x y) 30 x) 31
238 (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
239 (byte_of_nat (nat_of_byte y-S n)) 15))
240 (byte_of_nat (nat_of_byte x*S n)) a);
241 normalize in ⊢ (? ? (? ? % ? ?) ?);
246 rewrite > not_eq_a_b_to_eq_update_a_b; [2: apply H | ];
247 rewrite > not_eq_a_b_to_eq_update_a_b;
255 [ rewrite < (minus_S_S y n);
256 apply (minus_Sn_m (nat_of_byte y) (S n) H1)
257 | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
258 letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
264 | rewrite > associative_plus;
265 rewrite < times_n_Sm;
266 rewrite > sym_plus in ⊢ (? ? ? (? ? %));
275 let i ≝ 14 + 23 * y in
276 execute (mult_status x y) i =
277 mk_status (#(x*y)) 20 0
278 (eqbyte 〈x0, x0〉 (#(x*y)))
279 (plusbytec (byte_of_nat (x*pred y)) x)
281 (update (mult_memory x y) 31 〈x0, x0〉)
282 32 (byte_of_nat (x*y)))
285 cut (14 + 23 * y = 5 + 23*y + 9);
286 [2: autobatch paramodulation;
287 | rewrite > Hcut; (* clear Hcut; *)
288 rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
289 rewrite > loop_invariant';
291 | rewrite < minus_n_n;
293 [1,2,3,4,5,7: normalize; reflexivity
295 letin xxx \def ((mult_memory x y) { a ↦ x }).
296 change with (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat O)) 32
297 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a =
298 update (update (mult_memory x y) 31 〈x0, x0〉) 32
299 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a);
300 apply inj_update; intro;
301 apply inj_update; intro;
302 change in ⊢ (? ? (? ? ? % ?) ?) with (mult_memory x y 30);
303 apply eq_update_s_a_sa