move X and T0 to function parameters

examples/generate_2fa_token.adb

@@ -15,7 +15,6 @@ is
        Import,
        Convention => C,
        External_Name => "time";
-   package TOTP is new OTP.T;
 begin
    pragma Assert (LSC.Byte_Arrays.Natural_Index'Last / 5 > 32);
    pragma Warnings (Off, "no Global contract");
@@ -26,7 +25,7 @@ begin
      (for all C of Ada.Command_Line.Argument (1) =>
           Base32.Valid_Base32_Character (C)))
    then
-      Ada.Text_IO.Put_Line (OTP.Image (TOTP.TOTP (
+      Ada.Text_IO.Put_Line (OTP.Image (OTP.T.TOTP (
                             Base32.Decode (Ada.Command_Line.Argument (1)),
                             Time (System.Null_Address)), 6));
    else

src/base32.adb

@@ -123,12 +123,12 @@ is
    is
       N : Byte;
    begin
-      case Character'Pos (C) is
-         when 97 .. 122 =>
+      case C is
+         when 'a' .. 'z' =>
             N := Byte (Character'Pos (C) - 97);
-         when 65 .. 90 =>
+         when 'A' .. 'Z' =>
             N := Byte (Character'Pos (C) - 65);
-         when 50 .. 55 =>
+         when '2' .. '7' =>
             N := Byte (Character'Pos (C) - 24);
          when others =>
             raise Constraint_Error;

src/otp-h.ads

@@ -24,6 +24,8 @@ is
        Depends => (HOTP'Result => (Key, Counter)),
        Pre => Key'Length <= 64;
 
+private
+
    --  @private Only used to generate the token
    function Extract
      (Mac : HMAC.HMAC_Type)

src/otp-t.adb

@@ -1,17 +1,18 @@
-with Interfaces;
 with OTP.H;
-use all type Interfaces.Unsigned_64;
 
 package body OTP.T
+with SPARK_Mode
 is
 
    ----------
    -- TOTP --
    ----------
 
    function TOTP
-     (Key : LSC.Byte_Arrays.Byte_Array_Type;
-      Time : LSC.Types.Word64)
+     (Key  : LSC.Byte_Arrays.Byte_Array_Type;
+      Time : LSC.Types.Word64;
+      X    : LSC.Types.Word64 := 30;
+      T0   : LSC.Types.Word64 := 0)
       return OTP_Token
    is
    begin

src/otp-t.ads

@@ -1,30 +1,31 @@
 with LSC.Types;
 with LSC.Byte_Arrays;
+use all type LSC.Types.Word64;
 
 --  @summary
 --  Time based One-Time-Pad
 --
 --  @description
 --  Calculates the Time based One-Time-Pad based on RFC 6238
---
---  @param X Time step size
---  @param T0 Reference time
-generic
-   X : LSC.Types.Word64 := 30;
-   T0 : LSC.Types.Word64 := 0;
+
 package OTP.T
+with SPARK_Mode
 is
 
    --  Calculates the TOTP Token from a given key and time offset
    --  @param HMAC key
    --  @param Current time
+   --  @param X Time step size
+   --  @param T0 Reference time
    --  @return TOTP Token as 31bit word
    function TOTP
      (Key  : LSC.Byte_Arrays.Byte_Array_Type;
-      Time : LSC.Types.Word64)
+      Time : LSC.Types.Word64;
+      X    : LSC.Types.Word64 := 30;
+      T0   : LSC.Types.Word64 := 0)
       return OTP_Token
      with
-       Depends => (TOTP'Result => (Key, Time)),
-       Pre => Key'Length <= 64;
+       Depends => (TOTP'Result => (Key, Time, X, T0)),
+       Pre => Key'Length <= 64 and X > 0;
 
 end OTP.T;

src/otp.adb

@@ -15,9 +15,7 @@ is
       Value : OTP_Value (1 .. D) := (others => '0');
    begin
       for I in reverse Value'Range loop
-         pragma Loop_Invariant (for all C of Value =>
-                                  Character'Pos (C) > 47 and
-                                  Character'Pos (C) < 58);
+         pragma Loop_Invariant (for all C of Value => C in '0' .. '9');
          Value (I) := Character'Val ((Token mod 10) + 48);
          Token := Token / 10;
       end loop;

src/otp.ads

@@ -9,8 +9,7 @@ is
    subtype OTP_Value is String
      with
        Dynamic_Predicate =>
-         (for all C of OTP_Value =>
-            Character'Pos (C) > 47 and Character'Pos (C) < 58);
+         (for all C of OTP_Value => C in '0' .. '9');
 
    --  31 bit OTP token
    subtype OTP_Token is Integer range 0 .. 2 ** 31 - 1;

tests/totp_test.adb → tests/otp-t-test.adb

@@ -3,7 +3,7 @@ with OTP.T;
 with LSC.Types;
 with LSC.Byte_Arrays;
 
-package body TOTP_Test
+package body OTP.T.Test
 with SPARK_Mode
 is
 
@@ -20,12 +20,11 @@ is
          16#37#, 16#38#, 16#39#, 16#30#);
       Time : constant LSC.Types.Word64 := 59;
       Totp_Value : constant  OTP.OTP_Value := "94287082";
-      package TOTP is new OTP.T;
    begin
-      if OTP.Image (TOTP.TOTP (Key, Time), 8) /= Totp_Value then
+      if OTP.Image (OTP.T.TOTP (Key, Time), 8) /= Totp_Value then
          return "Calculating TOTP value failed";
       end if;
       return "PASSED";
    end Run;
 
-end TOTP_Test;
+end OTP.T.Test;

tests/totp_test.ads → tests/otp-t-test.ads

@@ -1,4 +1,4 @@
-package TOTP_Test
+package OTP.T.Test
 with SPARK_Mode
 is
 
@@ -8,4 +8,4 @@ is
      with
        Post => Run'Result'Length <= 128;
 
-end TOTP_Test;
+end OTP.T.Test;

tests/test.adb

@@ -5,7 +5,7 @@ with Base32.Test;
 with HMAC.Test;
 with OTP.Test;
 with OTP.H.Test;
-with TOTP_Test;
+with OTP.T.Test;
 
 procedure Test
 with SPARK_Mode
@@ -39,7 +39,7 @@ begin
    Eval (HMAC.Test.Name, HMAC.Test.Run, Passed);
    Eval (OTP.Test.Name, OTP.Test.Run, Passed);
    Eval (OTP.H.Test.Name, OTP.H.Test.Run, Passed);
-   Eval (TOTP_Test.Name, TOTP_Test.Run, Passed);
+   Eval (OTP.T.Test.Name, OTP.T.Test.Run, Passed);
    if not Passed then
       Ada.Command_Line.Set_Exit_Status (1);
    end if;