[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / byte8.ma

(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

(* ********************************************************************** *)
(*                          Progetto FreeScale                            *)
(*                                                                        *)
(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
(*                                                                        *)
(* ********************************************************************** *)

include "freescale/exadecim.ma".

(* **** *)
(* BYTE *)
(* **** *)

nrecord byte8 : Type ≝
 {
 b8h: exadecim;
 b8l: exadecim
 }.

(* \langle \rangle *)
notation "〈x,y〉" non associative with precedence 80
 for @{ 'mk_byte8 $x $y }.
interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).

(* operatore = *)
ndefinition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)).

(* operatore < *)
ndefinition lt_b8 ≝
λb1,b2:byte8.match lt_ex (b8h b1) (b8h b2) with
 [ true ⇒ true
 | false ⇒ match gt_ex (b8h b1) (b8h b2) with
  [ true ⇒ false
  | false ⇒ lt_ex (b8l b1) (b8l b2) ]].

(* operatore ≤ *)
ndefinition le_b8 ≝ λb1,b2:byte8.(eq_b8 b1 b2) ⊕ (lt_b8 b1 b2). 

(* operatore > *)
ndefinition gt_b8 ≝ λb1,b2:byte8.⊖ (le_b8 b1 b2).

(* operatore ≥ *)
ndefinition ge_b8 ≝ λb1,b2:byte8.⊖ (lt_b8 b1 b2).

(* operatore and *)
ndefinition and_b8 ≝
λb1,b2:byte8.mk_byte8 (and_ex (b8h b1) (b8h b2)) (and_ex (b8l b1) (b8l b2)).

(* operatore or *)
ndefinition or_b8 ≝
λb1,b2:byte8.mk_byte8 (or_ex (b8h b1) (b8h b2)) (or_ex (b8l b1) (b8l b2)).

(* operatore xor *)
ndefinition xor_b8 ≝
λb1,b2:byte8.mk_byte8 (xor_ex (b8h b1) (b8h b2)) (xor_ex (b8l b1) (b8l b2)).

(* operatore rotazione destra con carry *)
ndefinition rcr_b8 ≝
λb:byte8.λc:bool.match rcr_ex (b8h b) c with
 [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
  [ pair bl' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]]. 

(* operatore shift destro *)
ndefinition shr_b8 ≝
λb:byte8.match rcr_ex (b8h b) false with
 [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
  [ pair bl' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].

(* operatore rotazione destra *)
ndefinition ror_b8 ≝
λb:byte8.match rcr_ex (b8h b) false with
 [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
  [ pair bl' c'' ⇒ match c'' with
   [ true ⇒ mk_byte8 (or_ex x8 bh') bl'
   | false ⇒ mk_byte8 bh' bl' ]]].

(* operatore rotazione destra n-volte *)
nlet rec ror_b8_n (b:byte8) (n:nat) on n ≝
 match n with
  [ O ⇒ b
  | S n' ⇒ ror_b8_n (ror_b8 b) n' ].

(* operatore rotazione sinistra con carry *)
ndefinition rcl_b8 ≝
λb:byte8.λc:bool.match rcl_ex (b8l b) c with
 [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
  [ pair bh' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]]. 

(* operatore shift sinistro *)
ndefinition shl_b8 ≝
λb:byte8.match rcl_ex (b8l b) false with
 [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
  [ pair bh' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].

(* operatore rotazione sinistra *)
ndefinition rol_b8 ≝
λb:byte8.match rcl_ex (b8l b) false with
 [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
  [ pair bh' c'' ⇒ match c'' with
   [ true ⇒ mk_byte8 bh' (or_ex x1 bl')
   | false ⇒ mk_byte8 bh' bl' ]]].

(* operatore rotazione sinistra n-volte *)
nlet rec rol_b8_n (b:byte8) (n:nat) on n ≝
 match n with
  [ O ⇒ b
  | S n' ⇒ rol_b8_n (rol_b8 b) n' ].

(* operatore not/complemento a 1 *)
ndefinition not_b8 ≝
λb:byte8.mk_byte8 (not_ex (b8h b)) (not_ex (b8l b)).

(* operatore somma con data+carry → data+carry *)
ndefinition plus_b8_dc_dc ≝
λb1,b2:byte8.λc:bool.
 match plus_ex_dc_dc (b8l b1) (b8l b2) c with
  [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
   [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]].

(* operatore somma con data+carry → data *)
ndefinition plus_b8_dc_d ≝
λb1,b2:byte8.λc:bool.
 match plus_ex_dc_dc (b8l b1) (b8l b2) c with
  [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].

(* operatore somma con data+carry → c *)
ndefinition plus_b8_dc_c ≝
λb1,b2:byte8.λc:bool.
 plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_dc_c (b8l b1) (b8l b2) c).

(* operatore somma con data → data+carry *)
ndefinition plus_b8_d_dc ≝
λb1,b2:byte8.
 match plus_ex_d_dc (b8l b1) (b8l b2) with
  [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
   [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]].

(* operatore somma con data → data *)
ndefinition plus_b8_d_d ≝
λb1,b2:byte8.
 match plus_ex_d_dc (b8l b1) (b8l b2) with
  [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].

(* operatore somma con data → c *)
ndefinition plus_b8_d_c ≝
λb1,b2:byte8.
 plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_d_c (b8l b1) (b8l b2)).

(* operatore Most Significant Bit *)
ndefinition MSB_b8 ≝ λb:byte8.eq_ex x8 (and_ex x8 (b8h b)).

(* byte → naturali *)
ndefinition nat_of_byte8 ≝ λb:byte8.(16*(nat_of_exadecim (b8h b))) + (nat_of_exadecim (b8l b)).

(* operatore predecessore *)
ndefinition pred_b8 ≝
λb:byte8.match eq_ex (b8l b) x0 with
 [ true ⇒ mk_byte8 (pred_ex (b8h b)) (pred_ex (b8l b))
 | false ⇒ mk_byte8 (b8h b) (pred_ex (b8l b)) ]. 

(* operatore successore *)
ndefinition succ_b8 ≝
λb:byte8.match eq_ex (b8l b) xF with
 [ true ⇒ mk_byte8 (succ_ex (b8h b)) (succ_ex (b8l b))
 | false ⇒ mk_byte8 (b8h b) (succ_ex (b8l b)) ]. 

(* operatore neg/complemento a 2 *)
ndefinition compl_b8 ≝
λb:byte8.match MSB_b8 b with
 [ true ⇒ succ_b8 (not_b8 b)
 | false ⇒ not_b8 (pred_b8 b) ].

(* operatore moltiplicazione senza segno: e*e=[0x00,0xE1] *)
ndefinition mul_ex ≝
λe1,e2:exadecim.match e1 with
 [ x0 ⇒ match e2 with
  [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x0〉   | x2 ⇒ 〈x0,x0〉   | x3 ⇒ 〈x0,x0〉
  | x4 ⇒ 〈x0,x0〉   | x5 ⇒ 〈x0,x0〉   | x6 ⇒ 〈x0,x0〉   | x7 ⇒ 〈x0,x0〉
  | x8 ⇒ 〈x0,x0〉   | x9 ⇒ 〈x0,x0〉   | xA ⇒ 〈x0,x0〉   | xB ⇒ 〈x0,x0〉
  | xC ⇒ 〈x0,x0〉   | xD ⇒ 〈x0,x0〉   | xE ⇒ 〈x0,x0〉   | xF ⇒ 〈x0,x0〉 ]
 | x1 ⇒ match e2 with
  [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x1〉   | x2 ⇒ 〈x0,x2〉   | x3 ⇒ 〈x0,x3〉
  | x4 ⇒ 〈x0,x4〉   | x5 ⇒ 〈x0,x5〉   | x6 ⇒ 〈x0,x6〉   | x7 ⇒ 〈x0,x7〉
  | x8 ⇒ 〈x0,x8〉   | x9 ⇒ 〈x0,x9〉   | xA ⇒ 〈x0,xA〉   | xB ⇒ 〈x0,xB〉
  | xC ⇒ 〈x0,xC〉   | xD ⇒ 〈x0,xD〉   | xE ⇒ 〈x0,xE〉   | xF ⇒ 〈x0,xF〉 ]
 | x2 ⇒ match e2 with
  [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x2〉   | x2 ⇒ 〈x0,x4〉   | x3 ⇒ 〈x0,x6〉
  | x4 ⇒ 〈x0,x8〉   | x5 ⇒ 〈x0,xA〉   | x6 ⇒ 〈x0,xC〉   | x7 ⇒ 〈x0,xE〉
  | x8 ⇒ 〈x1,x0〉   | x9 ⇒ 〈x1,x2〉   | xA ⇒ 〈x1,x4〉   | xB ⇒ 〈x1,x6〉
  | xC ⇒ 〈x1,x8〉   | xD ⇒ 〈x1,xA〉   | xE ⇒ 〈x1,xC〉   | xF ⇒ 〈x1,xE〉 ]
 | x3 ⇒ match e2 with
  [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x3〉   | x2 ⇒ 〈x0,x6〉   | x3 ⇒ 〈x0,x9〉
  | x4 ⇒ 〈x0,xC〉   | x5 ⇒ 〈x0,xF〉   | x6 ⇒ 〈x1,x2〉   | x7 ⇒ 〈x1,x5〉
  | x8 ⇒ 〈x1,x8〉   | x9 ⇒ 〈x1,xB〉   | xA ⇒ 〈x1,xE〉   | xB ⇒ 〈x2,x1〉
  | xC ⇒ 〈x2,x4〉   | xD ⇒ 〈x2,x7〉   | xE ⇒ 〈x2,xA〉   | xF ⇒ 〈x2,xD〉 ]
 | x4 ⇒ match e2 with
  [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x4〉   | x2 ⇒ 〈x0,x8〉   | x3 ⇒ 〈x0,xC〉
  | x4 ⇒ 〈x1,x0〉   | x5 ⇒ 〈x1,x4〉   | x6 ⇒ 〈x1,x8〉   | x7 ⇒ 〈x1,xC〉
  | x8 ⇒ 〈x2,x0〉   | x9 ⇒ 〈x2,x4〉   | xA ⇒ 〈x2,x8〉   | xB ⇒ 〈x2,xC〉
  | xC ⇒ 〈x3,x0〉   | xD ⇒ 〈x3,x4〉   | xE ⇒ 〈x3,x8〉   | xF ⇒ 〈x3,xC〉 ]
 | x5 ⇒ match e2 with
  [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x5〉   | x2 ⇒ 〈x0,xA〉   | x3 ⇒ 〈x0,xF〉
  | x4 ⇒ 〈x1,x4〉   | x5 ⇒ 〈x1,x9〉   | x6 ⇒ 〈x1,xE〉   | x7 ⇒ 〈x2,x3〉
  | x8 ⇒ 〈x2,x8〉   | x9 ⇒ 〈x2,xD〉   | xA ⇒ 〈x3,x2〉   | xB ⇒ 〈x3,x7〉
  | xC ⇒ 〈x3,xC〉   | xD ⇒ 〈x4,x1〉   | xE ⇒ 〈x4,x6〉   | xF ⇒ 〈x4,xB〉 ]
 | x6 ⇒ match e2 with
  [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x6〉   | x2 ⇒ 〈x0,xC〉   | x3 ⇒ 〈x1,x2〉
  | x4 ⇒ 〈x1,x8〉   | x5 ⇒ 〈x1,xE〉   | x6 ⇒ 〈x2,x4〉   | x7 ⇒ 〈x2,xA〉
  | x8 ⇒ 〈x3,x0〉   | x9 ⇒ 〈x3,x6〉   | xA ⇒ 〈x3,xC〉   | xB ⇒ 〈x4,x2〉
  | xC ⇒ 〈x4,x8〉   | xD ⇒ 〈x4,xE〉   | xE ⇒ 〈x5,x4〉   | xF ⇒ 〈x5,xA〉 ]
 | x7 ⇒ match e2 with
  [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x7〉   | x2 ⇒ 〈x0,xE〉   | x3 ⇒ 〈x1,x5〉
  | x4 ⇒ 〈x1,xC〉   | x5 ⇒ 〈x2,x3〉   | x6 ⇒ 〈x2,xA〉   | x7 ⇒ 〈x3,x1〉
  | x8 ⇒ 〈x3,x8〉   | x9 ⇒ 〈x3,xF〉   | xA ⇒ 〈x4,x6〉   | xB ⇒ 〈x4,xD〉
  | xC ⇒ 〈x5,x4〉   | xD ⇒ 〈x5,xB〉   | xE ⇒ 〈x6,x2〉   | xF ⇒ 〈x6,x9〉 ]
 | x8 ⇒ match e2 with
  [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x8〉   | x2 ⇒ 〈x1,x0〉   | x3 ⇒ 〈x1,x8〉
  | x4 ⇒ 〈x2,x0〉   | x5 ⇒ 〈x2,x8〉   | x6 ⇒ 〈x3,x0〉   | x7 ⇒ 〈x3,x8〉
  | x8 ⇒ 〈x4,x0〉   | x9 ⇒ 〈x4,x8〉   | xA ⇒ 〈x5,x0〉   | xB ⇒ 〈x5,x8〉
  | xC ⇒ 〈x6,x0〉   | xD ⇒ 〈x6,x8〉   | xE ⇒ 〈x7,x0〉   | xF ⇒ 〈x7,x8〉 ]
 | x9 ⇒ match e2 with
  [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x9〉   | x2 ⇒ 〈x1,x2〉   | x3 ⇒ 〈x1,xB〉
  | x4 ⇒ 〈x2,x4〉   | x5 ⇒ 〈x2,xD〉   | x6 ⇒ 〈x3,x6〉   | x7 ⇒ 〈x3,xF〉
  | x8 ⇒ 〈x4,x8〉   | x9 ⇒ 〈x5,x1〉   | xA ⇒ 〈x5,xA〉   | xB ⇒ 〈x6,x3〉
  | xC ⇒ 〈x6,xC〉   | xD ⇒ 〈x7,x5〉   | xE ⇒ 〈x7,xE〉   | xF ⇒ 〈x8,x7〉 ]
 | xA ⇒ match e2 with
  [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xA〉   | x2 ⇒ 〈x1,x4〉   | x3 ⇒ 〈x1,xE〉
  | x4 ⇒ 〈x2,x8〉   | x5 ⇒ 〈x3,x2〉   | x6 ⇒ 〈x3,xC〉   | x7 ⇒ 〈x4,x6〉
  | x8 ⇒ 〈x5,x0〉   | x9 ⇒ 〈x5,xA〉   | xA ⇒ 〈x6,x4〉   | xB ⇒ 〈x6,xE〉
  | xC ⇒ 〈x7,x8〉   | xD ⇒ 〈x8,x2〉   | xE ⇒ 〈x8,xC〉   | xF ⇒ 〈x9,x6〉 ]
 | xB ⇒ match e2 with
  [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xB〉   | x2 ⇒ 〈x1,x6〉   | x3 ⇒ 〈x2,x1〉
  | x4 ⇒ 〈x2,xC〉   | x5 ⇒ 〈x3,x7〉   | x6 ⇒ 〈x4,x2〉   | x7 ⇒ 〈x4,xD〉
  | x8 ⇒ 〈x5,x8〉   | x9 ⇒ 〈x6,x3〉   | xA ⇒ 〈x6,xE〉   | xB ⇒ 〈x7,x9〉
  | xC ⇒ 〈x8,x4〉   | xD ⇒ 〈x8,xF〉   | xE ⇒ 〈x9,xA〉   | xF ⇒ 〈xA,x5〉 ]
 | xC ⇒ match e2 with
  [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xC〉   | x2 ⇒ 〈x1,x8〉   | x3 ⇒ 〈x2,x4〉
  | x4 ⇒ 〈x3,x0〉   | x5 ⇒ 〈x3,xC〉   | x6 ⇒ 〈x4,x8〉   | x7 ⇒ 〈x5,x4〉
  | x8 ⇒ 〈x6,x0〉   | x9 ⇒ 〈x6,xC〉   | xA ⇒ 〈x7,x8〉   | xB ⇒ 〈x8,x4〉
  | xC ⇒ 〈x9,x0〉   | xD ⇒ 〈x9,xC〉   | xE ⇒ 〈xA,x8〉   | xF ⇒ 〈xB,x4〉 ]
 | xD ⇒ match e2 with
  [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xD〉   | x2 ⇒ 〈x1,xA〉   | x3 ⇒ 〈x2,x7〉
  | x4 ⇒ 〈x3,x4〉   | x5 ⇒ 〈x4,x1〉   | x6 ⇒ 〈x4,xE〉   | x7 ⇒ 〈x5,xB〉
  | x8 ⇒ 〈x6,x8〉   | x9 ⇒ 〈x7,x5〉   | xA ⇒ 〈x8,x2〉   | xB ⇒ 〈x8,xF〉
  | xC ⇒ 〈x9,xC〉   | xD ⇒ 〈xA,x9〉   | xE ⇒ 〈xB,x6〉   | xF ⇒ 〈xC,x3〉 ]
 | xE ⇒ match e2 with
  [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xE〉   | x2 ⇒ 〈x1,xC〉   | x3 ⇒ 〈x2,xA〉
  | x4 ⇒ 〈x3,x8〉   | x5 ⇒ 〈x4,x6〉   | x6 ⇒ 〈x5,x4〉   | x7 ⇒ 〈x6,x2〉
  | x8 ⇒ 〈x7,x0〉   | x9 ⇒ 〈x7,xE〉   | xA ⇒ 〈x8,xC〉   | xB ⇒ 〈x9,xA〉
  | xC ⇒ 〈xA,x8〉   | xD ⇒ 〈xB,x6〉   | xE ⇒ 〈xC,x4〉   | xF ⇒ 〈xD,x2〉 ]
 | xF ⇒ match e2 with
  [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xF〉   | x2 ⇒ 〈x1,xE〉   | x3 ⇒ 〈x2,xD〉
  | x4 ⇒ 〈x3,xC〉   | x5 ⇒ 〈x4,xB〉   | x6 ⇒ 〈x5,xA〉   | x7 ⇒ 〈x6,x9〉
  | x8 ⇒ 〈x7,x8〉   | x9 ⇒ 〈x8,x7〉   | xA ⇒ 〈x9,x6〉   | xB ⇒ 〈xA,x5〉
  | xC ⇒ 〈xB,x4〉   | xD ⇒ 〈xC,x3〉   | xE ⇒ 〈xD,x2〉   | xF ⇒ 〈xE,x1〉 ]
 ].

(* correzione per somma su BCD *)
(* input: halfcarry,carry,X(BCD+BCD) *)
(* output: X',carry' *)
ndefinition daa_b8 ≝
λh,c:bool.λX:byte8.
 match lt_b8 X 〈x9,xA〉 with
  (* [X:0x00-0x99] *)
  (* c' = c *)
  (* X' = [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + [c=1 ? 0x60 : 0x00]
          [(b16l X):0xA-0xF] X + 0x06 + [c=1 ? 0x60 : 0x00] *)
  [ true ⇒
   let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
    [ true ⇒ X
    | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
   let X'' ≝ match c with
    [ true ⇒ plus_b8_d_d X' 〈x6,x0〉
    | false ⇒ X' ] in
   pair ?? X'' c
  (* [X:0x9A-0xFF] *)
  (* c' = 1 *)
  (* X' = [X:0x9A-0xFF]
          [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + 0x60
          [(b16l X):0xA-0xF] X + 0x6 + 0x60 *) 
  | false ⇒
   let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
    [ true ⇒ X
    | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
   let X'' ≝ plus_b8_d_d X' 〈x6,x0〉 in
   pair ?? X'' true
  ].

(* iteratore sui byte *)
ndefinition forall_byte8 ≝
 λP.
  forall_exadecim (λbh.
  forall_exadecim (λbl.
   P (mk_byte8 bh bl))).