File : ffa.ads
1 ------------------------------------------------------------------------------
2 ------------------------------------------------------------------------------
3 -- This file is part of 'Finite Field Arithmetic', aka 'FFA'. --
4 -- --
5 -- (C) 2018 Stanislav Datskovskiy ( www.loper-os.org ) --
6 -- http://wot.deedbot.org/17215D118B7239507FAFED98B98228A001ABFFC7.html --
7 -- --
8 -- You do not have, nor can you ever acquire the right to use, copy or --
9 -- distribute this software ; Should you use this software for any purpose, --
10 -- or copy and distribute it to anyone or in any manner, you are breaking --
11 -- the laws of whatever soi-disant jurisdiction, and you promise to --
12 -- continue doing so for the indefinite future. In any case, please --
13 -- always : read and understand any software ; verify any PGP signatures --
14 -- that you use - for any purpose. --
15 -- --
16 -- See also http://trilema.com/2015/a-new-software-licensing-paradigm . --
17 ------------------------------------------------------------------------------
18 ------------------------------------------------------------------------------
19
20 with Words; use Words;
21 with FZ_Type; use FZ_Type;
22
23 with W_Pred;
24
25 with FZ_Lim;
26 with FZ_Basic;
27 with FZ_IO;
28 with FZ_Cmp;
29 with FZ_Pred;
30 with FZ_BitOp;
31 with FZ_Divis;
32 with FZ_ModEx;
33 with FZ_Measr;
34 with FZ_QShft;
35
36
37 -- FFA Exports
38 package FFA is
39
40 pragma Pure;
41
42 ----------------------------------------------------------------------------
43 --- Current 'deg. Kelvin' Version of FFA
44 ----------------------------------------------------------------------------
45
46 FFA_K_Version : constant Natural := 255;
47
48 ----------------------------------------------------------------------------
49 --- Fundamental Types and Sizes
50 ----------------------------------------------------------------------------
51
52 subtype Word is Words.Word;
53 subtype WBool is Words.WBool;
54
55 subtype Nibble is Words.Nibble;
56
57 subtype FZ is FZ_Type.FZ;
58 subtype Indices is FZ_Type.Indices;
59 subtype FZBit_Index is FZ_Type.FZBit_Index;
60
61 subtype Char_Count is FZ_IO.Char_Count;
62
63 Bitness : Positive renames Words.Bitness;
64
65 ----------------------------------------------------------------------------
66 --- Word Predicates
67 ----------------------------------------------------------------------------
68
69 -- Return 1 if N is equal to 0; otherwise return 0.
70 function FFA_Word_ZeroP(N : in Word) return WBool
71 renames W_Pred.W_ZeroP;
72
73 -- Return 1 if N is unequal to 0; otherwise return 0.
74 function FFA_Word_NZeroP(N : in Word) return WBool
75 renames W_Pred.W_NZeroP;
76
77 -- Return WBool-complement of N.
78 function FFA_Word_Not(N : in WBool) return WBool
79 renames W_Pred.W_Not;
80
81 -- Return 1 if N is odd; otherwise return 0.
82 function FFA_Word_OddP(N : in Word) return WBool
83 renames W_Pred.W_OddP;
84
85 -- Return 1 if A is equal to B ; otherwise return 0.
86 function FFA_Word_EqP(A : in Word; B : in Word) return WBool
87 renames W_Pred.W_EqP;
88
89 ----------------------------------------------------------------------------
90 --- FZ Limits
91 ----------------------------------------------------------------------------
92
93 FFA_Validity_Rule_Doc : String renames FZ_Lim.FZ_Validity_Rule_Doc;
94
95 -- Determine if a proposed FFA Bitness is valid.
96 function FFA_FZ_Valid_Bitness_P(B : in Positive) return Boolean
97 renames FZ_Lim.FZ_Valid_Bitness_P;
98
99 ----------------------------------------------------------------------------
100 --- FZ Basics
101 ----------------------------------------------------------------------------
102
103 -- Determine the Bitness of N
104 function FFA_FZ_Bitness(N : in FZ) return Bit_Count
105 renames FZ_Basic.FZ_Bitness;
106
107 -- N := 0
108 procedure FFA_FZ_Clear(N : out FZ)
109 renames FZ_Basic.FZ_Clear;
110
111 -- Set given FZ to a given truth value
112 procedure FFA_WBool_To_FZ(V : in WBool; N : out FZ)
113 renames FZ_Basic.WBool_To_FZ;
114
115 -- First Word of N := Source
116 procedure FFA_FZ_Set_Head(N : out FZ; Source : in Word)
117 renames FZ_Basic.FZ_Set_Head;
118
119 -- First Word of N
120 function FFA_FZ_Get_Head(N : in FZ) return Word
121 renames FZ_Basic.FZ_Get_Head;
122
123 -- Exchange X and Y
124 procedure FFA_FZ_Swap(X : in out FZ; Y : in out FZ)
125 with Pre => X'Length = Y'Length;
126
127 -- Constant-time MUX: Sel = 0: Result := X; Sel = 1: Result := Y
128 procedure FFA_FZ_Mux(X : in FZ; Y : in FZ; Result : out FZ; Sel : in WBool)
129 with Pre => X'Length = Y'Length and X'Length = Result'Length;
130
131 ----------------------------------------------------------------------------
132 --- FZ IO Operations
133 ----------------------------------------------------------------------------
134
135 -- Expand FZ N by nibble D, and determine whether this operation overflowed
136 procedure FFA_FZ_Insert_Bottom_Nibble(N : in out FZ;
137 D : in Nibble;
138 Overflow : out WBool)
139 renames FZ_IO.FZ_Insert_Bottom_Nibble;
140
141 -- Determine the number of ASCII characters required to represent N
142 function FFA_FZ_ASCII_Length(N : in FZ) return Char_Count
143 renames FZ_IO.FZ_ASCII_Length;
144
145 -- Write an ASCII hex representation of N into existing string buffer S
146 procedure FFA_FZ_To_Hex_String(N : in FZ; S : out String)
147 renames FZ_IO.FZ_To_Hex_String;
148
149 ----------------------------------------------------------------------------
150 --- Comparison Predicate Operations on FZ
151 ----------------------------------------------------------------------------
152
153 -- 1 iff X == Y (branch-free); else 0
154 function FFA_FZ_EqP(X : in FZ; Y: in FZ) return WBool
155 renames FZ_Cmp.FZ_EqP;
156
157 -- 1 iff X < Y (branch-free); else 0
158 function FFA_FZ_LessThanP(X : in FZ; Y : in FZ) return WBool
159 renames FZ_Cmp.FZ_LessThanP;
160
161 -- 1 iff X > Y (branch-free); else 0
162 function FFA_FZ_GreaterThanP(X : in FZ; Y : in FZ) return WBool
163 renames FZ_Cmp.FZ_GreaterThanP;
164
165 ----------------------------------------------------------------------------
166 --- Fundamental Predicate Operations on FZ
167 ----------------------------------------------------------------------------
168
169 -- 1 iff N == 0 (branch-free); else 0
170 function FFA_FZ_ZeroP(N : in FZ) return WBool
171 renames FZ_Pred.FZ_ZeroP;
172
173 -- 1 iff N != 0 (branch-free); else 0
174 function FFA_FZ_NZeroP(N : in FZ) return WBool
175 renames FZ_Pred.FZ_NZeroP;
176
177 -- 1 iff N is odd
178 function FFA_FZ_OddP(N : in FZ) return WBool
179 renames FZ_Pred.FZ_OddP;
180
181 ----------------------------------------------------------------------------
182 --- Bitwise Operations on FZ
183 ----------------------------------------------------------------------------
184
185 -- Result := X & Y
186 procedure FFA_FZ_And(X : in FZ; Y : in FZ; Result : out FZ)
187 with Pre => X'Length = Y'Length and X'Length = Result'Length;
188
189 -- N := N & W, W is a Word
190 procedure FFA_FZ_And_W(N : in out FZ; W : in Word)
191 renames FZ_BitOp.FZ_And_W;
192
193 -- Result := X | Y
194 procedure FFA_FZ_Or(X : in FZ; Y : in FZ; Result : out FZ)
195 with Pre => X'Length = Y'Length and X'Length = Result'Length;
196
197 -- N := N | W, W is a Word
198 procedure FFA_FZ_Or_W(N : in out FZ; W : in Word)
199 renames FZ_BitOp.FZ_Or_W;
200
201 -- Result := X ^ Y
202 procedure FFA_FZ_Xor(X : in FZ; Y : in FZ; Result : out FZ)
203 with Pre => X'Length = Y'Length and X'Length = Result'Length;
204
205 -- N := N ^ W, W is a Word
206 procedure FFA_FZ_Xor_W(N : in out FZ; W : in Word)
207 renames FZ_BitOp.FZ_Xor_W;
208
209 -- NotN := ~N ('ones complement')
210 procedure FFA_FZ_Not(N : in FZ; NotN : out FZ)
211 with Pre => N'Length = NotN'Length;
212
213 ----------------------------------------------------------------------------
214 --- Basic Arithmetic on FZ
215 ----------------------------------------------------------------------------
216
217 -- Sum := X + Y; Overflow := Carry
218 procedure FFA_FZ_Add(X : in FZ;
219 Y : in FZ;
220 Sum : out FZ;
221 Overflow : out WBool)
222 with Pre => X'Length = Y'Length and X'Length = Sum'Length;
223
224 -- Difference := X - Y; Underflow := Borrow
225 procedure FFA_FZ_Subtract(X : in FZ;
226 Y : in FZ;
227 Difference : out FZ;
228 Underflow : out WBool)
229 with Pre => X'Length = Y'Length and X'Length = Difference'Length;
230
231 ----------------------------------------------------------------------------
232 --- Division on FZ
233 ----------------------------------------------------------------------------
234
235 -- Dividend is divided by Divisor, producing Quotient and Remainder.
236 -- WARNING: NO div0 test here! Caller must test.
237 procedure FFA_FZ_IDiv(Dividend : in FZ;
238 Divisor : in FZ;
239 Quotient : out FZ;
240 Remainder : out FZ)
241 renames FZ_Divis.FZ_IDiv;
242
243 -- Exactly same thing as IDiv, but keep only the Quotient
244 procedure FFA_FZ_Div(Dividend : in FZ;
245 Divisor : in FZ;
246 Quotient : out FZ)
247 renames FZ_Divis.FZ_Div;
248
249 -- Modulus.
250 procedure FFA_FZ_Mod(Dividend : in FZ;
251 Divisor : in FZ;
252 Remainder : out FZ)
253 renames FZ_Divis.FZ_Mod;
254
255 ----------------------------------------------------------------------------
256 --- Multiplication on FZ
257 ----------------------------------------------------------------------------
258
259 -- Multiplier. Preserves the inputs.
260 procedure FFA_FZ_Multiply(X : in FZ;
261 Y : in FZ;
262 XY_Lo : out FZ;
263 XY_Hi : out FZ)
264 with Pre => X'Length = Y'Length and
265 XY_Lo'Length = XY_Hi'Length and
266 XY_Lo'Length = ((X'Length + Y'Length) / 2);
267
268 -- Square. Preserves the inputs.
269 procedure FFA_FZ_Square(X : in FZ;
270 XX_Lo : out FZ;
271 XX_Hi : out FZ)
272 with Pre => XX_Lo'Length = X'Length and
273 XX_Hi'Length = X'Length and
274 X'Length mod 2 = 0;
275
276 ----------------------------------------------------------------------------
277 --- Modular Operations on FZ
278 ----------------------------------------------------------------------------
279
280 -- Modular Multiply: Product := X*Y mod Modulus
281 procedure FFA_FZ_Modular_Multiply(X : in FZ;
282 Y : in FZ;
283 Modulus : in FZ;
284 Product : out FZ)
285 renames FZ_ModEx.FZ_Mod_Mul;
286
287 -- Modular Exponent: Result := Base^Exponent mod Modulus
288 procedure FFA_FZ_Modular_Exponentiate(Base : in FZ;
289 Exponent : in FZ;
290 Modulus : in FZ;
291 Result : out FZ)
292 renames FZ_ModEx.FZ_Mod_Exp;
293
294 ----------------------------------------------------------------------------
295 --- Other Operations on FZ
296 ----------------------------------------------------------------------------
297
298 -- Find the index of eldest nonzero bit ( 0 if none, or 1 .. FZBitness )
299 function FFA_FZ_Measure(N : in FZ) return FZBit_Index
300 renames FZ_Measr.FZ_Measure;
301
302 -- Constant-time arbitrary right-shift.
303 procedure FFA_FZ_Quiet_ShiftRight(N : in FZ;
304 ShiftedN : in out FZ;
305 Count : in FZBit_Index)
306 renames FZ_QShft.FZ_Quiet_ShiftRight;
307
308 -- Constant-time arbitrary left-shift.
309 procedure FFA_FZ_Quiet_ShiftLeft(N : in FZ;
310 ShiftedN : in out FZ;
311 Count : in FZBit_Index)
312 renames FZ_QShft.FZ_Quiet_ShiftLeft;
313
314 end FFA;