with Interfaces;
with SPARK.Containers.Formal.Unbounded_Vectors;
with Ada;
with Ada.Containers;

use type Ada.Containers.Count_Type;

package Int8_Matmul_Pkg
  with SPARK_Mode => On
is

   package Integer_8_Vectors is new SPARK.Containers.Formal.Unbounded_Vectors
      (Index_Type   => Natural,
       Element_Type => Interfaces.Integer_8,
       "="          => Interfaces."=");

   type Int8_Matrix_Type is record
      Data                           : Integer_8_Vectors.Vector;
      Leading_Dimension              : Integer;
      Row_Count                      : Integer;
      Column_Count                   : Integer;
   end record;

   package Int8_Matrix_Type_Vectors is new SPARK.Containers.Formal.Unbounded_Vectors
      (Index_Type   => Natural,
       Element_Type => Int8_Matrix_Type);

   package Integer_32_Vectors is new SPARK.Containers.Formal.Unbounded_Vectors
      (Index_Type   => Natural,
       Element_Type => Interfaces.Integer_32,
       "="          => Interfaces."=");

   type Int32_Matrix_Type is record
      Data                           : Integer_32_Vectors.Vector;
      Leading_Dimension              : Integer;
      Row_Count                      : Integer;
      Column_Count                   : Integer;
   end record;

   package Int32_Matrix_Type_Vectors is new SPARK.Containers.Formal.Unbounded_Vectors
      (Index_Type   => Natural,
       Element_Type => Int32_Matrix_Type);

   function Sum_Of_Products
     (A             : Int8_Matrix_Type;
   B             : Int8_Matrix_Type;
   I, J, L_Upper : Integer;
   LDA, LDB      : Integer) return Interfaces.Integer_32
   is
     (if L_Upper <= 0 then 0
   else Interfaces."+"
          (Sum_Of_Products (A, B, I, J, L_Upper - 1, LDA, LDB),
           Interfaces."*"
             (Interfaces.Integer_32
                (Integer_8_Vectors.Element
                   (A.Data, (I - 1) + (L_Upper - 1) * LDA)),
              Interfaces.Integer_32
                (Integer_8_Vectors.Element
                   (B.Data, (L_Upper - 1) + (J - 1) * LDB)))))
   with Ghost,
     Pre => I >= 1
            and then J >= 1
            and then L_Upper >= 0
            and then LDA >= 1
            and then LDB >= 1;

   procedure Int8_Matmul
     (M   : Integer;
   N   : Integer;
   K   : Integer;
   A   : Int8_Matrix_Type;
   LDA : Integer;
   B   : Int8_Matrix_Type;
   LDB : Integer;
   LDC : Integer;
   C   : out Int32_Matrix_Type)
   with
     Pre  => M > 0
          and then N > 0
          and then K > 0
          and then LDA >= M
          and then LDB >= K
          and then LDC >= M
          and then K <= 133164
          and then A.Leading_Dimension = LDA
          and then A.Row_Count >= M
          and then A.Column_Count >= K
          and then B.Leading_Dimension = LDB
          and then B.Row_Count >= K
          and then B.Column_Count >= N
          and then Ada.Containers.Count_Type
                     (Integer_8_Vectors.Length (A.Data))
                   >= Ada.Containers.Count_Type (LDA * K)
          and then Ada.Containers.Count_Type
                     (Integer_8_Vectors.Length (B.Data))
                   >= Ada.Containers.Count_Type (LDB * N),
     Post => C.Row_Count = M
          and then C.Column_Count = N
          and then C.Leading_Dimension = LDC
          and then Ada.Containers.Count_Type
                     (Integer_32_Vectors.Length (C.Data))
                   >= Ada.Containers.Count_Type (LDC * N)
          and then (for all I in 1 .. M =>
                      (for all J in 1 .. N =>
                         Interfaces."="
                           (Integer_32_Vectors.Element
                              (C.Data, (I - 1) + (J - 1) * LDC),
                            Sum_Of_Products
                              (A, B, I, J, K, LDA, LDB))));

end Int8_Matmul_Pkg;