matita/library/assembly/byte.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "assembly/exadecimal.ma".
  18
  19 record byte : Type ≝ {
  20  bh: exadecimal;
  21  bl: exadecimal
  22 }.
  23
  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).
  27
  28 definition eqbyte ≝
  29  λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
  30
  31 definition plusbyte ≝
  32  λb1,b2,c.
  33   match plusex (bl b1) (bl b2) c with
  34    [ couple l c' ⇒
  35       match plusex (bh b1) (bh b2) c' with
  36        [ couple h c'' ⇒ couple ? ? (mk_byte h l) c'' ]].
  37
  38 definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
  39
  40 coercion cic:/matita/assembly/byte/nat_of_byte.con.
  41
  42 definition byte_of_nat ≝
  43  λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
  44
  45 interpretation "byte_of_nat" 'byte_of_opcode a =
  46  (cic:/matita/assembly/byte/byte_of_nat.con a).
  47
  48 lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
  49  intros;
  50  elim b;
  51  elim e;
  52  elim e1;
  53  reflexivity.
  54 qed.
  55
  56 lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256.
  57  intro;
  58  unfold nat_of_byte;
  59  letin H ≝ (lt_nat_of_exadecimal_16 (bh b)); clearbody H;
  60  letin K ≝ (lt_nat_of_exadecimal_16 (bl b)); clearbody K;
  61  unfold lt in H 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;
  64  apply le_S_S;
  65  cut (16*bh b ≤ 16*15);
  66   [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
  67     simplify in Hf:(? ? %);
  68     assumption
  69   | apply le_times_r. apply H'.
  70   ]
  71 qed.
  72
  73 lemma nat_of_byte_byte_of_nat: ∀n. nat_of_byte (byte_of_nat n) = n \mod 256.
  74  intro;
  75  letin H ≝ (lt_nat_of_byte_256 (byte_of_nat n)); clearbody H;
  76  rewrite < (lt_to_eq_mod ? ? H); clear H;
  77  unfold byte_of_nat;
  78  unfold nat_of_byte;
  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 ⊢ (? ? % ?);
  92   [ reflexivity
  93   | autobatch
  94   ].
  95 qed.
  96
  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).
  99  intro;
 100  unfold byte_of_nat;
 101  apply eq_f2;
 102   [ rewrite > exadecimal_of_nat_mod in ⊢ (? ? % ?);
 103     rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
 104     apply eq_f;
 105     elim daemon
 106   | rewrite > exadecimal_of_nat_mod;
 107     rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
 108     rewrite > divides_to_eq_mod_mod_mod;
 109      [ reflexivity
 110      | apply (witness ? ? 16). reflexivity.
 111      ]
 112   ]
 113 qed.
 114
 115 lemma plusbyte_ok:
 116  ∀b1,b2,c.
 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
 119    ].
 120  intros; elim daemon.
 121  (*
 122  unfold plusbyte;
 123  generalize in match (plusex_ok (bl b1) (bl b2) c);
 124  elim (plusex (bl b1) (bl b2) c);
 125  simplify in H ⊢ %;
 126  generalize in match (plusex_ok (bh b1) (bh b2) t1);
 127  elim (plusex (bh b1) (bh b2) t1);
 128  simplify in H1 ⊢ %;
 129  change in ⊢ (? ? ? (? (? % ?) ?)) with (16 * t2);
 130  unfold nat_of_byte;
 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 | ];
 141  clear K';
 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.
 153  *)
 154 qed.
 155
 156 definition bpred ≝
 157  λb.
 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))
 161    ].
 162
 163 lemma plusbyte_O_x:
 164  ∀b. plusbyte (mk_byte x0 x0) b false = couple ? ? b false.
 165  intros;
 166  elim b;
 167  elim e;
 168  elim e1;
 169  reflexivity.
 170 qed.
 171
 172 definition plusbytenc ≝
 173  λx,y.
 174   match plusbyte x y false with
 175    [couple res _ ⇒ res].
 176
 177 definition plusbytec ≝
 178  λx,y.
 179   match plusbyte x y false with
 180    [couple _ c ⇒ c].
 181
 182 lemma plusbytenc_O_x:
 183  ∀x. plusbytenc (mk_byte x0 x0) x = x.
 184  intros;
 185  unfold plusbytenc;
 186  rewrite > plusbyte_O_x;
 187  reflexivity.
 188 qed.
 189
 190 lemma eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256.
 191  intro;
 192  lapply (lt_nat_of_byte_256 b);
 193  rewrite > (lt_to_eq_mod ? ? Hletin) in ⊢ (? ? ? %);
 194  reflexivity.
 195 qed.
 196
 197 theorem plusbytenc_ok:
 198  ∀b1,b2:byte. nat_of_byte (plusbytenc b1 b2) = (b1 + b2) \mod 256.
 199  intros;
 200  unfold plusbytenc;
 201  generalize in match (plusbyte_ok b1 b2 false);
 202  elim (plusbyte b1 b2 false);
 203  simplify in H ⊢ %;
 204  change with (nat_of_byte t = (b1 + b2) \mod 256);
 205  rewrite < plus_n_O in H;
 206  rewrite > H; clear H;
 207  rewrite > mod_plus;
 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';
 210   [ autobatch | ];
 211  autobatch paramodulation.
 212 qed.
 213
 214
 215
 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.
 218  intros;
 219  unfold byte_of_nat;
 220  cut (b < 15 ∨ b ≥ 15);
 221   [ elim Hcut;
 222     [ unfold eqbyte;
 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)))));
 227          simplify;
 228          reflexivity
 229        | assumption
 230        ]
 231     | unfold eqbyte;
 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 ? ?);
 234        [ autobatch
 235        | unfold in H1;
 236          apply le_S_S;
 237          assumption
 238        | clearbody K;
 239          elim K; clear K;
 240          rewrite > H2;
 241          rewrite > eq_eqex_S_x0_false;
 242           [ reflexivity
 243           | unfold lt;
 244             unfold lt in H;
 245             rewrite < H2;
 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);
 251             [apply lt_S_to_le;
 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;
 256             ]
 257           ]
 258        ]
 259     ]
 260   | elim (or_lt_le b 15);unfold ge;autobatch
 261   ].
 262 qed.
 263
 264 axiom eq_mod_O_to_exists: ∀n,m. n \mod m = 0 → ∃z. n = z*m.
 265
 266 lemma eq_bpred_S_a_a:
 267  ∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a.
 268  intros;
 269  unfold bpred;
 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))))
 272      = byte_of_nat a);
 273     rewrite > (eqex_true_to_eq ? ? H1);
 274     normalize in ⊢ (? ? (? ? %) ?);
 275     unfold byte_of_nat;
 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;
 285     rewrite > H1;
 286     rewrite > lt_O_to_div_times; [2: autobatch | ]
 287     lapply (eq_f ? ? (λx.x/16) ? ? H1);
 288     rewrite > lt_O_to_div_times in Hletin; [2: autobatch | ]
 289     lapply (eq_f ? ? (λx.x \mod 16) ? ? H1);
 290     rewrite > eq_mod_times_n_m_m_O in Hletin1;
 291     elim daemon
 292   | change with (mk_byte (bh (byte_of_nat (S a))) (xpred (bl (byte_of_nat (S a))))
 293     = byte_of_nat a);
 294     unfold byte_of_nat;
 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);
 301      [2: intro;
 302        apply Hletin;
 303        lapply (eq_f ? ? exadecimal_of_nat ? ? H2);
 304        rewrite > exadecimal_of_nat_nat_of_exadecimal in Hletin1;
 305        apply Hletin1
 306      | ];
 307
 308     elim daemon
 309   ]
 310 qed.
 311
 312 lemma plusbytenc_S:
 313  ∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n).
 314  intros;
 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 ⊢ (? ? (? (? % ?)) ?);
 324  reflexivity.
 325 qed.
 326
 327 lemma eq_plusbytec_x0_x0_x_false:
 328  ∀x.plusbytec (mk_byte x0 x0) x = false.
 329  intro;
 330  elim x;
 331  elim e;
 332  elim e1;
 333  reflexivity.
 334 qed.