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;