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