matita/contribs/assembly/freescale/byte8.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 (*                           Progetto FreeScale                           *)
  17 (*                                                                        *)
  18 (* Sviluppato da:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/exadecim.ma".
  28
  29 (* ******************** *)
  30 (* DEFINIZIONE DEI BYTE *)
  31 (* ******************** *)
  32
  33 record byte8 : Type ≝
  34  {
  35  b8h: exadecim;
  36  b8l: exadecim
  37  }.
  38
  39 (* \langle \rangle *)
  40 notation "〈x,y〉" non associative with precedence 80
  41  for @{ 'mk_byte8 $x $y }.
  42 interpretation "mk_byte8" 'mk_byte8 x y =
  43  (cic:/matita/freescale/byte8/byte8.ind#xpointer(1/1/1) x y).
  44
  45 (* operatore = *)
  46 definition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)).
  47
  48 (* operatore < *)
  49 definition lt_b8 ≝
  50 λb1,b2:byte8.match lt_ex (b8h b1) (b8h b2) with
  51  [ true ⇒ true
  52  | false ⇒ match gt_ex (b8h b1) (b8h b2) with
  53   [ true ⇒ false
  54   | false ⇒ lt_ex (b8l b1) (b8l b2) ]].
  55
  56 (* operatore ≤ *)
  57 definition le_b8 ≝ λb1,b2:byte8.(eq_b8 b1 b2) ⊕ (lt_b8 b1 b2).
  58
  59 (* operatore > *)
  60 definition gt_b8 ≝ λb1,b2:byte8.⊖ (le_b8 b1 b2).
  61
  62 (* operatore ≥ *)
  63 definition ge_b8 ≝ λb1,b2:byte8.⊖ (lt_b8 b1 b2).
  64
  65 (* operatore and *)
  66 definition and_b8 ≝
  67 λb1,b2:byte8.mk_byte8 (and_ex (b8h b1) (b8h b2)) (and_ex (b8l b1) (b8l b2)).
  68
  69 (* operatore or *)
  70 definition or_b8 ≝
  71 λb1,b2:byte8.mk_byte8 (or_ex (b8h b1) (b8h b2)) (or_ex (b8l b1) (b8l b2)).
  72
  73 (* operatore xor *)
  74 definition xor_b8 ≝
  75 λb1,b2:byte8.mk_byte8 (xor_ex (b8h b1) (b8h b2)) (xor_ex (b8l b1) (b8l b2)).
  76
  77 (* operatore rotazione destra con carry *)
  78 definition rcr_b8 ≝
  79 λb:byte8.λc:bool.match rcr_ex (b8h b) c with
  80  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
  81   [ pair bl' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
  82
  83 (* operatore shift destro *)
  84 definition shr_b8 ≝
  85 λb:byte8.match rcr_ex (b8h b) false with
  86  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
  87   [ pair bl' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
  88
  89 (* operatore rotazione destra *)
  90 definition ror_b8 ≝
  91 λb:byte8.match rcr_ex (b8h b) false with
  92  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
  93   [ pair bl' c'' ⇒ match c'' with
  94    [ true ⇒ mk_byte8 (or_ex x8 bh') bl'
  95    | false ⇒ mk_byte8 bh' bl' ]]].
  96
  97 (* operatore rotazione destra n-volte *)
  98 let rec ror_b8_n (b:byte8) (n:nat) on n ≝
  99  match n with
 100   [ O ⇒ b
 101   | S n' ⇒ ror_b8_n (ror_b8 b) n' ].
 102
 103 (* operatore rotazione sinistra con carry *)
 104 definition rcl_b8 ≝
 105 λb:byte8.λc:bool.match rcl_ex (b8l b) c with
 106  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
 107   [ pair bh' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
 108
 109 (* operatore shift sinistro *)
 110 definition shl_b8 ≝
 111 λb:byte8.match rcl_ex (b8l b) false with
 112  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
 113   [ pair bh' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
 114
 115 (* operatore rotazione sinistra *)
 116 definition rol_b8 ≝
 117 λb:byte8.match rcl_ex (b8l b) false with
 118  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
 119   [ pair bh' c'' ⇒ match c'' with
 120    [ true ⇒ mk_byte8 bh' (or_ex x1 bl')
 121    | false ⇒ mk_byte8 bh' bl' ]]].
 122
 123 (* operatore rotazione sinistra n-volte *)
 124 let rec rol_b8_n (b:byte8) (n:nat) on n ≝
 125  match n with
 126   [ O ⇒ b
 127   | S n' ⇒ rol_b8_n (rol_b8 b) n' ].
 128
 129 (* operatore not/complemento a 1 *)
 130 definition not_b8 ≝
 131 λb:byte8.mk_byte8 (not_ex (b8h b)) (not_ex (b8l b)).
 132
 133 (* operatore somma con carry *)
 134 definition plus_b8 ≝
 135 λb1,b2:byte8.λc:bool.
 136  match plus_ex (b8l b1) (b8l b2) c with
 137   [ pair l c' ⇒ match plus_ex (b8h b1) (b8h b2) c' with
 138    [ pair h c'' ⇒ pair ?? (mk_byte8 h l) c'' ]].
 139
 140 (* operatore somma senza carry *)
 141 definition plus_b8nc ≝
 142 λb1,b2:byte8.fst ?? (plus_b8 b1 b2 false).
 143
 144 (* operatore carry della somma *)
 145 definition plus_b8c ≝
 146 λb1,b2:byte8.snd ?? (plus_b8 b1 b2 false).
 147
 148 (* operatore Most Significant Bit *)
 149 definition MSB_b8 ≝ λb:byte8.eq_ex x8 (and_ex x8 (b8h b)).
 150
 151 (* byte → naturali *)
 152 definition nat_of_byte8 ≝ λb:byte8.16*(b8h b) + (b8l b).
 153
 154 coercion cic:/matita/freescale/byte8/nat_of_byte8.con.
 155
 156 (* naturali → byte *)
 157 definition byte8_of_nat ≝ λn.mk_byte8 (exadecim_of_nat (n/16)) (exadecim_of_nat n).
 158
 159 (* operatore predecessore *)
 160 definition pred_b8 ≝
 161 λb:byte8.match eq_ex (b8l b) x0 with
 162  [ true ⇒ mk_byte8 (pred_ex (b8h b)) (pred_ex (b8l b))
 163  | false ⇒ mk_byte8 (b8h b) (pred_ex (b8l b)) ].
 164
 165 (* operatore successore *)
 166 definition succ_b8 ≝
 167 λb:byte8.match eq_ex (b8l b) xF with
 168  [ true ⇒ mk_byte8 (succ_ex (b8h b)) (succ_ex (b8l b))
 169  | false ⇒ mk_byte8 (b8h b) (succ_ex (b8l b)) ].
 170
 171 (* operatore neg/complemento a 2 *)
 172 definition compl_b8 ≝
 173 λb:byte8.match MSB_b8 b with
 174  [ true ⇒ succ_b8 (not_b8 b)
 175  | false ⇒ not_b8 (pred_b8 b) ].
 176
 177 (* operatore moltiplicazione senza segno: e*e=[0x00,0xE1] *)
 178 definition mul_ex ≝
 179 λe1,e2:exadecim.match e1 with
 180  [ x0 ⇒ match e2 with
 181   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x0〉   | x2 ⇒ 〈x0,x0〉   | x3 ⇒ 〈x0,x0〉
 182   | x4 ⇒ 〈x0,x0〉   | x5 ⇒ 〈x0,x0〉   | x6 ⇒ 〈x0,x0〉   | x7 ⇒ 〈x0,x0〉
 183   | x8 ⇒ 〈x0,x0〉   | x9 ⇒ 〈x0,x0〉   | xA ⇒ 〈x0,x0〉   | xB ⇒ 〈x0,x0〉
 184   | xC ⇒ 〈x0,x0〉   | xD ⇒ 〈x0,x0〉   | xE ⇒ 〈x0,x0〉   | xF ⇒ 〈x0,x0〉 ]
 185  | x1 ⇒ match e2 with
 186   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x1〉   | x2 ⇒ 〈x0,x2〉   | x3 ⇒ 〈x0,x3〉
 187   | x4 ⇒ 〈x0,x4〉   | x5 ⇒ 〈x0,x5〉   | x6 ⇒ 〈x0,x6〉   | x7 ⇒ 〈x0,x7〉
 188   | x8 ⇒ 〈x0,x8〉   | x9 ⇒ 〈x0,x9〉   | xA ⇒ 〈x0,xA〉   | xB ⇒ 〈x0,xB〉
 189   | xC ⇒ 〈x0,xC〉   | xD ⇒ 〈x0,xD〉   | xE ⇒ 〈x0,xE〉   | xF ⇒ 〈x0,xF〉 ]
 190  | x2 ⇒ match e2 with
 191   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x2〉   | x2 ⇒ 〈x0,x4〉   | x3 ⇒ 〈x0,x6〉
 192   | x4 ⇒ 〈x0,x8〉   | x5 ⇒ 〈x0,xA〉   | x6 ⇒ 〈x0,xC〉   | x7 ⇒ 〈x0,xE〉
 193   | x8 ⇒ 〈x1,x0〉   | x9 ⇒ 〈x1,x2〉   | xA ⇒ 〈x1,x4〉   | xB ⇒ 〈x1,x6〉
 194   | xC ⇒ 〈x1,x8〉   | xD ⇒ 〈x1,xA〉   | xE ⇒ 〈x1,xC〉   | xF ⇒ 〈x1,xE〉 ]
 195  | x3 ⇒ match e2 with
 196   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x3〉   | x2 ⇒ 〈x0,x6〉   | x3 ⇒ 〈x0,x9〉
 197   | x4 ⇒ 〈x0,xC〉   | x5 ⇒ 〈x0,xF〉   | x6 ⇒ 〈x1,x2〉   | x7 ⇒ 〈x1,x5〉
 198   | x8 ⇒ 〈x1,x8〉   | x9 ⇒ 〈x1,xB〉   | xA ⇒ 〈x1,xE〉   | xB ⇒ 〈x2,x1〉
 199   | xC ⇒ 〈x2,x4〉   | xD ⇒ 〈x2,x7〉   | xE ⇒ 〈x2,xA〉   | xF ⇒ 〈x2,xD〉 ]
 200  | x4 ⇒ match e2 with
 201   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x4〉   | x2 ⇒ 〈x0,x8〉   | x3 ⇒ 〈x0,xC〉
 202   | x4 ⇒ 〈x1,x0〉   | x5 ⇒ 〈x1,x4〉   | x6 ⇒ 〈x1,x8〉   | x7 ⇒ 〈x1,xC〉
 203   | x8 ⇒ 〈x2,x0〉   | x9 ⇒ 〈x2,x4〉   | xA ⇒ 〈x2,x8〉   | xB ⇒ 〈x2,xC〉
 204   | xC ⇒ 〈x3,x0〉   | xD ⇒ 〈x3,x4〉   | xE ⇒ 〈x3,x8〉   | xF ⇒ 〈x3,xC〉 ]
 205  | x5 ⇒ match e2 with
 206   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x5〉   | x2 ⇒ 〈x0,xA〉   | x3 ⇒ 〈x0,xF〉
 207   | x4 ⇒ 〈x1,x4〉   | x5 ⇒ 〈x1,x9〉   | x6 ⇒ 〈x1,xE〉   | x7 ⇒ 〈x2,x3〉
 208   | x8 ⇒ 〈x2,x8〉   | x9 ⇒ 〈x2,xD〉   | xA ⇒ 〈x3,x2〉   | xB ⇒ 〈x3,x7〉
 209   | xC ⇒ 〈x3,xC〉   | xD ⇒ 〈x4,x1〉   | xE ⇒ 〈x4,x6〉   | xF ⇒ 〈x4,xB〉 ]
 210  | x6 ⇒ match e2 with
 211   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x6〉   | x2 ⇒ 〈x0,xC〉   | x3 ⇒ 〈x1,x2〉
 212   | x4 ⇒ 〈x1,x8〉   | x5 ⇒ 〈x1,xE〉   | x6 ⇒ 〈x2,x4〉   | x7 ⇒ 〈x2,xA〉
 213   | x8 ⇒ 〈x3,x0〉   | x9 ⇒ 〈x3,x6〉   | xA ⇒ 〈x3,xC〉   | xB ⇒ 〈x4,x2〉
 214   | xC ⇒ 〈x4,x8〉   | xD ⇒ 〈x4,xE〉   | xE ⇒ 〈x5,x4〉   | xF ⇒ 〈x5,xA〉 ]
 215  | x7 ⇒ match e2 with
 216   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x7〉   | x2 ⇒ 〈x0,xE〉   | x3 ⇒ 〈x1,x5〉
 217   | x4 ⇒ 〈x1,xC〉   | x5 ⇒ 〈x2,x3〉   | x6 ⇒ 〈x2,xA〉   | x7 ⇒ 〈x3,x1〉
 218   | x8 ⇒ 〈x3,x8〉   | x9 ⇒ 〈x3,xF〉   | xA ⇒ 〈x4,x6〉   | xB ⇒ 〈x4,xD〉
 219   | xC ⇒ 〈x5,x4〉   | xD ⇒ 〈x5,xB〉   | xE ⇒ 〈x6,x2〉   | xF ⇒ 〈x6,x9〉 ]
 220  | x8 ⇒ match e2 with
 221   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x8〉   | x2 ⇒ 〈x1,x0〉   | x3 ⇒ 〈x1,x8〉
 222   | x4 ⇒ 〈x2,x0〉   | x5 ⇒ 〈x2,x8〉   | x6 ⇒ 〈x3,x0〉   | x7 ⇒ 〈x3,x8〉
 223   | x8 ⇒ 〈x4,x0〉   | x9 ⇒ 〈x4,x8〉   | xA ⇒ 〈x5,x0〉   | xB ⇒ 〈x5,x8〉
 224   | xC ⇒ 〈x6,x0〉   | xD ⇒ 〈x6,x8〉   | xE ⇒ 〈x7,x0〉   | xF ⇒ 〈x7,x8〉 ]
 225  | x9 ⇒ match e2 with
 226   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x9〉   | x2 ⇒ 〈x1,x2〉   | x3 ⇒ 〈x1,xB〉
 227   | x4 ⇒ 〈x2,x4〉   | x5 ⇒ 〈x2,xD〉   | x6 ⇒ 〈x3,x6〉   | x7 ⇒ 〈x3,xF〉
 228   | x8 ⇒ 〈x4,x8〉   | x9 ⇒ 〈x5,x1〉   | xA ⇒ 〈x5,xA〉   | xB ⇒ 〈x6,x3〉
 229   | xC ⇒ 〈x6,xC〉   | xD ⇒ 〈x7,x5〉   | xE ⇒ 〈x7,xE〉   | xF ⇒ 〈x8,x7〉 ]
 230  | xA ⇒ match e2 with
 231   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xA〉   | x2 ⇒ 〈x1,x4〉   | x3 ⇒ 〈x1,xE〉
 232   | x4 ⇒ 〈x2,x8〉   | x5 ⇒ 〈x3,x2〉   | x6 ⇒ 〈x3,xC〉   | x7 ⇒ 〈x4,x6〉
 233   | x8 ⇒ 〈x5,x0〉   | x9 ⇒ 〈x5,xA〉   | xA ⇒ 〈x6,x4〉   | xB ⇒ 〈x6,xE〉
 234   | xC ⇒ 〈x7,x8〉   | xD ⇒ 〈x8,x2〉   | xE ⇒ 〈x8,xC〉   | xF ⇒ 〈x9,x6〉 ]
 235  | xB ⇒ match e2 with
 236   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xB〉   | x2 ⇒ 〈x1,x6〉   | x3 ⇒ 〈x2,x1〉
 237   | x4 ⇒ 〈x2,xC〉   | x5 ⇒ 〈x3,x7〉   | x6 ⇒ 〈x4,x2〉   | x7 ⇒ 〈x4,xD〉
 238   | x8 ⇒ 〈x5,x8〉   | x9 ⇒ 〈x6,x3〉   | xA ⇒ 〈x6,xE〉   | xB ⇒ 〈x7,x9〉
 239   | xC ⇒ 〈x8,x4〉   | xD ⇒ 〈x8,xF〉   | xE ⇒ 〈x9,xA〉   | xF ⇒ 〈xA,x5〉 ]
 240  | xC ⇒ match e2 with
 241   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xC〉   | x2 ⇒ 〈x1,x8〉   | x3 ⇒ 〈x2,x4〉
 242   | x4 ⇒ 〈x3,x0〉   | x5 ⇒ 〈x3,xC〉   | x6 ⇒ 〈x4,x8〉   | x7 ⇒ 〈x5,x4〉
 243   | x8 ⇒ 〈x6,x0〉   | x9 ⇒ 〈x6,xC〉   | xA ⇒ 〈x7,x8〉   | xB ⇒ 〈x8,x4〉
 244   | xC ⇒ 〈x9,x0〉   | xD ⇒ 〈x9,xC〉   | xE ⇒ 〈xA,x8〉   | xF ⇒ 〈xB,x4〉 ]
 245  | xD ⇒ match e2 with
 246   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xD〉   | x2 ⇒ 〈x1,xA〉   | x3 ⇒ 〈x2,x7〉
 247   | x4 ⇒ 〈x3,x4〉   | x5 ⇒ 〈x4,x1〉   | x6 ⇒ 〈x4,xE〉   | x7 ⇒ 〈x5,xB〉
 248   | x8 ⇒ 〈x6,x8〉   | x9 ⇒ 〈x7,x5〉   | xA ⇒ 〈x8,x2〉   | xB ⇒ 〈x8,xF〉
 249   | xC ⇒ 〈x9,xC〉   | xD ⇒ 〈xA,x9〉   | xE ⇒ 〈xB,x6〉   | xF ⇒ 〈xC,x3〉 ]
 250  | xE ⇒ match e2 with
 251   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xE〉   | x2 ⇒ 〈x1,xC〉   | x3 ⇒ 〈x2,xA〉
 252   | x4 ⇒ 〈x3,x8〉   | x5 ⇒ 〈x4,x6〉   | x6 ⇒ 〈x5,x4〉   | x7 ⇒ 〈x6,x2〉
 253   | x8 ⇒ 〈x7,x0〉   | x9 ⇒ 〈x7,xE〉   | xA ⇒ 〈x8,xC〉   | xB ⇒ 〈x9,xA〉
 254   | xC ⇒ 〈xA,x8〉   | xD ⇒ 〈xB,x6〉   | xE ⇒ 〈xC,x4〉   | xF ⇒ 〈xD,x2〉 ]
 255  | xF ⇒ match e2 with
 256   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xF〉   | x2 ⇒ 〈x1,xE〉   | x3 ⇒ 〈x2,xD〉
 257   | x4 ⇒ 〈x3,xC〉   | x5 ⇒ 〈x4,xB〉   | x6 ⇒ 〈x5,xA〉   | x7 ⇒ 〈x6,x9〉
 258   | x8 ⇒ 〈x7,x8〉   | x9 ⇒ 〈x8,x7〉   | xA ⇒ 〈x9,x6〉   | xB ⇒ 〈xA,x5〉
 259   | xC ⇒ 〈xB,x4〉   | xD ⇒ 〈xC,x3〉   | xE ⇒ 〈xD,x2〉   | xF ⇒ 〈xE,x1〉 ]
 260  ].
 261
 262 (* correzione per somma su BCD *)
 263 (* input: halfcarry,carry,X(BCD+BCD) *)
 264 (* output: X',carry' *)
 265 definition daa_b8 ≝
 266 λh,c:bool.λX:byte8.
 267  match lt_b8 X 〈x9,xA〉 with
 268   (* [X:0x00-0x99] *)
 269   (* c' = c *)
 270   (* X' = [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + [c=1 ? 0x60 : 0x00]
 271           [(b16l X):0xA-0xF] X + 0x06 + [c=1 ? 0x60 : 0x00] *)
 272   [ true ⇒
 273    let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
 274     [ true ⇒ X
 275     | false ⇒ plus_b8nc X 〈x0,x6〉 ] in
 276    let X'' ≝ match c with
 277     [ true ⇒ plus_b8nc X' 〈x6,x0〉
 278     | false ⇒ X' ] in
 279    pair ?? X'' c
 280   (* [X:0x9A-0xFF] *)
 281   (* c' = 1 *)
 282   (* X' = [X:0x9A-0xFF]
 283           [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + 0x60
 284           [(b16l X):0xA-0xF] X + 0x6 + 0x60 *)
 285   | false ⇒
 286    let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
 287     [ true ⇒ X
 288     | false ⇒ plus_b8nc X 〈x0,x6〉 ] in
 289    let X'' ≝ plus_b8nc X' 〈x6,x0〉 in
 290    pair ?? X'' true
 291   ].
 292
 293 (* iteratore sui byte *)
 294 definition forall_byte8 ≝
 295  λP.
 296   forall_exadecim (λbh.
 297   forall_exadecim (λbl.
 298    P (mk_byte8 bh bl))).
 299
 300 (* ********************** *)
 301 (* TEOREMI/LEMMMI/ASSIOMI *)
 302 (* ********************** *)
 303
 304 lemma byte8_of_nat_nat_of_byte8: ∀b. byte8_of_nat (nat_of_byte8 b) = b.
 305  intros;
 306  elim b;
 307  elim e;
 308  elim e1;
 309  reflexivity.
 310 qed.
 311
 312 lemma lt_nat_of_byte8_256: ∀b. nat_of_byte8 b < 256.
 313  intro;
 314  unfold nat_of_byte8;
 315  letin H ≝ (lt_nat_of_exadecim_16 (b8h b)); clearbody H;
 316  letin K ≝ (lt_nat_of_exadecim_16 (b8l b)); clearbody K;
 317  unfold lt in H K ⊢ %;
 318  letin H' ≝ (le_S_S_to_le ? ? H); clearbody H'; clear H;
 319  letin K' ≝ (le_S_S_to_le ? ? K); clearbody K'; clear K;
 320  apply le_S_S;
 321  cut (16*b8h b ≤ 16*15);
 322   [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
 323     simplify in Hf:(? ? %);
 324     assumption
 325   | apply le_times_r. apply H'.
 326   ]
 327 qed.
 328
 329 lemma nat_of_byte8_byte8_of_nat: ∀n. nat_of_byte8 (byte8_of_nat n) = n \mod 256.
 330  intro;
 331  letin H ≝ (lt_nat_of_byte8_256 (byte8_of_nat n)); clearbody H;
 332  rewrite < (lt_to_eq_mod ? ? H); clear H;
 333  unfold byte8_of_nat;
 334  unfold nat_of_byte8;
 335  change with ((16*(exadecim_of_nat (n/16)) + exadecim_of_nat n) \mod 256 = n \mod 256);
 336  letin H ≝ (div_mod n 16 ?); clearbody H; [ autobatch | ];
 337  rewrite > symmetric_times in H;
 338  rewrite > nat_of_exadecim_exadecim_of_nat in ⊢ (? ? (? (? % ?) ?) ?);
 339  rewrite > nat_of_exadecim_exadecim_of_nat in ⊢ (? ? (? (? ? %) ?) ?);
 340  rewrite > H in ⊢ (? ? ? (? % ?)); clear H;
 341  rewrite > mod_plus in ⊢ (? ? % ?);
 342  rewrite > mod_plus in ⊢ (? ? ? %);
 343  apply eq_mod_to_eq_plus_mod;
 344  rewrite < mod_mod in ⊢ (? ? ? %); [ | autobatch];
 345  rewrite < mod_mod in ⊢ (? ? % ?); [ | autobatch];
 346  rewrite < (eq_mod_times_times_mod ? ? 16 256) in ⊢ (? ? (? % ?) ?); [2: reflexivity | ];
 347  rewrite < mod_mod in ⊢ (? ? % ?);
 348   [ reflexivity
 349   | autobatch
 350   ].
 351 qed.
 352
 353 lemma eq_nat_of_byte8_n_nat_of_byte8_mod_n_256:
 354  ∀n. byte8_of_nat n = byte8_of_nat (n \mod 256).
 355  intro;
 356  unfold byte8_of_nat;
 357  apply eq_f2;
 358   [ rewrite > exadecim_of_nat_mod in ⊢ (? ? % ?);
 359     rewrite > exadecim_of_nat_mod in ⊢ (? ? ? %);
 360     apply eq_f;
 361     elim daemon
 362   | rewrite > exadecim_of_nat_mod;
 363     rewrite > exadecim_of_nat_mod in ⊢ (? ? ? %);
 364     rewrite > divides_to_eq_mod_mod_mod;
 365      [ reflexivity
 366      | apply (witness ? ? 16). reflexivity.
 367      ]
 368   ]
 369 qed.
 370
 371 lemma plusb8_ok:
 372  ∀b1,b2,c.
 373   match plus_b8 b1 b2 c with
 374    [ pair r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte8 r + nat_of_bool c' * 256
 375    ].
 376  intros; elim daemon.
 377 qed.
 378
 379 lemma plusb8_O_x:
 380  ∀b. plus_b8 (mk_byte8 x0 x0) b false = pair ?? b false.
 381  intros;
 382  elim b;
 383  elim e;
 384  elim e1;
 385  reflexivity.
 386 qed.
 387
 388 lemma plusb8nc_O_x:
 389  ∀x. plus_b8nc (mk_byte8 x0 x0) x = x.
 390  intros;
 391  unfold plus_b8nc;
 392  rewrite > plusb8_O_x;
 393  reflexivity.
 394 qed.
 395
 396 lemma eq_nat_of_byte8_mod: ∀b. nat_of_byte8 b = nat_of_byte8 b \mod 256.
 397  intro;
 398  lapply (lt_nat_of_byte8_256 b);
 399  rewrite > (lt_to_eq_mod ? ? Hletin) in ⊢ (? ? ? %);
 400  reflexivity.
 401 qed.
 402
 403 theorem plusb8nc_ok:
 404  ∀b1,b2:byte8.nat_of_byte8 (plus_b8nc b1 b2) = (b1 + b2) \mod 256.
 405  intros;
 406  unfold plus_b8nc;
 407  generalize in match (plusb8_ok b1 b2 false);
 408  elim (plus_b8 b1 b2 false);
 409  simplify in H ⊢ %;
 410  change with (nat_of_byte8 a = (b1 + b2) \mod 256);
 411  rewrite < plus_n_O in H;
 412  rewrite > H; clear H;
 413  rewrite > mod_plus;
 414  letin K ≝ (eq_nat_of_byte8_mod a); clearbody K;
 415  letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool b) 256 ?); clearbody K';
 416   [ autobatch | ];
 417  autobatch paramodulation.
 418 qed.
 419
 420 lemma eq_eqb8_x0_x0_byte8_of_nat_S_false:
 421  ∀b. b < 255 → eq_b8 (mk_byte8 x0 x0) (byte8_of_nat (S b)) = false.
 422  intros;
 423  unfold byte8_of_nat;
 424  cut (b < 15 ∨ b ≥ 15);
 425   [ elim Hcut;
 426     [ unfold eq_b8;
 427       change in ⊢ (? ? (? ? %) ?) with (eq_ex x0 (exadecim_of_nat (S b)));
 428       rewrite > eq_eqex_S_x0_false;
 429        [ elim (eq_ex (b8h (mk_byte8 x0 x0))
 430           (b8h (mk_byte8 (exadecim_of_nat (S b/16)) (exadecim_of_nat (S b)))));
 431          simplify;
 432          reflexivity
 433        | assumption
 434        ]
 435     | unfold eq_b8;
 436       change in ⊢ (? ? (? % ?) ?) with (eq_ex x0 (exadecim_of_nat (S b/16)));
 437       letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?);
 438        [ autobatch
 439        | unfold in H1;
 440          apply le_S_S;
 441          assumption
 442        | clearbody K;
 443          elim K; clear K;
 444          rewrite > H2;
 445          rewrite > eq_eqex_S_x0_false;
 446           [ reflexivity
 447           | unfold lt;
 448             unfold lt in H;
 449             rewrite < H2;
 450             clear H2; clear a; clear H1; clear Hcut;
 451             apply (le_times_to_le 16) [ autobatch | ] ;
 452             rewrite > (div_mod (S b) 16) in H;[2:autobatch|]
 453             rewrite > (div_mod 255 16) in H:(? ? %);[2:autobatch|]
 454             lapply (le_to_le_plus_to_le ? ? ? ? ? H);
 455             [apply lt_S_to_le;
 456              apply lt_mod_m_m;autobatch
 457             |rewrite > sym_times;
 458              rewrite > sym_times in ⊢ (? ? %);
 459              normalize in ⊢ (? ? %);apply Hletin;
 460             ]
 461           ]
 462        ]
 463     ]
 464   | elim (or_lt_le b 15);unfold ge;autobatch
 465   ].
 466 qed.
 467
 468 axiom eq_mod_O_to_exists: ∀n,m. n \mod m = 0 → ∃z. n = z*m.
 469
 470 lemma eq_b8pred_S_a_a:
 471  ∀a. a < 255 → pred_b8 (byte8_of_nat (S a)) = byte8_of_nat a.
 472  intros;
 473  unfold pred_b8;
 474  apply (bool_elim ? (eq_ex (b8l (byte8_of_nat (S a))) x0)); intros;
 475   [ change with (mk_byte8 (pred_ex (b8h (byte8_of_nat (S a)))) (pred_ex (b8l (byte8_of_nat (S a))))
 476      = byte8_of_nat a);
 477     rewrite > (eqex_true_to_eq ? ? H1);
 478     normalize in ⊢ (? ? (? ? %) ?);
 479     unfold byte8_of_nat;
 480     change with (mk_byte8 (pred_ex (exadecim_of_nat (S a/16))) xF =
 481                  mk_byte8 (exadecim_of_nat (a/16)) (exadecim_of_nat a));
 482     lapply (eqex_true_to_eq ? ? H1); clear H1;
 483     unfold byte8_of_nat in Hletin;
 484     change in Hletin with (exadecim_of_nat (S a) = x0);
 485     lapply (eq_f ? ? nat_of_exadecim ? ? Hletin); clear Hletin;
 486     normalize in Hletin1:(? ? ? %);
 487     rewrite > nat_of_exadecim_exadecim_of_nat in Hletin1;
 488     elim (eq_mod_O_to_exists ? ? Hletin1); clear Hletin1;
 489     rewrite > H1;
 490     rewrite > lt_O_to_div_times; [2: autobatch | ]
 491     lapply (eq_f ? ? (λx.x/16) ? ? H1);
 492     rewrite > lt_O_to_div_times in Hletin; [2: autobatch | ]
 493     lapply (eq_f ? ? (λx.x \mod 16) ? ? H1);
 494     rewrite > eq_mod_times_n_m_m_O in Hletin1;
 495     elim daemon
 496   | change with (mk_byte8 (b8h (byte8_of_nat (S a))) (pred_ex (b8l (byte8_of_nat (S a))))
 497     = byte8_of_nat a);
 498     unfold byte8_of_nat;
 499     change with (mk_byte8 (exadecim_of_nat (S a/16)) (pred_ex (exadecim_of_nat (S a)))
 500     = mk_byte8 (exadecim_of_nat (a/16)) (exadecim_of_nat a));
 501     lapply (eqex_false_to_not_eq ? ? H1);
 502     unfold byte8_of_nat in Hletin;
 503     change in Hletin with (exadecim_of_nat (S a) ≠ x0);
 504     cut (nat_of_exadecim (exadecim_of_nat (S a)) ≠ 0);
 505      [2: intro;
 506        apply Hletin;
 507        lapply (eq_f ? ? exadecim_of_nat ? ? H2);
 508        rewrite > exadecim_of_nat_nat_of_exadecim in Hletin1;
 509        apply Hletin1
 510      | ];
 511     elim daemon
 512   ]
 513 qed.
 514
 515 lemma plusb8nc_S:
 516  ∀x:byte8.∀n.plus_b8nc (byte8_of_nat (x*n)) x = byte8_of_nat (x * S n).
 517  intros;
 518  rewrite < byte8_of_nat_nat_of_byte8;
 519  rewrite > (plusb8nc_ok (byte8_of_nat (x*n)) x);
 520  rewrite < times_n_Sm;
 521  rewrite > nat_of_byte8_byte8_of_nat in ⊢ (? ? (? (? (? % ?) ?)) ?);
 522  rewrite > eq_nat_of_byte8_n_nat_of_byte8_mod_n_256 in ⊢ (? ? ? %);
 523  rewrite > mod_plus in ⊢ (? ? (? %) ?);
 524  rewrite > mod_plus in ⊢ (? ? ? (? %));
 525  rewrite < mod_mod in ⊢ (? ? (? (? (? % ?) ?)) ?); [2: autobatch | ];
 526  rewrite > sym_plus in ⊢ (? ? (? (? % ?)) ?);
 527  reflexivity.
 528 qed.
 529
 530 lemma eq_plusb8c_x0_x0_x_false:
 531  ∀x.plus_b8c (mk_byte8 x0 x0) x = false.
 532  intro;
 533  elim x;
 534  elim e;
 535  elim e1;
 536  reflexivity.
 537 qed.
 538
 539 axiom eqb8_true_to_eq: ∀b,b'. eq_b8 b b' = true → b=b'.
 540
 541 axiom eqb8_false_to_not_eq: ∀b,b'. eq_b8 b b' = false → b ≠ b'.
 542
 543 axiom byte8_of_nat_mod: ∀n.byte8_of_nat n = byte8_of_nat (n \mod 256).
 544
 545 (* nuovi *)
 546
 547 lemma ok_mul_ex :
 548 ∀e1,e2.nat_of_byte8 (mul_ex e1 e2) = (nat_of_exadecim e1) * (nat_of_exadecim e2).
 549 intros;
 550 elim e1;
 551 elim e2;
 552 reflexivity.
 553 qed.