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    ----------------------------------------------------------------------------
 260    --- Modular Operations on FZ
 261    ----------------------------------------------------------------------------
 262    
 263    -- Modular Multiply: Product := X*Y mod Modulus
 264    procedure FFA_FZ_Modular_Multiply(X        : in  FZ;
 265                                      Y        : in  FZ;
 266                                      Modulus  : in  FZ;
 267                                      Product  : out FZ)
 268      renames FZ_ModEx.FZ_Mod_Mul;
 269    
 270    -- Modular Exponent: Result := Base^Exponent mod Modulus
 271    procedure FFA_FZ_Modular_Exponentiate(Base     : in  FZ;
 272                                          Exponent : in  FZ;
 273                                          Modulus  : in  FZ;
 274                                          Result   : out FZ)
 275      renames FZ_ModEx.FZ_Mod_Exp;
 276    
 277 end FFA;