]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_assembly/num/byte8.ma
freescale porting
[helm.git] / helm / software / matita / contribs / ng_assembly / num / 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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "num/exadecim.ma".
24 include "num/bitrigesim.ma".
25
26 (* **** *)
27 (* BYTE *)
28 (* **** *)
29
30 nrecord byte8 : Type ≝
31  {
32  b8h: exadecim;
33  b8l: exadecim
34  }.
35
36 (* \langle \rangle *)
37 notation "〈x,y〉" non associative with precedence 80
38  for @{ 'mk_byte8 $x $y }.
39 interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).
40
41 (* operatore = *)
42 ndefinition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)).
43
44 (* operatore < *)
45 ndefinition lt_b8 ≝
46 λb1,b2:byte8.
47  (lt_ex (b8h b1) (b8h b2)) ⊕
48  ((eq_ex (b8h b1) (b8h b2)) ⊗ (lt_ex (b8l b1) (b8l b2))).
49
50 (* operatore ≤ *)
51 ndefinition le_b8 ≝
52 λb1,b2:byte8.
53  (lt_ex (b8h b1) (b8h b2)) ⊕
54  ((eq_ex (b8h b1) (b8h b2)) ⊗ (le_ex (b8l b1) (b8l b2))).
55
56 (* operatore > *)
57 ndefinition gt_b8 ≝
58 λb1,b2:byte8.
59  (gt_ex (b8h b1) (b8h b2)) ⊕
60  ((eq_ex (b8h b1) (b8h b2)) ⊗ (gt_ex (b8l b1) (b8l b2))).
61
62 (* operatore ≥ *)
63 ndefinition ge_b8 ≝
64 λb1,b2:byte8.
65  (gt_ex (b8h b1) (b8h b2)) ⊕
66  ((eq_ex (b8h b1) (b8h b2)) ⊗ (ge_ex (b8l b1) (b8l b2))).
67
68 (* operatore and *)
69 ndefinition and_b8 ≝
70 λb1,b2:byte8.mk_byte8 (and_ex (b8h b1) (b8h b2)) (and_ex (b8l b1) (b8l b2)).
71
72 (* operatore or *)
73 ndefinition or_b8 ≝
74 λb1,b2:byte8.mk_byte8 (or_ex (b8h b1) (b8h b2)) (or_ex (b8l b1) (b8l b2)).
75
76 (* operatore xor *)
77 ndefinition xor_b8 ≝
78 λb1,b2:byte8.mk_byte8 (xor_ex (b8h b1) (b8h b2)) (xor_ex (b8l b1) (b8l b2)).
79
80 (* operatore rotazione destra con carry *)
81 ndefinition rcr_b8 ≝
82 λb:byte8.λc:bool.match rcr_ex (b8h b) c with
83  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
84   [ pair bl' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]]. 
85
86 (* operatore shift destro *)
87 ndefinition shr_b8 ≝
88 λb:byte8.match shr_ex (b8h b) with
89  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
90   [ pair bl' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
91
92 (* operatore rotazione destra *)
93 ndefinition ror_b8 ≝
94 λb:byte8.match shr_ex (b8h b) with
95  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
96   [ pair bl' c'' ⇒ match c'' with
97    [ true ⇒ mk_byte8 (or_ex x8 bh') bl'
98    | false ⇒ mk_byte8 bh' bl' ]]].
99
100 (* operatore rotazione destra n-volte *)
101 nlet rec ror_b8_n (b:byte8) (o:oct) (ro:rec_oct o) on ro ≝
102  match ro with
103   [ oc_O ⇒ b
104   | oc_S o' n' ⇒ ror_b8_n (ror_b8 b) o' n' ].
105
106 (* operatore rotazione sinistra con carry *)
107 ndefinition rcl_b8 ≝
108 λb:byte8.λc:bool.match rcl_ex (b8l b) c with
109  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
110   [ pair bh' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]]. 
111
112 (* operatore shift sinistro *)
113 ndefinition shl_b8 ≝
114 λb:byte8.match shl_ex (b8l b) with
115  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
116   [ pair bh' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
117
118 (* operatore rotazione sinistra *)
119 ndefinition rol_b8 ≝
120 λb:byte8.match shl_ex (b8l b) with
121  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
122   [ pair bh' c'' ⇒ match c'' with
123    [ true ⇒ mk_byte8 bh' (or_ex x1 bl')
124    | false ⇒ mk_byte8 bh' bl' ]]].
125
126 (* operatore rotazione sinistra n-volte *)
127 nlet rec rol_b8_n (b:byte8) (o:oct) (ro:rec_oct o) on ro ≝
128  match ro with
129   [ oc_O ⇒ b
130   | oc_S o' n' ⇒ rol_b8_n (rol_b8 b) o' n' ].
131
132 (* operatore not/complemento a 1 *)
133 ndefinition not_b8 ≝
134 λb:byte8.mk_byte8 (not_ex (b8h b)) (not_ex (b8l b)).
135
136 (* operatore somma con data+carry → data+carry *)
137 ndefinition plus_b8_dc_dc ≝
138 λb1,b2:byte8.λc:bool.
139  match plus_ex_dc_dc (b8l b1) (b8l b2) c with
140   [ pair l c' ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c' with
141    [ pair h c'' ⇒ pair … 〈h,l〉 c'' ]].
142
143 (* operatore somma con data+carry → data *)
144 ndefinition plus_b8_dc_d ≝
145 λb1,b2:byte8.λc:bool.
146  match plus_ex_dc_dc (b8l b1) (b8l b2) c with
147   [ pair l c' ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c',l〉 ].
148
149 (* operatore somma con data+carry → c *)
150 ndefinition plus_b8_dc_c ≝
151 λb1,b2:byte8.λc:bool.
152  plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_dc_c (b8l b1) (b8l b2) c).
153
154 (* operatore somma con data → data+carry *)
155 ndefinition plus_b8_d_dc ≝
156 λb1,b2:byte8.
157  match plus_ex_d_dc (b8l b1) (b8l b2) with
158   [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
159    [ pair h c' ⇒ pair … 〈h,l〉 c' ]].
160
161 (* operatore somma con data → data *)
162 ndefinition plus_b8_d_d ≝
163 λb1,b2:byte8.
164  match plus_ex_d_dc (b8l b1) (b8l b2) with
165   [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].
166
167 (* operatore somma con data → c *)
168 ndefinition plus_b8_d_c ≝
169 λb1,b2:byte8.
170  plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_d_c (b8l b1) (b8l b2)).
171
172 (* operatore Most Significant Bit *)
173 ndefinition MSB_b8 ≝ λb:byte8.eq_ex x8 (and_ex x8 (b8h b)).
174
175 (* operatore predecessore *)
176 ndefinition pred_b8 ≝
177 λb:byte8.match eq_ex (b8l b) x0 with
178  [ true ⇒ mk_byte8 (pred_ex (b8h b)) (pred_ex (b8l b))
179  | false ⇒ mk_byte8 (b8h b) (pred_ex (b8l b)) ]. 
180
181 (* operatore successore *)
182 ndefinition succ_b8 ≝
183 λb:byte8.match eq_ex (b8l b) xF with
184  [ true ⇒ mk_byte8 (succ_ex (b8h b)) (succ_ex (b8l b))
185  | false ⇒ mk_byte8 (b8h b) (succ_ex (b8l b)) ]. 
186
187 (* operatore neg/complemento a 2 *)
188 ndefinition compl_b8 ≝
189 λb:byte8.match MSB_b8 b with
190  [ true ⇒ succ_b8 (not_b8 b)
191  | false ⇒ not_b8 (pred_b8 b) ].
192
193 (* operatore moltiplicazione senza segno: e*e=[0x00,0xE1] *)
194 ndefinition mul_ex ≝
195 λe1,e2:exadecim.match e1 with
196  [ x0 ⇒ match e2 with
197   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x0〉   | x2 ⇒ 〈x0,x0〉   | x3 ⇒ 〈x0,x0〉
198   | x4 ⇒ 〈x0,x0〉   | x5 ⇒ 〈x0,x0〉   | x6 ⇒ 〈x0,x0〉   | x7 ⇒ 〈x0,x0〉
199   | x8 ⇒ 〈x0,x0〉   | x9 ⇒ 〈x0,x0〉   | xA ⇒ 〈x0,x0〉   | xB ⇒ 〈x0,x0〉
200   | xC ⇒ 〈x0,x0〉   | xD ⇒ 〈x0,x0〉   | xE ⇒ 〈x0,x0〉   | xF ⇒ 〈x0,x0〉 ]
201  | x1 ⇒ match e2 with
202   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x1〉   | x2 ⇒ 〈x0,x2〉   | x3 ⇒ 〈x0,x3〉
203   | x4 ⇒ 〈x0,x4〉   | x5 ⇒ 〈x0,x5〉   | x6 ⇒ 〈x0,x6〉   | x7 ⇒ 〈x0,x7〉
204   | x8 ⇒ 〈x0,x8〉   | x9 ⇒ 〈x0,x9〉   | xA ⇒ 〈x0,xA〉   | xB ⇒ 〈x0,xB〉
205   | xC ⇒ 〈x0,xC〉   | xD ⇒ 〈x0,xD〉   | xE ⇒ 〈x0,xE〉   | xF ⇒ 〈x0,xF〉 ]
206  | x2 ⇒ match e2 with
207   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x2〉   | x2 ⇒ 〈x0,x4〉   | x3 ⇒ 〈x0,x6〉
208   | x4 ⇒ 〈x0,x8〉   | x5 ⇒ 〈x0,xA〉   | x6 ⇒ 〈x0,xC〉   | x7 ⇒ 〈x0,xE〉
209   | x8 ⇒ 〈x1,x0〉   | x9 ⇒ 〈x1,x2〉   | xA ⇒ 〈x1,x4〉   | xB ⇒ 〈x1,x6〉
210   | xC ⇒ 〈x1,x8〉   | xD ⇒ 〈x1,xA〉   | xE ⇒ 〈x1,xC〉   | xF ⇒ 〈x1,xE〉 ]
211  | x3 ⇒ match e2 with
212   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x3〉   | x2 ⇒ 〈x0,x6〉   | x3 ⇒ 〈x0,x9〉
213   | x4 ⇒ 〈x0,xC〉   | x5 ⇒ 〈x0,xF〉   | x6 ⇒ 〈x1,x2〉   | x7 ⇒ 〈x1,x5〉
214   | x8 ⇒ 〈x1,x8〉   | x9 ⇒ 〈x1,xB〉   | xA ⇒ 〈x1,xE〉   | xB ⇒ 〈x2,x1〉
215   | xC ⇒ 〈x2,x4〉   | xD ⇒ 〈x2,x7〉   | xE ⇒ 〈x2,xA〉   | xF ⇒ 〈x2,xD〉 ]
216  | x4 ⇒ match e2 with
217   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x4〉   | x2 ⇒ 〈x0,x8〉   | x3 ⇒ 〈x0,xC〉
218   | x4 ⇒ 〈x1,x0〉   | x5 ⇒ 〈x1,x4〉   | x6 ⇒ 〈x1,x8〉   | x7 ⇒ 〈x1,xC〉
219   | x8 ⇒ 〈x2,x0〉   | x9 ⇒ 〈x2,x4〉   | xA ⇒ 〈x2,x8〉   | xB ⇒ 〈x2,xC〉
220   | xC ⇒ 〈x3,x0〉   | xD ⇒ 〈x3,x4〉   | xE ⇒ 〈x3,x8〉   | xF ⇒ 〈x3,xC〉 ]
221  | x5 ⇒ match e2 with
222   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x5〉   | x2 ⇒ 〈x0,xA〉   | x3 ⇒ 〈x0,xF〉
223   | x4 ⇒ 〈x1,x4〉   | x5 ⇒ 〈x1,x9〉   | x6 ⇒ 〈x1,xE〉   | x7 ⇒ 〈x2,x3〉
224   | x8 ⇒ 〈x2,x8〉   | x9 ⇒ 〈x2,xD〉   | xA ⇒ 〈x3,x2〉   | xB ⇒ 〈x3,x7〉
225   | xC ⇒ 〈x3,xC〉   | xD ⇒ 〈x4,x1〉   | xE ⇒ 〈x4,x6〉   | xF ⇒ 〈x4,xB〉 ]
226  | x6 ⇒ match e2 with
227   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x6〉   | x2 ⇒ 〈x0,xC〉   | x3 ⇒ 〈x1,x2〉
228   | x4 ⇒ 〈x1,x8〉   | x5 ⇒ 〈x1,xE〉   | x6 ⇒ 〈x2,x4〉   | x7 ⇒ 〈x2,xA〉
229   | x8 ⇒ 〈x3,x0〉   | x9 ⇒ 〈x3,x6〉   | xA ⇒ 〈x3,xC〉   | xB ⇒ 〈x4,x2〉
230   | xC ⇒ 〈x4,x8〉   | xD ⇒ 〈x4,xE〉   | xE ⇒ 〈x5,x4〉   | xF ⇒ 〈x5,xA〉 ]
231  | x7 ⇒ match e2 with
232   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x7〉   | x2 ⇒ 〈x0,xE〉   | x3 ⇒ 〈x1,x5〉
233   | x4 ⇒ 〈x1,xC〉   | x5 ⇒ 〈x2,x3〉   | x6 ⇒ 〈x2,xA〉   | x7 ⇒ 〈x3,x1〉
234   | x8 ⇒ 〈x3,x8〉   | x9 ⇒ 〈x3,xF〉   | xA ⇒ 〈x4,x6〉   | xB ⇒ 〈x4,xD〉
235   | xC ⇒ 〈x5,x4〉   | xD ⇒ 〈x5,xB〉   | xE ⇒ 〈x6,x2〉   | xF ⇒ 〈x6,x9〉 ]
236  | x8 ⇒ match e2 with
237   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x8〉   | x2 ⇒ 〈x1,x0〉   | x3 ⇒ 〈x1,x8〉
238   | x4 ⇒ 〈x2,x0〉   | x5 ⇒ 〈x2,x8〉   | x6 ⇒ 〈x3,x0〉   | x7 ⇒ 〈x3,x8〉
239   | x8 ⇒ 〈x4,x0〉   | x9 ⇒ 〈x4,x8〉   | xA ⇒ 〈x5,x0〉   | xB ⇒ 〈x5,x8〉
240   | xC ⇒ 〈x6,x0〉   | xD ⇒ 〈x6,x8〉   | xE ⇒ 〈x7,x0〉   | xF ⇒ 〈x7,x8〉 ]
241  | x9 ⇒ match e2 with
242   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x9〉   | x2 ⇒ 〈x1,x2〉   | x3 ⇒ 〈x1,xB〉
243   | x4 ⇒ 〈x2,x4〉   | x5 ⇒ 〈x2,xD〉   | x6 ⇒ 〈x3,x6〉   | x7 ⇒ 〈x3,xF〉
244   | x8 ⇒ 〈x4,x8〉   | x9 ⇒ 〈x5,x1〉   | xA ⇒ 〈x5,xA〉   | xB ⇒ 〈x6,x3〉
245   | xC ⇒ 〈x6,xC〉   | xD ⇒ 〈x7,x5〉   | xE ⇒ 〈x7,xE〉   | xF ⇒ 〈x8,x7〉 ]
246  | xA ⇒ match e2 with
247   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xA〉   | x2 ⇒ 〈x1,x4〉   | x3 ⇒ 〈x1,xE〉
248   | x4 ⇒ 〈x2,x8〉   | x5 ⇒ 〈x3,x2〉   | x6 ⇒ 〈x3,xC〉   | x7 ⇒ 〈x4,x6〉
249   | x8 ⇒ 〈x5,x0〉   | x9 ⇒ 〈x5,xA〉   | xA ⇒ 〈x6,x4〉   | xB ⇒ 〈x6,xE〉
250   | xC ⇒ 〈x7,x8〉   | xD ⇒ 〈x8,x2〉   | xE ⇒ 〈x8,xC〉   | xF ⇒ 〈x9,x6〉 ]
251  | xB ⇒ match e2 with
252   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xB〉   | x2 ⇒ 〈x1,x6〉   | x3 ⇒ 〈x2,x1〉
253   | x4 ⇒ 〈x2,xC〉   | x5 ⇒ 〈x3,x7〉   | x6 ⇒ 〈x4,x2〉   | x7 ⇒ 〈x4,xD〉
254   | x8 ⇒ 〈x5,x8〉   | x9 ⇒ 〈x6,x3〉   | xA ⇒ 〈x6,xE〉   | xB ⇒ 〈x7,x9〉
255   | xC ⇒ 〈x8,x4〉   | xD ⇒ 〈x8,xF〉   | xE ⇒ 〈x9,xA〉   | xF ⇒ 〈xA,x5〉 ]
256  | xC ⇒ match e2 with
257   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xC〉   | x2 ⇒ 〈x1,x8〉   | x3 ⇒ 〈x2,x4〉
258   | x4 ⇒ 〈x3,x0〉   | x5 ⇒ 〈x3,xC〉   | x6 ⇒ 〈x4,x8〉   | x7 ⇒ 〈x5,x4〉
259   | x8 ⇒ 〈x6,x0〉   | x9 ⇒ 〈x6,xC〉   | xA ⇒ 〈x7,x8〉   | xB ⇒ 〈x8,x4〉
260   | xC ⇒ 〈x9,x0〉   | xD ⇒ 〈x9,xC〉   | xE ⇒ 〈xA,x8〉   | xF ⇒ 〈xB,x4〉 ]
261  | xD ⇒ match e2 with
262   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xD〉   | x2 ⇒ 〈x1,xA〉   | x3 ⇒ 〈x2,x7〉
263   | x4 ⇒ 〈x3,x4〉   | x5 ⇒ 〈x4,x1〉   | x6 ⇒ 〈x4,xE〉   | x7 ⇒ 〈x5,xB〉
264   | x8 ⇒ 〈x6,x8〉   | x9 ⇒ 〈x7,x5〉   | xA ⇒ 〈x8,x2〉   | xB ⇒ 〈x8,xF〉
265   | xC ⇒ 〈x9,xC〉   | xD ⇒ 〈xA,x9〉   | xE ⇒ 〈xB,x6〉   | xF ⇒ 〈xC,x3〉 ]
266  | xE ⇒ match e2 with
267   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xE〉   | x2 ⇒ 〈x1,xC〉   | x3 ⇒ 〈x2,xA〉
268   | x4 ⇒ 〈x3,x8〉   | x5 ⇒ 〈x4,x6〉   | x6 ⇒ 〈x5,x4〉   | x7 ⇒ 〈x6,x2〉
269   | x8 ⇒ 〈x7,x0〉   | x9 ⇒ 〈x7,xE〉   | xA ⇒ 〈x8,xC〉   | xB ⇒ 〈x9,xA〉
270   | xC ⇒ 〈xA,x8〉   | xD ⇒ 〈xB,x6〉   | xE ⇒ 〈xC,x4〉   | xF ⇒ 〈xD,x2〉 ]
271  | xF ⇒ match e2 with
272   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xF〉   | x2 ⇒ 〈x1,xE〉   | x3 ⇒ 〈x2,xD〉
273   | x4 ⇒ 〈x3,xC〉   | x5 ⇒ 〈x4,xB〉   | x6 ⇒ 〈x5,xA〉   | x7 ⇒ 〈x6,x9〉
274   | x8 ⇒ 〈x7,x8〉   | x9 ⇒ 〈x8,x7〉   | xA ⇒ 〈x9,x6〉   | xB ⇒ 〈xA,x5〉
275   | xC ⇒ 〈xB,x4〉   | xD ⇒ 〈xC,x3〉   | xE ⇒ 〈xD,x2〉   | xF ⇒ 〈xE,x1〉 ]
276  ].
277
278 (* correzione per somma su BCD *)
279 (* input: halfcarry,carry,X(BCD+BCD) *)
280 (* output: X',carry' *)
281 ndefinition daa_b8 ≝
282 λh,c:bool.λX:byte8.
283  match lt_b8 X 〈x9,xA〉 with
284   (* [X:0x00-0x99] *)
285   (* c' = c *)
286   (* X' = [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + [c=1 ? 0x60 : 0x00]
287           [(b16l X):0xA-0xF] X + 0x06 + [c=1 ? 0x60 : 0x00] *)
288   [ true ⇒
289    let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
290     [ true ⇒ X
291     | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
292    let X'' ≝ match c with
293     [ true ⇒ plus_b8_d_d X' 〈x6,x0〉
294     | false ⇒ X' ] in
295    pair … X'' c
296   (* [X:0x9A-0xFF] *)
297   (* c' = 1 *)
298   (* X' = [X:0x9A-0xFF]
299           [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + 0x60
300           [(b16l X):0xA-0xF] X + 0x6 + 0x60 *) 
301   | false ⇒
302    let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
303     [ true ⇒ X
304     | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
305    let X'' ≝ plus_b8_d_d X' 〈x6,x0〉 in
306    pair … X'' true
307   ].
308
309 (* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
310 nlet rec div_b8_ex_aux (divd:byte8) (divs:byte8) (molt:exadecim) (q:exadecim) (qu:quatern) (rqu:rec_quatern qu) on rqu ≝
311  let w' ≝ plus_b8_d_d divd (compl_b8 divs) in
312   match rqu with
313   [ qu_O ⇒ match le_b8 divs divd with
314    [ true ⇒ triple … (or_ex molt q) (b8l w') (⊖ (eq_ex (b8h w') x0))
315    | false ⇒ triple … q (b8l divd) (⊖ (eq_ex (b8h divd) x0)) ]
316   | qu_S qu' rqu' ⇒ match le_b8 divs divd with
317    [ true ⇒ div_b8_ex_aux w' (ror_b8 divs) (ror_ex molt) (or_ex molt q) qu' rqu'
318    | false ⇒ div_b8_ex_aux divd (ror_b8 divs) (ror_ex molt) q qu' rqu' ]].
319
320 ndefinition div_b8_ex ≝
321 λb:byte8.λe:exadecim.match eq_ex e x0 with
322 (* 
323    la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato
324 *)
325  [ true ⇒ triple … xF (b8l b) true
326  | false ⇒ match eq_b8 b 〈x0,x0〉 with
327 (* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *)
328   [ true ⇒ triple … x0 x0 false
329 (* 1) e' una divisione sensata che produrra' overflow/risultato *)
330 (* 2) parametri: dividendo, divisore, moltiplicatore, quoziente, contatore *)
331 (* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
332 (* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
333 (*    puo' essere sottratto al dividendo *) 
334   | false ⇒ div_b8_ex_aux b (rol_b8_n 〈x0,e〉 ? (oct_to_recoct o3)) x8 x0 ? (qu_to_recqu q3) ]].
335
336 (* operatore x in [inf,sup] o in sup],[inf *)
337 ndefinition inrange_b8 ≝
338 λx,inf,sup:byte8.
339  match le_b8 inf sup with
340   [ true ⇒ and_bool | false ⇒ or_bool ]
341  (le_b8 inf x) (le_b8 x sup).
342
343 (* iteratore sui byte *)
344 ndefinition forall_b8 ≝
345  λP.
346   forall_ex (λbh.
347   forall_ex (λbl.
348    P (mk_byte8 bh bl))).
349
350 (* byte ricorsivi *)
351 ninductive rec_byte8 : byte8 → Type ≝
352   b8_O : rec_byte8 〈x0,x0〉
353 | b8_S : ∀n.rec_byte8 n → rec_byte8 (succ_b8 n).
354
355 (* byte → byte ricorsivi *)
356 ndefinition b8_to_recb8_aux1 : Πn.rec_byte8 〈n,x0〉 → rec_byte8 〈succ_ex n,x0〉 ≝
357 λn.λrecb:rec_byte8 〈n,x0〉.
358  b8_S 〈n,xF〉 (b8_S 〈n,xE〉 (b8_S 〈n,xD〉 (b8_S 〈n,xC〉 (
359  b8_S 〈n,xB〉 (b8_S 〈n,xA〉 (b8_S 〈n,x9〉 (b8_S 〈n,x8〉 (
360  b8_S 〈n,x7〉 (b8_S 〈n,x6〉 (b8_S 〈n,x5〉 (b8_S 〈n,x4〉 (
361  b8_S 〈n,x3〉 (b8_S 〈n,x2〉 (b8_S 〈n,x1〉 (b8_S 〈n,x0〉 recb))))))))))))))).
362
363 (* ... cifra esadecimale superiore *)
364 nlet rec b8_to_recb8_aux2 (n:exadecim) (r:rec_exadecim n) on r ≝
365  match r return λx.λy:rec_exadecim x.rec_byte8 〈x,x0〉 with
366   [ ex_O ⇒ b8_O
367   | ex_S t n' ⇒ b8_to_recb8_aux1 ? (b8_to_recb8_aux2 t n')
368   ].
369
370 (* ... cifra esadecimale inferiore *)
371 ndefinition b8_to_recb8_aux3 : Πn1,n2.rec_byte8 〈n1,x0〉 → rec_byte8 〈n1,n2〉 ≝
372 λn1,n2.λrecb:rec_byte8 〈n1,x0〉.
373  match n2 return λx.rec_byte8 〈n1,x〉 with
374   [ x0 ⇒ recb
375   | x1 ⇒ b8_S 〈n1,x0〉 recb
376   | x2 ⇒ b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)
377   | x3 ⇒ b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))
378   | x4 ⇒ b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))
379   | x5 ⇒ b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
380          b8_S 〈n1,x0〉 recb))))
381   | x6 ⇒ b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
382          b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))
383   | x7 ⇒ b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
384          b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))
385   | x8 ⇒ b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (
386          b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))
387   | x9 ⇒ b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (
388          b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
389          b8_S 〈n1,x0〉 recb))))))))
390   | xA ⇒ b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (
391          b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
392          b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))
393   | xB ⇒ b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (
394          b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
395          b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))))))
396   | xC ⇒ b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (
397          b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (
398          b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))))
399   | xD ⇒ b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (
400          b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (
401          b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
402          b8_S 〈n1,x0〉 recb))))))))))))
403   | xE ⇒ b8_S 〈n1,xD〉 (b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (
404          b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (
405          b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
406          b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))))))
407   | xF ⇒ b8_S 〈n1,xE〉 (b8_S 〈n1,xD〉 (b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (
408          b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (
409          b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
410          b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))))))))))
411   ].
412
413 (*
414 nlemma b8_to_recb8 : Πb.rec_byte8 b.
415  #b; nletin K ≝ (b8_to_recb8_aux3 
416      (b8h b) (b8l b) (b8_to_recb8_aux2 (b8h b) (ex_to_recex (b8h b))));
417  ncases b in K; #e1; #e2; #K; napply K;
418 nqed.
419 *)
420
421 ndefinition b8_to_recb8 : Πb.rec_byte8 b ≝
422 λb.match b with [ mk_byte8 h l ⇒ b8_to_recb8_aux3 h l (b8_to_recb8_aux2 h (ex_to_recex h)) ].
423
424 (* ottali → esadecimali *)
425 ndefinition b8_of_bit ≝
426 λn.match n with
427  [ t00 ⇒ 〈x0,x0〉 | t01 ⇒ 〈x0,x1〉 | t02 ⇒ 〈x0,x2〉 | t03 ⇒ 〈x0,x3〉
428  | t04 ⇒ 〈x0,x4〉 | t05 ⇒ 〈x0,x5〉 | t06 ⇒ 〈x0,x6〉 | t07 ⇒ 〈x0,x7〉
429  | t08 ⇒ 〈x0,x8〉 | t09 ⇒ 〈x0,x9〉 | t0A ⇒ 〈x0,xA〉 | t0B ⇒ 〈x0,xB〉
430  | t0C ⇒ 〈x0,xC〉 | t0D ⇒ 〈x0,xD〉 | t0E ⇒ 〈x0,xE〉 | t0F ⇒ 〈x0,xF〉
431  | t10 ⇒ 〈x1,x0〉 | t11 ⇒ 〈x1,x1〉 | t12 ⇒ 〈x1,x2〉 | t13 ⇒ 〈x1,x3〉
432  | t14 ⇒ 〈x1,x4〉 | t15 ⇒ 〈x1,x5〉 | t16 ⇒ 〈x1,x6〉 | t17 ⇒ 〈x1,x7〉
433  | t18 ⇒ 〈x1,x8〉 | t19 ⇒ 〈x1,x9〉 | t1A ⇒ 〈x1,xA〉 | t1B ⇒ 〈x1,xB〉
434  | t1C ⇒ 〈x1,xC〉 | t1D ⇒ 〈x1,xD〉 | t1E ⇒ 〈x1,xE〉 | t1F ⇒ 〈x1,xF〉
435  ].