ada - 二重ループに埋め込まれた関数で Ada/SPARK 前提条件を証明する方法

Question

以下のプログラムの実行中に「prepend」の前提条件が成立することを証明しようとしています。前提条件は次のとおりです。

Length (Container) < Container.Capacity

これを証明するための私の試みは、プラグマの形式で以下のコードにあります。この前提条件が 1 つのループには当てはまることを証明できますが、2 つのループには当てはまりません。非常に複雑なループ不変条件の例は見つかりましたが、二重ループの例は見つかりません。

仕様:

with Ada.Containers.Formal_Doubly_Linked_Lists; use Ada.Containers;

package spec with SPARK_Mode is

   MAX_ILLUMINATION_SOURCES : constant Count_Type := 250001;

   package Illumination_Sources_Pkg is new 
Ada.Containers.Formal_Doubly_Linked_Lists
      (Element_Type => Positive);

   Illumination_Sources : 
Illumination_Sources_Pkg.List(MAX_ILLUMINATION_SOURCES);

end spec;

体：

with spec; use spec;
with Ada.Containers; use Ada.Containers;

procedure Main with SPARK_Mode
is
begin
   Illumination_Sources_Pkg.Clear(Illumination_Sources);

   for Y in 1 .. 500 loop
      pragma Loop_Invariant( Y <= 500 );
      for X in 1 .. 500 loop
         Illumination_Sources_Pkg.Prepend(Illumination_Sources, 17);

         pragma Loop_Invariant( X <= 500 and X*Y <= 500*500 and 
                             Illumination_Sources_Pkg.Length(Illumination_Sources) <= Count_Type(X*Y) and
                            Count_Type(X*Y) <     Illumination_Sources.Capacity);
      end loop;
   end loop;
end Main;

エラーは「ループ不変式は最初の反復で失敗する可能性があり、Illumination_Sources_Pkg.Length(Illumination_Sources) <= X*Y を証明できません」です。最初の反復後に失敗する可能性があるとは言っていないので、それは何かです。