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 simplify in ⊢ (? ? ? %);
136 change in ⊢ (? ? ? (? (? (? ? ? %) ? ?) ? ? ?)) with (mult_memory x y 30);
137 rewrite > byte_of_nat_nat_of_byte;
138 change in ⊢ (? ? ? (? (? ? ? %) ? ? ?)) with (mult_memory x y 31);
141 rewrite > (eq_update_s_a_sa (update (mult_memory x y) 30 (mult_memory x y 30))
143 rewrite > eq_update_s_a_sa;
146 | cut (5 + 23 * S n = 5 + 23 * n + 23);
147 [ rewrite > Hcut; clear Hcut;
148 rewrite > breakpoint;
149 rewrite > H; clear H;
150 [2: apply le_S_S_to_le;
153 | cut (∃z.y-n=S z ∧ z < 255);
154 [ elim Hcut; clear Hcut;
157 (* instruction LDAd *)
158 change in ⊢ (? ? (? ? %) ?) with (3+20);
159 rewrite > breakpoint in ⊢ (? ? % ?);
160 whd in ⊢ (? ? (? % ?) ?);
161 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
162 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
163 with (byte_of_nat (S a));
164 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
166 (* instruction BEQ *)
167 change in ⊢ (? ? (? ? %) ?) with (3+17);
168 rewrite > breakpoint in ⊢ (? ? % ?);
169 whd in ⊢ (? ? (? % ?) ?);
170 letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
171 rewrite > K; clear K;
172 simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
173 (* instruction LDAd *)
174 change in ⊢ (? ? (? ? %) ?) with (3+14);
175 rewrite > breakpoint in ⊢ (? ? % ?);
176 whd in ⊢ (? ? (? % ?) ?);
177 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
178 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
179 change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte 〈x0, x0〉 (byte_of_nat (x*n)));
180 (* instruction DECd *)
181 change in ⊢ (? ? (? ? %) ?) with (5+9);
182 rewrite > breakpoint in ⊢ (? ? % ?);
183 whd in ⊢ (? ? (? % ?) ?);
184 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
185 rewrite > (eq_bpred_S_a_a ? H3);
186 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
187 normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
189 [2: rewrite > eq_minus_S_pred;
192 rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
193 (* instruction ADDd *)
194 change in ⊢ (? ? (? ? %) ?) with (3+6);
195 rewrite > breakpoint in ⊢ (? ? % ?);
196 whd in ⊢ (? ? (? % ?) ?);
197 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
198 (plusbytenc (byte_of_nat (x*n)) x);
199 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
200 (plusbytenc (byte_of_nat (x*n)) x);
201 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
202 change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
203 with (plusbytec (byte_of_nat (x*n)) x);
204 rewrite > plusbytenc_S;
205 (* instruction STAd *)
206 rewrite > (breakpoint ? 3 3);
207 whd in ⊢ (? ? (? % ?) ?);
208 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
209 (* instruction BRA *)
211 normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
214 [1,2,3,4,7: normalize; reflexivity
215 | change with (plusbytec #(x*n) x = plusbytec #(x*n) x);
218 simplify in ⊢ (? ? ? %);
219 normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? (? %) ?) ?) ?) ?);
220 change in ⊢ (? ? % ?) with
221 ((mult_memory x y){30↦x}{31↦#(S (y-S n))}{32↦#(x*n)}{31↦#(y-S n)}
222 {〈x2,x0〉↦ #(x*S n)} a);
227 rewrite > not_eq_a_b_to_eq_update_a_b; [2: apply H | ];
228 rewrite > not_eq_a_b_to_eq_update_a_b;
236 [ rewrite < (minus_S_S y n);
237 apply (minus_Sn_m (nat_of_byte y) (S n) H1)
238 | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
239 letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
240 [ apply (lt_to_le_to_lt O (S n) (nat_of_byte y) ? ?);
249 | rewrite > associative_plus;
250 rewrite < times_n_Sm;
251 rewrite > sym_plus in ⊢ (? ? ? (? ? %));
260 let i ≝ 14 + 23 * y in
261 execute (mult_status x y) i =
262 mk_status (#(x*y)) 20 0
263 (eqbyte 〈x0, x0〉 (#(x*y)))
264 (plusbytec (byte_of_nat (x*pred y)) x)
266 (update (mult_memory x y) 31 〈x0, x0〉)
267 32 (byte_of_nat (x*y)))
270 cut (14 + 23 * y = 5 + 23*y + 9);
271 [2: autobatch paramodulation;
272 | rewrite > Hcut; (* clear Hcut; *)
273 rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
274 rewrite > loop_invariant';
276 | rewrite < minus_n_n;
278 [1,2,3,4,5,7: normalize; reflexivity
280 simplify in ⊢ (? ? ? %);
281 change in ⊢ (? ? % ?) with
282 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat O)) 32
283 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a);
284 repeat (apply inj_update; intro);
285 apply (eq_update_s_a_sa ? 30)