Replace some single-letter names with more descriptive names. (#11)

In several instances the terminology used is chosen to match the
Keccak specification. E.g. 'F' for the permutation function,
'L' for the lane size logarithm, 'W' for the lane size in bits,
and 'B' for the Keccak state size in bits. However, these names
are not particularly descriptive when reading the source code
unless the reader is familiar with the Keccak specification.

This commit renames these instances to use more descriptive names,
e.g. 'Permute' instead of 'F', as well as clarifying a few other names.

src/common/keccak-generic_duplex.adb

@@ -38,7 +38,7 @@ is
    begin
       Init_State (Ctx.State);
 
-      Ctx.Rate := State_Size - Capacity;
+      Ctx.Rate := State_Size_Bits - Capacity;
    end Init;
 
    --------------
@@ -53,7 +53,7 @@ is
    is
       use type Keccak.Types.Byte;
 
-      Block     : Keccak.Types.Byte_Array (0 .. (State_Size + 7) / 8 - 1) := (others => 0);
+      Block     : Keccak.Types.Byte_Array (0 .. (State_Size_Bits + 7) / 8 - 1) := (others => 0);
 
       Num_Bytes : constant Natural := (In_Data_Bit_Length + 7) / 8;
 
@@ -71,7 +71,7 @@ is
                            Block (0 .. ((Ctx.Rate + 7) / 8) - 1),
                            Rate_Of (Ctx));
 
-      F (Ctx.State);
+      Permute (Ctx.State);
 
       Extract_Bits (Ctx.State, Out_Data, Out_Data_Bit_Length);
    end Duplex;
@@ -86,7 +86,7 @@ is
    is
       use type Keccak.Types.Byte;
 
-      Block   : Keccak.Types.Byte_Array (0 .. (State_Size + 7) / 8 - 1) := (others => 0);
+      Block   : Keccak.Types.Byte_Array (0 .. (State_Size_Bits + 7) / 8 - 1) := (others => 0);
 
    begin
       Pad (Block (0 .. ((Rate_Of (Ctx) + 7) / 8) - 1),
@@ -97,7 +97,7 @@ is
                            Block (0 .. ((Ctx.Rate + 7) / 8) - 1),
                            Rate_Of (Ctx));
 
-      F (Ctx.State);
+      Permute (Ctx.State);
 
       Extract_Bits (Ctx.State, Out_Data, Out_Data_Bit_Length);
    end Duplex_Blank;
@@ -110,7 +110,7 @@ is
                           In_Data            : in     Keccak.Types.Byte_Array;
                           In_Data_Bit_Length : in     Natural)
    is
-      Block    : Keccak.Types.Byte_Array (0 .. (State_Size + 7) / 8 - 1) := (others => 0);
+      Block    : Keccak.Types.Byte_Array (0 .. (State_Size_Bits + 7) / 8 - 1) := (others => 0);
 
       Nb_Bytes : constant Natural := (In_Data_Bit_Length + 7) / 8;
 
@@ -127,7 +127,7 @@ is
                            Block (0 .. ((Ctx.Rate + 7) / 8) - 1),
                            Rate_Of (Ctx));
 
-      F (Ctx.State);
+      Permute (Ctx.State);
    end Duplex_Mute;
 
 end Keccak.Generic_Duplex;

src/common/keccak-generic_duplex.ads

@@ -29,7 +29,7 @@ with Keccak.Types;
 
 generic
    --  Size of the Duplex state in bits (e.g. 1600 for Keccak[1600])
-   State_Size : Positive;
+   State_Size_Bits : Positive;
 
    --  Type for the Duplex state (e.g. this could be a Keccak[1600] state).
    type State_Type is private;
@@ -38,7 +38,7 @@ generic
    with procedure Init_State (A : out State_Type);
 
    --  Procedure to permute the state.
-   with procedure F (A : in out State_Type);
+   with procedure Permute (A : in out State_Type);
 
    --  Procedure to XOR bits into the generic state.
    with procedure XOR_Bits_Into_State (A       : in out State_Type;
@@ -68,19 +68,19 @@ generic
    --  specification "Cryptographic Sponge Functions" from authors of Keccak.
 package Keccak.Generic_Duplex
 is
-   subtype Rate_Number is Positive range 1 + Min_Padding_Bits .. State_Size - 1;
+   subtype Rate_Number is Positive range 1 + Min_Padding_Bits .. State_Size_Bits - 1;
 
    type Context is private;
 
    procedure Init (Ctx      :    out Context;
                    Capacity : in     Positive)
      with Global => null,
      Depends => (Ctx => Capacity),
-     Pre => (Capacity < (State_Size - Min_Padding_Bits)),
-     Post => Rate_Of (Ctx) = State_Size - Capacity;
+     Pre => (Capacity < (State_Size_Bits - Min_Padding_Bits)),
+     Post => Rate_Of (Ctx) = State_Size_Bits - Capacity;
    --  Initialize the context.
    --
-   --  After initialization, the rate is equal to the State_Size - Capacity.
+   --  After initialization, the rate is equal to the State_Size_Bits - Capacity.
    --  For example, if the state size is 1600 bits and the capacity is 512 bits
    --  then the rate is 1088 bits.
    --
@@ -96,7 +96,7 @@ is
      with Global => null;
    --  Get the rate of the context.
    --
-   --  @return The rate (in bits). This is always less than the State_Size
+   --  @return The rate (in bits). This is always less than the State_Size_Bits
 
    function Max_Input_Length (Ctx : in Context) return Positive
      with Global => null;

src/common/keccak-generic_keccakf-bit_lanes.adb

@@ -24,7 +24,7 @@
 --  (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
 --  THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 -------------------------------------------------------------------------------
-with Interfaces;
+with Interfaces; use Interfaces;
 
 package body Keccak.Generic_KeccakF.Bit_Lanes
 is
@@ -37,8 +37,6 @@ is
                                   Data    : in     Keccak.Types.Byte_Array;
                                   Bit_Len : in     Natural)
    is
-      use type Keccak.Types.Byte;
-
       X                : X_Coord := 0;
       Y                : Y_Coord := 0;
 
@@ -58,8 +56,9 @@ is
             Lane : Lane_Type;
 
          begin
-            for I in Natural range 0 .. (8 / W) - 1 loop
-               Lane := Lane_Type (Interfaces.Shift_Right (Byte, I * W) and (2**W - 1));
+            for I in Natural range 0 .. (8 / Lane_Size_Bits) - 1 loop
+               Lane := Lane_Type (Shift_Right (Byte,
+                                               I * Lane_Size_Bits) and (2**Lane_Size_Bits - 1));
 
                A (X, Y) := A (X, Y) xor Lane;
 
@@ -81,8 +80,9 @@ is
          begin
             Byte := Data (Data'First + Offset) and (2**Remaining_Bits - 1);
 
-            for I in Natural range 0 .. (8 / W) - 1 loop
-               Lane := Lane_Type (Interfaces.Shift_Right (Byte, I * W) and (2**W - 1));
+            for I in Natural range 0 .. (8 / Lane_Size_Bits) - 1 loop
+               Lane := Lane_Type (Shift_Right (Byte,
+                                               I * Lane_Size_Bits) and (2**Lane_Size_Bits - 1));
 
                A (X, Y) := A (X, Y) xor Lane;
 
@@ -119,8 +119,6 @@ is
    procedure Extract_Bytes (A    : in     State;
                             Data :    out Keccak.Types.Byte_Array)
    is
-      use type Keccak.Types.Byte;
-
       X               : X_Coord := 0;
       Y               : Y_Coord := 0;
 
@@ -132,15 +130,16 @@ is
       Data := (others => 0); --  workaround for flow analysis.
 
       --  Process entire bytes
-      while Remaining_Bytes > 0 and Offset < B / 8 loop
+      while Remaining_Bytes > 0 and Offset < State_Size_Bits / 8 loop
          pragma Loop_Variant (Increases => Offset,
                               Decreases => Remaining_Bytes);
          pragma Loop_Invariant (Offset + Remaining_Bytes = Data'Length);
 
          Byte := 0;
 
-         for I in Natural range 0 .. (8 / W) - 1 loop
-            Byte := Byte or Interfaces.Shift_Left (Keccak.Types.Byte (A (X, Y)), I * W);
+         for I in Natural range 0 .. (8 / Lane_Size_Bits) - 1 loop
+            Byte := Byte or Shift_Left (Keccak.Types.Byte (A (X, Y)),
+                                        I * Lane_Size_Bits);
 
             X := X + 1;
             if X = 0 then
@@ -159,8 +158,9 @@ is
 
          Byte := 0;
 
-         for I in Natural range 0 .. (8 / W) - 1 loop
-            Byte := Byte or Interfaces.Shift_Left (Keccak.Types.Byte (A (X, Y)), I * W);
+         for I in Natural range 0 .. (8 / Lane_Size_Bits) - 1 loop
+            Byte := Byte or Shift_Left (Keccak.Types.Byte (A (X, Y)),
+                                        I * Lane_Size_Bits);
 
             X := X + 1;
             if X = 0 then
@@ -182,8 +182,6 @@ is
    procedure Extract_Bytes (A    : in     Lane_Complemented_State;
                             Data :    out Keccak.Types.Byte_Array)
    is
-      use type Keccak.Types.Byte;
-
       Complement_Mask : constant Lane_Complemented_State :=
         (0 => (4         => Lane_Type'Last,
                others    => 0),
@@ -207,16 +205,16 @@ is
       Data := (others => 0); --  workaround for flow analysis.
 
       --  Process entire bytes
-      while Remaining_Bytes > 0 and Offset < B / 8 loop
+      while Remaining_Bytes > 0 and Offset < State_Size_Bits / 8 loop
          pragma Loop_Variant (Increases => Offset,
                               Decreases => Remaining_Bytes);
          pragma Loop_Invariant (Offset + Remaining_Bytes = Data'Length);
 
          Byte := 0;
 
-         for I in Natural range 0 .. (8 / W) - 1 loop
+         for I in Natural range 0 .. (8 / Lane_Size_Bits) - 1 loop
             Lane := A (X, Y) xor Complement_Mask (X, Y);
-            Byte := Byte or Interfaces.Shift_Left (Keccak.Types.Byte (Lane), I * W);
+            Byte := Byte or Shift_Left (Keccak.Types.Byte (Lane), I * Lane_Size_Bits);
 
             X := X + 1;
             if X = 0 then
@@ -235,9 +233,9 @@ is
 
          Byte := 0;
 
-         for I in Natural range 0 .. (8 / W) - 1 loop
+         for I in Natural range 0 .. (8 / Lane_Size_Bits) - 1 loop
             Lane := A (X, Y) xor Complement_Mask (X, Y);
-            Byte := Byte or Interfaces.Shift_Left (Keccak.Types.Byte (Lane), I * W);
+            Byte := Byte or Shift_Left (Keccak.Types.Byte (Lane), I * Lane_Size_Bits);
 
             X := X + 1;
             if X = 0 then
@@ -260,8 +258,6 @@ is
                            Data    :    out Keccak.Types.Byte_Array;
                            Bit_Len : in     Natural)
    is
-      use type Keccak.Types.Byte;
-
    begin
       Extract_Bytes (A, Data);
 
@@ -280,8 +276,6 @@ is
                            Data    :    out Keccak.Types.Byte_Array;
                            Bit_Len : in     Natural)
    is
-      use type Keccak.Types.Byte;
-
    begin
       Extract_Bytes (A, Data);
 

src/common/keccak-generic_keccakf-bit_lanes.ads

@@ -34,7 +34,7 @@ package Keccak.Generic_KeccakF.Bit_Lanes
 is
 
    pragma Assert
-     (W in 1 | 2 | 4,
+     (Lane_Size_Bits in 1 | 2 | 4,
       "Bit_Lanes can only be used with lane sizes that 1, 2, or 4 bits wide");
 
    procedure XOR_Bits_Into_State (A       : in out State;
@@ -44,7 +44,7 @@ is
      Depends => (A =>+ (Data, Bit_Len)),
      Pre => (Data'Length <= Natural'Last / 8
              and then Bit_Len <= Data'Length * 8
-             and then Bit_Len <= B);
+             and then Bit_Len <= State_Size_Bits);
 
    procedure XOR_Bits_Into_State (A       : in out Lane_Complemented_State;
                                   Data    : in     Keccak.Types.Byte_Array;
@@ -54,34 +54,34 @@ is
      Depends => (A =>+ (Data, Bit_Len)),
      Pre => (Data'Length <= Natural'Last / 8
              and then Bit_Len <= Data'Length * 8
-             and then Bit_Len <= B);
+             and then Bit_Len <= State_Size_Bits);
 
    procedure Extract_Bytes (A    : in     State;
                             Data :    out Keccak.Types.Byte_Array)
      with Global => null,
      Depends => (Data =>+ A),
-     Pre => Data'Length <= ((B + 7) / 8);
+     Pre => Data'Length <= ((State_Size_Bits + 7) / 8);
 
    procedure Extract_Bytes (A    : in     Lane_Complemented_State;
                             Data :    out Keccak.Types.Byte_Array)
      with Global => null,
      Depends => (Data =>+ A),
-     Pre => Data'Length <= ((B + 7) / 8);
+     Pre => Data'Length <= ((State_Size_Bits + 7) / 8);
 
    procedure Extract_Bits (A       : in     State;
                            Data    :    out Keccak.Types.Byte_Array;
                            Bit_Len : in     Natural)
      with Global => null,
      Depends => (Data =>+ (A, Bit_Len)),
-     Pre => (Bit_Len <= B
+     Pre => (Bit_Len <= State_Size_Bits
              and then Data'Length = (Bit_Len + 7) / 8);
 
    procedure Extract_Bits (A       : in     Lane_Complemented_State;
                            Data    :    out Keccak.Types.Byte_Array;
                            Bit_Len : in     Natural)
      with Global => null,
      Depends => (Data =>+ (A, Bit_Len)),
-     Pre => (Bit_Len <= B
+     Pre => (Bit_Len <= State_Size_Bits
              and then Data'Length = (Bit_Len + 7) / 8);
 
 end Keccak.Generic_KeccakF.Bit_Lanes;