with SPARKNaCl;       use SPARKNaCl;
with SPARKNaCl.Debug; use SPARKNaCl.Debug;
with SPARKNaCl.MAC;   use SPARKNaCl.MAC;

with Random;
with Interfaces;      use Interfaces;
with Ada.Numerics.Discrete_Random;
procedure Onetimeauth7
is
   package RB is new Ada.Numerics.Discrete_Random (Byte);
   package RBI16 is new Ada.Numerics.Discrete_Random (Index_16);
   RBG    : RB.Generator;
   RBI16G : RBI16.Generator;
   Raw_K  : Bytes_32;
   K      : Poly_1305_Key;
   A      : Bytes_16;
begin
   RB.Reset (RBG);
   RBI16.Reset (RBI16G);
--   for I in N32 range 0 .. 9999 loop
   for I in N32 range 0 .. 99 loop
      declare
         subtype C_Index is N32 range 0 .. I;
         subtype CT is Byte_Seq (C_Index);
         package RCI is new Ada.Numerics.Discrete_Random (C_Index);
         RCIG : RCI.Generator;
         C : CT;
         R1 : C_Index;
         R2 : Byte;
         R3 : Index_16;
      begin
         RCI.Reset (RCIG);
         Random.Random_Bytes (C);
         Random.Random_Bytes (Raw_K);
         Construct (K, Raw_K);
         Onetimeauth (A, C, K);
         if not Onetimeauth_Verify (A, C, K) then
            DH ("Fail ", I64 (I));
            return;
         end if;
         R1 := RCI.Random (RCIG);
         R2 := RB.Random (RBG) mod 255;
         C (R1) := C (R1) + 1 + R2;
         if Onetimeauth_Verify (A, C, K) then
            DH ("Forgery", I64 (I));
            return;
         end if;

         R2 := RB.Random (RBG) mod 255;
         R3 := RBI16.Random (RBI16G);
         A (R3) := A (R3) + 1 + R2;
         if Onetimeauth_Verify (A, C, K) then
            DH ("Forgery", I64 (I));
            return;
         end if;
      end;
   end loop;
end Onetimeauth7;