]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_assembly/freescale/byte8.ma
(no commit message)
[helm.git] / helm / software / matita / contribs / ng_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 (* BYTE *)
31 (* **** *)
32
33 nrecord byte8 : Type ≝
34  {
35  b8h: exadecim;
36  b8l: exadecim
37  }.
38
39 ndefinition byte8_ind : ΠP:byte8 → Prop.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
40 λP:byte8 → Prop.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
41  match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
42
43 ndefinition byte8_rec : ΠP:byte8 → Set.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
44 λP:byte8 → Set.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
45  match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
46
47 ndefinition byte8_rect : ΠP:byte8 → Type.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
48 λP:byte8 → Type.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
49  match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
50
51 ndefinition b8h ≝ λb:byte8.match b with [ mk_byte8 x _ ⇒ x ].
52 ndefinition b8l ≝ λb:byte8.match b with [ mk_byte8 _ x ⇒ x ].
53
54 (* \langle \rangle *)
55 notation "〈x,y〉" non associative with precedence 80
56  for @{ 'mk_byte8 $x $y }.
57 interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).
58
59 (* operatore = *)
60 ndefinition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)).
61
62 (* operatore < *)
63 ndefinition lt_b8 ≝
64 λb1,b2:byte8.match lt_ex (b8h b1) (b8h b2) with
65  [ true ⇒ true
66  | false ⇒ match gt_ex (b8h b1) (b8h b2) with
67   [ true ⇒ false
68   | false ⇒ lt_ex (b8l b1) (b8l b2) ]].
69
70 (* operatore ≤ *)
71 ndefinition le_b8 ≝ λb1,b2:byte8.(eq_b8 b1 b2) ⊕ (lt_b8 b1 b2). 
72
73 (* operatore > *)
74 ndefinition gt_b8 ≝ λb1,b2:byte8.⊖ (le_b8 b1 b2).
75
76 (* operatore ≥ *)
77 ndefinition ge_b8 ≝ λb1,b2:byte8.⊖ (lt_b8 b1 b2).
78
79 (* operatore and *)
80 ndefinition and_b8 ≝
81 λb1,b2:byte8.mk_byte8 (and_ex (b8h b1) (b8h b2)) (and_ex (b8l b1) (b8l b2)).
82
83 (* operatore or *)
84 ndefinition or_b8 ≝
85 λb1,b2:byte8.mk_byte8 (or_ex (b8h b1) (b8h b2)) (or_ex (b8l b1) (b8l b2)).
86
87 (* operatore xor *)
88 ndefinition xor_b8 ≝
89 λb1,b2:byte8.mk_byte8 (xor_ex (b8h b1) (b8h b2)) (xor_ex (b8l b1) (b8l b2)).
90
91 (* operatore rotazione destra con carry *)
92 ndefinition rcr_b8 ≝
93 λb:byte8.λc:bool.match rcr_ex (b8h b) c with
94  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
95   [ pair bl' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]]. 
96
97 (* operatore shift destro *)
98 ndefinition shr_b8 ≝
99 λb:byte8.match rcr_ex (b8h b) false with
100  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
101   [ pair bl' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
102
103 (* operatore rotazione destra *)
104 ndefinition ror_b8 ≝
105 λb:byte8.match rcr_ex (b8h b) false with
106  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
107   [ pair bl' c'' ⇒ match c'' with
108    [ true ⇒ mk_byte8 (or_ex x8 bh') bl'
109    | false ⇒ mk_byte8 bh' bl' ]]].
110
111 (* operatore rotazione destra n-volte *)
112 nlet rec ror_b8_n (b:byte8) (n:nat) on n ≝
113  match n with
114   [ O ⇒ b
115   | S n' ⇒ ror_b8_n (ror_b8 b) n' ].
116
117 (* operatore rotazione sinistra con carry *)
118 ndefinition rcl_b8 ≝
119 λb:byte8.λc:bool.match rcl_ex (b8l b) c with
120  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
121   [ pair bh' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]]. 
122
123 (* operatore shift sinistro *)
124 ndefinition shl_b8 ≝
125 λb:byte8.match rcl_ex (b8l b) false with
126  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
127   [ pair bh' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
128
129 (* operatore rotazione sinistra *)
130 ndefinition rol_b8 ≝
131 λb:byte8.match rcl_ex (b8l b) false with
132  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
133   [ pair bh' c'' ⇒ match c'' with
134    [ true ⇒ mk_byte8 bh' (or_ex x1 bl')
135    | false ⇒ mk_byte8 bh' bl' ]]].
136
137 (* operatore rotazione sinistra n-volte *)
138 nlet rec rol_b8_n (b:byte8) (n:nat) on n ≝
139  match n with
140   [ O ⇒ b
141   | S n' ⇒ rol_b8_n (rol_b8 b) n' ].
142
143 (* operatore not/complemento a 1 *)
144 ndefinition not_b8 ≝
145 λb:byte8.mk_byte8 (not_ex (b8h b)) (not_ex (b8l b)).
146
147 (* operatore somma con data+carry → data+carry *)
148 ndefinition plus_b8_dc_dc ≝
149 λb1,b2:byte8.λc:bool.
150  match plus_ex_dc_dc (b8l b1) (b8l b2) c with
151   [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
152    [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]].
153
154 (* operatore somma con data+carry → data *)
155 ndefinition plus_b8_dc_d ≝
156 λb1,b2:byte8.λc:bool.
157  match plus_ex_dc_dc (b8l b1) (b8l b2) c with
158   [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].
159
160 (* operatore somma con data+carry → c *)
161 ndefinition plus_b8_dc_c ≝
162 λb1,b2:byte8.λc:bool.
163  plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_dc_c (b8l b1) (b8l b2) c).
164
165 (* operatore somma con data → data+carry *)
166 ndefinition plus_b8_d_dc ≝
167 λb1,b2:byte8.
168  match plus_ex_d_dc (b8l b1) (b8l b2) with
169   [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
170    [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]].
171
172 (* operatore somma con data → data *)
173 ndefinition plus_b8_d_d ≝
174 λb1,b2:byte8.
175  match plus_ex_d_dc (b8l b1) (b8l b2) with
176   [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].
177
178 (* operatore somma con data → c *)
179 ndefinition plus_b8_d_c ≝
180 λb1,b2:byte8.
181  plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_d_c (b8l b1) (b8l b2)).
182
183 (* operatore Most Significant Bit *)
184 ndefinition MSB_b8 ≝ λb:byte8.eq_ex x8 (and_ex x8 (b8h b)).
185
186 (* byte → naturali *)
187 ndefinition nat_of_byte8 ≝ λb:byte8.(16*(nat_of_exadecim (b8h b))) + (nat_of_exadecim (b8l b)).
188
189 (* operatore predecessore *)
190 ndefinition pred_b8 ≝
191 λb:byte8.match eq_ex (b8l b) x0 with
192  [ true ⇒ mk_byte8 (pred_ex (b8h b)) (pred_ex (b8l b))
193  | false ⇒ mk_byte8 (b8h b) (pred_ex (b8l b)) ]. 
194
195 (* operatore successore *)
196 ndefinition succ_b8 ≝
197 λb:byte8.match eq_ex (b8l b) xF with
198  [ true ⇒ mk_byte8 (succ_ex (b8h b)) (succ_ex (b8l b))
199  | false ⇒ mk_byte8 (b8h b) (succ_ex (b8l b)) ]. 
200
201 (* operatore neg/complemento a 2 *)
202 ndefinition compl_b8 ≝
203 λb:byte8.match MSB_b8 b with
204  [ true ⇒ succ_b8 (not_b8 b)
205  | false ⇒ not_b8 (pred_b8 b) ].
206
207 (* operatore moltiplicazione senza segno: e*e=[0x00,0xE1] *)
208 ndefinition mul_ex ≝
209 λe1,e2:exadecim.match e1 with
210  [ x0 ⇒ match e2 with
211   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x0〉   | x2 ⇒ 〈x0,x0〉   | x3 ⇒ 〈x0,x0〉
212   | x4 ⇒ 〈x0,x0〉   | x5 ⇒ 〈x0,x0〉   | x6 ⇒ 〈x0,x0〉   | x7 ⇒ 〈x0,x0〉
213   | x8 ⇒ 〈x0,x0〉   | x9 ⇒ 〈x0,x0〉   | xA ⇒ 〈x0,x0〉   | xB ⇒ 〈x0,x0〉
214   | xC ⇒ 〈x0,x0〉   | xD ⇒ 〈x0,x0〉   | xE ⇒ 〈x0,x0〉   | xF ⇒ 〈x0,x0〉 ]
215  | x1 ⇒ match e2 with
216   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x1〉   | x2 ⇒ 〈x0,x2〉   | x3 ⇒ 〈x0,x3〉
217   | x4 ⇒ 〈x0,x4〉   | x5 ⇒ 〈x0,x5〉   | x6 ⇒ 〈x0,x6〉   | x7 ⇒ 〈x0,x7〉
218   | x8 ⇒ 〈x0,x8〉   | x9 ⇒ 〈x0,x9〉   | xA ⇒ 〈x0,xA〉   | xB ⇒ 〈x0,xB〉
219   | xC ⇒ 〈x0,xC〉   | xD ⇒ 〈x0,xD〉   | xE ⇒ 〈x0,xE〉   | xF ⇒ 〈x0,xF〉 ]
220  | x2 ⇒ match e2 with
221   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x2〉   | x2 ⇒ 〈x0,x4〉   | x3 ⇒ 〈x0,x6〉
222   | x4 ⇒ 〈x0,x8〉   | x5 ⇒ 〈x0,xA〉   | x6 ⇒ 〈x0,xC〉   | x7 ⇒ 〈x0,xE〉
223   | x8 ⇒ 〈x1,x0〉   | x9 ⇒ 〈x1,x2〉   | xA ⇒ 〈x1,x4〉   | xB ⇒ 〈x1,x6〉
224   | xC ⇒ 〈x1,x8〉   | xD ⇒ 〈x1,xA〉   | xE ⇒ 〈x1,xC〉   | xF ⇒ 〈x1,xE〉 ]
225  | x3 ⇒ match e2 with
226   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x3〉   | x2 ⇒ 〈x0,x6〉   | x3 ⇒ 〈x0,x9〉
227   | x4 ⇒ 〈x0,xC〉   | x5 ⇒ 〈x0,xF〉   | x6 ⇒ 〈x1,x2〉   | x7 ⇒ 〈x1,x5〉
228   | x8 ⇒ 〈x1,x8〉   | x9 ⇒ 〈x1,xB〉   | xA ⇒ 〈x1,xE〉   | xB ⇒ 〈x2,x1〉
229   | xC ⇒ 〈x2,x4〉   | xD ⇒ 〈x2,x7〉   | xE ⇒ 〈x2,xA〉   | xF ⇒ 〈x2,xD〉 ]
230  | x4 ⇒ match e2 with
231   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x4〉   | x2 ⇒ 〈x0,x8〉   | x3 ⇒ 〈x0,xC〉
232   | x4 ⇒ 〈x1,x0〉   | x5 ⇒ 〈x1,x4〉   | x6 ⇒ 〈x1,x8〉   | x7 ⇒ 〈x1,xC〉
233   | x8 ⇒ 〈x2,x0〉   | x9 ⇒ 〈x2,x4〉   | xA ⇒ 〈x2,x8〉   | xB ⇒ 〈x2,xC〉
234   | xC ⇒ 〈x3,x0〉   | xD ⇒ 〈x3,x4〉   | xE ⇒ 〈x3,x8〉   | xF ⇒ 〈x3,xC〉 ]
235  | x5 ⇒ match e2 with
236   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x5〉   | x2 ⇒ 〈x0,xA〉   | x3 ⇒ 〈x0,xF〉
237   | x4 ⇒ 〈x1,x4〉   | x5 ⇒ 〈x1,x9〉   | x6 ⇒ 〈x1,xE〉   | x7 ⇒ 〈x2,x3〉
238   | x8 ⇒ 〈x2,x8〉   | x9 ⇒ 〈x2,xD〉   | xA ⇒ 〈x3,x2〉   | xB ⇒ 〈x3,x7〉
239   | xC ⇒ 〈x3,xC〉   | xD ⇒ 〈x4,x1〉   | xE ⇒ 〈x4,x6〉   | xF ⇒ 〈x4,xB〉 ]
240  | x6 ⇒ match e2 with
241   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x6〉   | x2 ⇒ 〈x0,xC〉   | x3 ⇒ 〈x1,x2〉
242   | x4 ⇒ 〈x1,x8〉   | x5 ⇒ 〈x1,xE〉   | x6 ⇒ 〈x2,x4〉   | x7 ⇒ 〈x2,xA〉
243   | x8 ⇒ 〈x3,x0〉   | x9 ⇒ 〈x3,x6〉   | xA ⇒ 〈x3,xC〉   | xB ⇒ 〈x4,x2〉
244   | xC ⇒ 〈x4,x8〉   | xD ⇒ 〈x4,xE〉   | xE ⇒ 〈x5,x4〉   | xF ⇒ 〈x5,xA〉 ]
245  | x7 ⇒ match e2 with
246   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x7〉   | x2 ⇒ 〈x0,xE〉   | x3 ⇒ 〈x1,x5〉
247   | x4 ⇒ 〈x1,xC〉   | x5 ⇒ 〈x2,x3〉   | x6 ⇒ 〈x2,xA〉   | x7 ⇒ 〈x3,x1〉
248   | x8 ⇒ 〈x3,x8〉   | x9 ⇒ 〈x3,xF〉   | xA ⇒ 〈x4,x6〉   | xB ⇒ 〈x4,xD〉
249   | xC ⇒ 〈x5,x4〉   | xD ⇒ 〈x5,xB〉   | xE ⇒ 〈x6,x2〉   | xF ⇒ 〈x6,x9〉 ]
250  | x8 ⇒ match e2 with
251   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x8〉   | x2 ⇒ 〈x1,x0〉   | x3 ⇒ 〈x1,x8〉
252   | x4 ⇒ 〈x2,x0〉   | x5 ⇒ 〈x2,x8〉   | x6 ⇒ 〈x3,x0〉   | x7 ⇒ 〈x3,x8〉
253   | x8 ⇒ 〈x4,x0〉   | x9 ⇒ 〈x4,x8〉   | xA ⇒ 〈x5,x0〉   | xB ⇒ 〈x5,x8〉
254   | xC ⇒ 〈x6,x0〉   | xD ⇒ 〈x6,x8〉   | xE ⇒ 〈x7,x0〉   | xF ⇒ 〈x7,x8〉 ]
255  | x9 ⇒ match e2 with
256   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,x9〉   | x2 ⇒ 〈x1,x2〉   | x3 ⇒ 〈x1,xB〉
257   | x4 ⇒ 〈x2,x4〉   | x5 ⇒ 〈x2,xD〉   | x6 ⇒ 〈x3,x6〉   | x7 ⇒ 〈x3,xF〉
258   | x8 ⇒ 〈x4,x8〉   | x9 ⇒ 〈x5,x1〉   | xA ⇒ 〈x5,xA〉   | xB ⇒ 〈x6,x3〉
259   | xC ⇒ 〈x6,xC〉   | xD ⇒ 〈x7,x5〉   | xE ⇒ 〈x7,xE〉   | xF ⇒ 〈x8,x7〉 ]
260  | xA ⇒ match e2 with
261   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xA〉   | x2 ⇒ 〈x1,x4〉   | x3 ⇒ 〈x1,xE〉
262   | x4 ⇒ 〈x2,x8〉   | x5 ⇒ 〈x3,x2〉   | x6 ⇒ 〈x3,xC〉   | x7 ⇒ 〈x4,x6〉
263   | x8 ⇒ 〈x5,x0〉   | x9 ⇒ 〈x5,xA〉   | xA ⇒ 〈x6,x4〉   | xB ⇒ 〈x6,xE〉
264   | xC ⇒ 〈x7,x8〉   | xD ⇒ 〈x8,x2〉   | xE ⇒ 〈x8,xC〉   | xF ⇒ 〈x9,x6〉 ]
265  | xB ⇒ match e2 with
266   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xB〉   | x2 ⇒ 〈x1,x6〉   | x3 ⇒ 〈x2,x1〉
267   | x4 ⇒ 〈x2,xC〉   | x5 ⇒ 〈x3,x7〉   | x6 ⇒ 〈x4,x2〉   | x7 ⇒ 〈x4,xD〉
268   | x8 ⇒ 〈x5,x8〉   | x9 ⇒ 〈x6,x3〉   | xA ⇒ 〈x6,xE〉   | xB ⇒ 〈x7,x9〉
269   | xC ⇒ 〈x8,x4〉   | xD ⇒ 〈x8,xF〉   | xE ⇒ 〈x9,xA〉   | xF ⇒ 〈xA,x5〉 ]
270  | xC ⇒ match e2 with
271   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xC〉   | x2 ⇒ 〈x1,x8〉   | x3 ⇒ 〈x2,x4〉
272   | x4 ⇒ 〈x3,x0〉   | x5 ⇒ 〈x3,xC〉   | x6 ⇒ 〈x4,x8〉   | x7 ⇒ 〈x5,x4〉
273   | x8 ⇒ 〈x6,x0〉   | x9 ⇒ 〈x6,xC〉   | xA ⇒ 〈x7,x8〉   | xB ⇒ 〈x8,x4〉
274   | xC ⇒ 〈x9,x0〉   | xD ⇒ 〈x9,xC〉   | xE ⇒ 〈xA,x8〉   | xF ⇒ 〈xB,x4〉 ]
275  | xD ⇒ match e2 with
276   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xD〉   | x2 ⇒ 〈x1,xA〉   | x3 ⇒ 〈x2,x7〉
277   | x4 ⇒ 〈x3,x4〉   | x5 ⇒ 〈x4,x1〉   | x6 ⇒ 〈x4,xE〉   | x7 ⇒ 〈x5,xB〉
278   | x8 ⇒ 〈x6,x8〉   | x9 ⇒ 〈x7,x5〉   | xA ⇒ 〈x8,x2〉   | xB ⇒ 〈x8,xF〉
279   | xC ⇒ 〈x9,xC〉   | xD ⇒ 〈xA,x9〉   | xE ⇒ 〈xB,x6〉   | xF ⇒ 〈xC,x3〉 ]
280  | xE ⇒ match e2 with
281   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xE〉   | x2 ⇒ 〈x1,xC〉   | x3 ⇒ 〈x2,xA〉
282   | x4 ⇒ 〈x3,x8〉   | x5 ⇒ 〈x4,x6〉   | x6 ⇒ 〈x5,x4〉   | x7 ⇒ 〈x6,x2〉
283   | x8 ⇒ 〈x7,x0〉   | x9 ⇒ 〈x7,xE〉   | xA ⇒ 〈x8,xC〉   | xB ⇒ 〈x9,xA〉
284   | xC ⇒ 〈xA,x8〉   | xD ⇒ 〈xB,x6〉   | xE ⇒ 〈xC,x4〉   | xF ⇒ 〈xD,x2〉 ]
285  | xF ⇒ match e2 with
286   [ x0 ⇒ 〈x0,x0〉   | x1 ⇒ 〈x0,xF〉   | x2 ⇒ 〈x1,xE〉   | x3 ⇒ 〈x2,xD〉
287   | x4 ⇒ 〈x3,xC〉   | x5 ⇒ 〈x4,xB〉   | x6 ⇒ 〈x5,xA〉   | x7 ⇒ 〈x6,x9〉
288   | x8 ⇒ 〈x7,x8〉   | x9 ⇒ 〈x8,x7〉   | xA ⇒ 〈x9,x6〉   | xB ⇒ 〈xA,x5〉
289   | xC ⇒ 〈xB,x4〉   | xD ⇒ 〈xC,x3〉   | xE ⇒ 〈xD,x2〉   | xF ⇒ 〈xE,x1〉 ]
290  ].
291
292 (* correzione per somma su BCD *)
293 (* input: halfcarry,carry,X(BCD+BCD) *)
294 (* output: X',carry' *)
295 ndefinition daa_b8 ≝
296 λh,c:bool.λX:byte8.
297  match lt_b8 X 〈x9,xA〉 with
298   (* [X:0x00-0x99] *)
299   (* c' = c *)
300   (* X' = [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + [c=1 ? 0x60 : 0x00]
301           [(b16l X):0xA-0xF] X + 0x06 + [c=1 ? 0x60 : 0x00] *)
302   [ true ⇒
303    let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
304     [ true ⇒ X
305     | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
306    let X'' ≝ match c with
307     [ true ⇒ plus_b8_d_d X' 〈x6,x0〉
308     | false ⇒ X' ] in
309    pair ?? X'' c
310   (* [X:0x9A-0xFF] *)
311   (* c' = 1 *)
312   (* X' = [X:0x9A-0xFF]
313           [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + 0x60
314           [(b16l X):0xA-0xF] X + 0x6 + 0x60 *) 
315   | false ⇒
316    let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
317     [ true ⇒ X
318     | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
319    let X'' ≝ plus_b8_d_d X' 〈x6,x0〉 in
320    pair ?? X'' true
321   ].
322
323 (* iteratore sui byte *)
324 ndefinition forall_byte8 ≝
325  λP.
326   forall_exadecim (λbh.
327   forall_exadecim (λbl.
328    P (mk_byte8 bh bl))).