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/byte".
17 include "assembly/exadecimal.ma".
19 record byte : Type ≝ {
24 notation "〈 x, y 〉" non associative with precedence 80 for @{ 'mk_byte $x $y }.
25 interpretation "mk_byte" 'mk_byte x y =
26 (cic:/matita/assembly/byte/byte.ind#xpointer(1/1/1) x y).
29 λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
33 match plusex (bl b1) (bl b2) c with
35 match plusex (bh b1) (bh b2) c' with
36 [ couple h c'' ⇒ couple ? ? (mk_byte h l) c'' ]].
38 definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
40 coercion cic:/matita/assembly/byte/nat_of_byte.con.
42 definition byte_of_nat ≝
43 λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
45 interpretation "byte_of_nat" 'byte_of_opcode a =
46 (cic:/matita/assembly/byte/byte_of_nat.con a).
48 lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
56 lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256.
59 letin H ≝ (lt_nat_of_exadecimal_16 (bh b)); clearbody H;
60 letin K ≝ (lt_nat_of_exadecimal_16 (bl b)); clearbody K;
62 letin H' ≝ (le_S_S_to_le ? ? H); clearbody H'; clear H;
63 letin K' ≝ (le_S_S_to_le ? ? K); clearbody K'; clear K;
65 cut (16*bh b ≤ 16*15);
66 [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
67 simplify in Hf:(? ? %);
69 | apply le_times_r. apply H'.
73 lemma nat_of_byte_byte_of_nat: ∀n. nat_of_byte (byte_of_nat n) = n \mod 256.
75 letin H ≝ (lt_nat_of_byte_256 (byte_of_nat n)); clearbody H;
76 rewrite < (lt_to_eq_mod ? ? H); clear H;
79 change with ((16*(exadecimal_of_nat (n/16)) + exadecimal_of_nat n) \mod 256 = n \mod 256);
80 letin H ≝ (div_mod n 16 ?); clearbody H; [ autobatch | ];
81 rewrite > symmetric_times in H;
82 rewrite > nat_of_exadecimal_exadecimal_of_nat in ⊢ (? ? (? (? % ?) ?) ?);
83 rewrite > nat_of_exadecimal_exadecimal_of_nat in ⊢ (? ? (? (? ? %) ?) ?);
84 rewrite > H in ⊢ (? ? ? (? % ?)); clear H;
85 rewrite > mod_plus in ⊢ (? ? % ?);
86 rewrite > mod_plus in ⊢ (? ? ? %);
87 apply eq_mod_to_eq_plus_mod;
88 rewrite < mod_mod in ⊢ (? ? ? %); [ | autobatch];
89 rewrite < mod_mod in ⊢ (? ? % ?); [ | autobatch];
90 rewrite < (eq_mod_times_times_mod ? ? 16 256) in ⊢ (? ? (? % ?) ?); [2: reflexivity | ];
91 rewrite < mod_mod in ⊢ (? ? % ?);
97 lemma eq_nat_of_byte_n_nat_of_byte_mod_n_256:
98 ∀n. byte_of_nat n = byte_of_nat (n \mod 256).
102 [ rewrite > exadecimal_of_nat_mod in ⊢ (? ? % ?);
103 rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
106 | rewrite > exadecimal_of_nat_mod;
107 rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
108 rewrite > divides_to_eq_mod_mod_mod;
110 | apply (witness ? ? 16). reflexivity.
117 match plusbyte b1 b2 c with
118 [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c' * 256
123 generalize in match (plusex_ok (bl b1) (bl b2) c);
124 elim (plusex (bl b1) (bl b2) c);
126 generalize in match (plusex_ok (bh b1) (bh b2) t1);
127 elim (plusex (bh b1) (bh b2) t1);
129 change in ⊢ (? ? ? (? (? % ?) ?)) with (16 * t2);
131 letin K ≝ (eq_f ? ? (λy.16*y) ? ? H1); clearbody K; clear H1;
132 rewrite > distr_times_plus in K:(? ? ? %);
133 rewrite > symmetric_times in K:(? ? ? (? ? (? ? %)));
134 rewrite < associative_times in K:(? ? ? (? ? %));
135 normalize in K:(? ? ? (? ? (? % ?)));
136 rewrite > symmetric_times in K:(? ? ? (? ? %));
137 rewrite > sym_plus in ⊢ (? ? ? (? % ?));
138 rewrite > associative_plus in ⊢ (? ? ? %);
139 letin K' ≝ (eq_f ? ? (plus t) ? ? K); clearbody K'; clear K;
140 apply transitive_eq; [3: apply K' | skip | ];
142 rewrite > sym_plus in ⊢ (? ? (? (? ? %) ?) ?);
143 rewrite > associative_plus in ⊢ (? ? (? % ?) ?);
144 rewrite > associative_plus in ⊢ (? ? % ?);
145 rewrite > associative_plus in ⊢ (? ? (? ? %) ?);
146 rewrite > associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
147 rewrite > sym_plus in ⊢ (? ? (? ? (? ? (? ? %))) ?);
148 rewrite < associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
149 rewrite < associative_plus in ⊢ (? ? (? ? %) ?);
150 rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?);
151 rewrite > H; clear H;
152 autobatch paramodulation.
158 match eqex (bl b) x0 with
159 [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
160 | false ⇒ mk_byte (bh b) (xpred (bl b))
164 ∀b. plusbyte (mk_byte x0 x0) b false = couple ? ? b false.
172 definition plusbytenc ≝
174 match plusbyte x y false with
175 [couple res _ ⇒ res].
177 definition plusbytec ≝
179 match plusbyte x y false with
182 lemma plusbytenc_O_x:
183 ∀x. plusbytenc (mk_byte x0 x0) x = x.
186 rewrite > plusbyte_O_x;
190 lemma eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256.
192 lapply (lt_nat_of_byte_256 b);
193 rewrite > (lt_to_eq_mod ? ? Hletin) in ⊢ (? ? ? %);
197 theorem plusbytenc_ok:
198 ∀b1,b2:byte. nat_of_byte (plusbytenc b1 b2) = (b1 + b2) \mod 256.
201 generalize in match (plusbyte_ok b1 b2 false);
202 elim (plusbyte b1 b2 false);
204 change with (nat_of_byte t = (b1 + b2) \mod 256);
205 rewrite < plus_n_O in H;
206 rewrite > H; clear H;
208 letin K ≝ (eq_nat_of_byte_mod t); clearbody K;
209 letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K';
211 autobatch paramodulation.
216 lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
217 ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b)) = false.
220 cut (b < 15 ∨ b ≥ 15);
223 change in ⊢ (? ? (? ? %) ?) with (eqex x0 (exadecimal_of_nat (S b)));
224 rewrite > eq_eqex_S_x0_false;
225 [ elim (eqex (bh (mk_byte x0 x0))
226 (bh (mk_byte (exadecimal_of_nat (S b/16)) (exadecimal_of_nat (S b)))));
232 change in ⊢ (? ? (? % ?) ?) with (eqex x0 (exadecimal_of_nat (S b/16)));
233 letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?);
241 rewrite > eq_eqex_S_x0_false;
246 clear H2; clear a; clear H1; clear Hcut;
247 apply (le_times_to_le 16) [ autobatch | ] ;
248 rewrite > (div_mod (S b) 16) in H;[2:autobatch|]
249 rewrite > (div_mod 255 16) in H:(? ? %);[2:autobatch|]
250 lapply (le_to_le_plus_to_le ? ? ? ? ? H);
252 apply lt_mod_m_m;autobatch
253 |rewrite > sym_times;
254 rewrite > sym_times in ⊢ (? ? %); (* just to speed up qed *)
255 normalize in ⊢ (? ? %);apply Hletin;
260 | elim (or_lt_le b 15);unfold ge;autobatch
264 axiom eq_mod_O_to_exists: ∀n,m. n \mod m = 0 → ∃z. n = z*m.
266 lemma eq_bpred_S_a_a:
267 ∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a.
270 apply (bool_elim ? (eqex (bl (byte_of_nat (S a))) x0)); intros;
271 [ change with (mk_byte (xpred (bh (byte_of_nat (S a)))) (xpred (bl (byte_of_nat (S a))))
273 rewrite > (eqex_true_to_eq ? ? H1);
274 normalize in ⊢ (? ? (? ? %) ?);
276 change with (mk_byte (xpred (exadecimal_of_nat (S a/16))) xF =
277 mk_byte (exadecimal_of_nat (a/16)) (exadecimal_of_nat a));
278 lapply (eqex_true_to_eq ? ? H1); clear H1;
279 unfold byte_of_nat in Hletin;
280 change in Hletin with (exadecimal_of_nat (S a) = x0);
281 lapply (eq_f ? ? nat_of_exadecimal ? ? Hletin); clear Hletin;
282 normalize in Hletin1:(? ? ? %);
283 rewrite > nat_of_exadecimal_exadecimal_of_nat in Hletin1;
284 elim (eq_mod_O_to_exists ? ? Hletin1); clear Hletin1;
286 rewrite > div_times_ltO; [2: autobatch | ]
287 lapply (eq_f ? ? (λx.x/16) ? ? H1);
288 rewrite > div_times_ltO in Hletin; [2: autobatch | ]
289 lapply (eq_f ? ? (λx.x \mod 16) ? ? H1);
290 rewrite > eq_mod_times_n_m_m_O in Hletin1;
292 | change with (mk_byte (bh (byte_of_nat (S a))) (xpred (bl (byte_of_nat (S a))))
295 change with (mk_byte (exadecimal_of_nat (S a/16)) (xpred (exadecimal_of_nat (S a)))
296 = mk_byte (exadecimal_of_nat (a/16)) (exadecimal_of_nat a));
297 lapply (eqex_false_to_not_eq ? ? H1);
298 unfold byte_of_nat in Hletin;
299 change in Hletin with (exadecimal_of_nat (S a) ≠ x0);
300 cut (nat_of_exadecimal (exadecimal_of_nat (S a)) ≠ 0);
303 lapply (eq_f ? ? exadecimal_of_nat ? ? H2);
304 rewrite > exadecimal_of_nat_nat_of_exadecimal in Hletin1;
313 ∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n).
315 rewrite < byte_of_nat_nat_of_byte;
316 rewrite > (plusbytenc_ok (byte_of_nat (x*n)) x);
317 rewrite < times_n_Sm;
318 rewrite > nat_of_byte_byte_of_nat in ⊢ (? ? (? (? (? % ?) ?)) ?);
319 rewrite > eq_nat_of_byte_n_nat_of_byte_mod_n_256 in ⊢ (? ? ? %);
320 rewrite > mod_plus in ⊢ (? ? (? %) ?);
321 rewrite > mod_plus in ⊢ (? ? ? (? %));
322 rewrite < mod_mod in ⊢ (? ? (? (? (? % ?) ?)) ?); [2: autobatch | ];
323 rewrite > sym_plus in ⊢ (? ? (? (? % ?)) ?);
327 lemma eq_plusbytec_x0_x0_x_false:
328 ∀x.plusbytec (mk_byte x0 x0) x = false.