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