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

use type Ada.Containers.Count_Type;

package Relu_Pkg
  with SPARK_Mode => On
is

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

   type Activation_Vector_Type is record
      Elements                       : IEEE_Float_64_Vectors.Vector;
   end record;

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

   procedure Apply_Relu
     (Input  : in     Activation_Vector_Type;
      Length : in     Integer;
      Output :    out Activation_Vector_Type)
   with
     Pre  => Length >= 0
             and then Integer (IEEE_Float_64_Vectors.Length (Input.Elements)) >= Length,
     Post => Integer (IEEE_Float_64_Vectors.Length (Output.Elements)) = Length
             and then (for all I in 1 .. Length =>
                         Interfaces."=" (IEEE_Float_64_Vectors.Element (Output.Elements, I),
                           (if Interfaces.">" (IEEE_Float_64_Vectors.Element (Input.Elements, I), 0.0)
                            then IEEE_Float_64_Vectors.Element (Input.Elements, I)
                            else 0.0)))
             and then (for all I in 1 .. Length =>
                         Interfaces.">=" (IEEE_Float_64_Vectors.Element (Output.Elements, I), 0.0));

end Relu_Pkg;