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;
123 | cut (5 + 23 * S n = 5 + 23 * n + 23);
124 [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K;
125 letin H' ≝ (H ?); clearbody H'; clear H;
127 | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx;
131 apply (transitive_eq ? ? ? ? K);
135 cut (∃z.y-n=S z ∧ z < 255);
136 [ elim Hcut; clear Hcut;
139 (* instruction LDAd *)
142 (mk_status (byte_of_nat (x*n)) 4 O
143 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
144 (plusbytec (byte_of_nat (x*pred n)) x)
145 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
146 (byte_of_nat (x*n))) O)
148 normalize in K:(? ? (? ? %) ?);
149 apply transitive_eq; [2: apply K | skip | ]; clear K;
150 whd in ⊢ (? ? (? % ?) ?);
151 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
152 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
153 with (byte_of_nat (S a));
154 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
156 (* instruction BEQ *)
159 (mk_status (byte_of_nat (S a)) 6 O
160 (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
161 (plusbytec (byte_of_nat (x*pred n)) x)
162 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
163 (byte_of_nat (x*n))) O)
165 normalize in K:(? ? (? ? %) ?);
166 apply transitive_eq; [2: apply K | skip | ]; clear K;
167 whd in ⊢ (? ? (? % ?) ?);
168 letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
169 rewrite > K; clear K;
170 simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
171 (* instruction LDAd *)
174 (mk_status (byte_of_nat (S a)) 8 O
175 (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
176 (plusbytec (byte_of_nat (x*pred n)) x)
177 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
178 (byte_of_nat (x*n))) O)
180 normalize in K:(? ? (? ? %) ?);
181 apply transitive_eq; [2: apply K | skip | ]; clear K;
182 whd in ⊢ (? ? (? % ?) ?);
183 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
184 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
185 change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)));
186 (* instruction DECd *)
189 (mk_status (byte_of_nat (x*n)) 10 O
190 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
191 (plusbytec (byte_of_nat (x*pred n)) x)
192 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
193 (byte_of_nat (x*n))) O)
195 normalize in K:(? ? (? ? %) ?);
196 apply transitive_eq; [2: apply K | skip | ]; clear K;
197 whd in ⊢ (? ? (? % ?) ?);
198 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
199 rewrite > (eq_bpred_S_a_a ? H3);
200 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
201 normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
204 rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
205 (* instruction ADDd *)
208 (mk_status (byte_of_nat (x*n)) 12
209 O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n)))
210 (plusbytec (byte_of_nat (x*pred n)) x)
212 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
213 32 (byte_of_nat (x*n))) 31
214 (byte_of_nat (y-S n))) O)
216 normalize in K:(? ? (? ? %) ?);
217 apply transitive_eq; [2: apply K | skip | ]; clear K;
218 whd in ⊢ (? ? (? % ?) ?);
219 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
220 (plusbytenc (byte_of_nat (x*n)) x);
221 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
222 (plusbytenc (byte_of_nat (x*n)) x);
223 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
224 change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
225 with (plusbytec (byte_of_nat (x*n)) x);
226 rewrite > plusbytenc_S;
227 (* instruction STAd *)
230 (mk_status (byte_of_nat (x*S n)) 14 O
231 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n)))
232 (plusbytec (byte_of_nat (x*n)) x)
234 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
235 32 (byte_of_nat (x*n))) 31
236 (byte_of_nat (y-S n))) O)
238 normalize in K:(? ? (? ? %) ?);
239 apply transitive_eq; [2: apply K | skip | ]; clear K;
240 whd in ⊢ (? ? (? % ?) ?);
241 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
242 (* instruction BRA *)
244 normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
247 [1,2,3,4,7: normalize; reflexivity
248 | change with (plusbytec (byte_of_nat (x*n)) x =
249 plusbytec (byte_of_nat (x*n)) x);
257 [ rewrite < (minus_S_S y n);
259 | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
260 letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
266 | rewrite > associative_plus;
267 autobatch paramodulation
274 let i ≝ 14 + 23 * y in
275 execute (mult_status x y) i =
276 mk_status (byte_of_nat (x*y)) 20 0
277 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*y)))
278 (plusbytec (byte_of_nat (x*pred y)) x)
280 (update (mult_memory x y) 31 (mk_byte x0 x0))
281 32 (byte_of_nat (x*y)))
284 cut (14 + 23 * y = 5 + 23*y + 9);
285 [2: autobatch paramodulation;
286 | rewrite > Hcut; (* clear Hcut; *)
287 rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
288 rewrite > loop_invariant';
290 | rewrite < minus_n_n;
292 [1,2,3,4,5,7: normalize; reflexivity