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