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