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