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