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