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