package body Relu_Pkg
  with SPARK_Mode => On
is

   procedure Apply_Relu
     (Input  : in     Activation_Vector_Type;
      Length : in     Integer;
      Output :    out Activation_Vector_Type)
   is
      Result : IEEE_Float_64_Vectors.Vector;
   begin
      for I in 1 .. Length loop
         declare
            X : constant Interfaces.IEEE_Float_64 :=
              IEEE_Float_64_Vectors.Element (Input.Elements, I);
         begin
            if Interfaces.">" (X, 0.0) then
               IEEE_Float_64_Vectors.Append (Result, X);
            else
               IEEE_Float_64_Vectors.Append (Result, 0.0);
            end if;
         end;
         pragma Loop_Invariant
           (Integer (IEEE_Float_64_Vectors.Length (Result)) = I);
         pragma Loop_Invariant
           (for all K in 1 .. I =>
              Interfaces."=" (IEEE_Float_64_Vectors.Element (Result, K),
                (if Interfaces.">" (IEEE_Float_64_Vectors.Element (Input.Elements, K), 0.0)
                 then IEEE_Float_64_Vectors.Element (Input.Elements, K)
                 else 0.0)));
         pragma Loop_Invariant
           (for all K in 1 .. I =>
              Interfaces.">=" (IEEE_Float_64_Vectors.Element (Result, K), 0.0));
      end loop;
      Output := (Elements => Result);
   end Apply_Relu;

end Relu_Pkg;