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_ch12_karatsub...  259    -- Square. Preserves the inputs.
ffa_ch12_karatsub...  260    procedure FFA_FZ_Square(X     : in  FZ;
ffa_ch12_karatsub...  261                            XX_Lo : out FZ;
ffa_ch12_karatsub...  262                            XX_Hi : out FZ)
ffa_ch12_karatsub...  263      with Pre => XX_Lo'Length = X'Length and
ffa_ch12_karatsub...  264      XX_Hi'Length = X'Length and
ffa_ch12_karatsub...  265      X'Length mod 2 = 0;
ffa_ch12_karatsub...  266    
ffa_ch11_tuning_a...  267    ----------------------------------------------------------------------------
ffa_ch11_tuning_a...  268    --- Modular Operations on FZ
ffa_ch11_tuning_a...  269    ----------------------------------------------------------------------------
ffa_ch11_tuning_a...  270    
ffa_ch11_tuning_a...  271    -- Modular Multiply: Product := X*Y mod Modulus
ffa_ch11_tuning_a...  272    procedure FFA_FZ_Modular_Multiply(X        : in  FZ;
ffa_ch11_tuning_a...  273                                      Y        : in  FZ;
ffa_ch11_tuning_a...  274                                      Modulus  : in  FZ;
ffa_ch11_tuning_a...  275                                      Product  : out FZ)
ffa_ch11_tuning_a...  276      renames FZ_ModEx.FZ_Mod_Mul;
ffa_ch11_tuning_a...  277    
ffa_ch11_tuning_a...  278    -- Modular Exponent: Result := Base^Exponent mod Modulus
ffa_ch11_tuning_a...  279    procedure FFA_FZ_Modular_Exponentiate(Base     : in  FZ;
ffa_ch11_tuning_a...  280                                          Exponent : in  FZ;
ffa_ch11_tuning_a...  281                                          Modulus  : in  FZ;
ffa_ch11_tuning_a...  282                                          Result   : out FZ)
ffa_ch11_tuning_a...  283      renames FZ_ModEx.FZ_Mod_Exp;
ffa_ch11_tuning_a...  284    
ffa_ch11_tuning_a...  285 end FFA;