I’ve been generating SPARK bodies against fixed specifications and checking them with gnatprove --level=2, and I’ve hit an obligation I can’t discharge. I suspect I’m missing a standard idiom rather than anything deep, so I’d be glad of a steer.
The specification is a cumulative product over an array, with everything bounded by construction:
Max_Index : constant := 13;
Max_Value : constant := 4;
Max_Product : constant := Max_Value ** (Max_Index + 1);
subtype Index_Type is Natural range 0 .. Max_Index;
subtype Value_Type is Integer range -Max_Value .. Max_Value;
subtype Product_Type is Integer range -Max_Product .. Max_Product;
type Int_Array is array (Index_Type range <>) of Value_Type;
type Product_Array is array (Index_Type range <>) of Product_Type;
procedure Cum_Prod (A : Int_Array; Result : out Product_Array) with
Pre => Result'First = A'First and then Result'Last = A'Last
and then A'Length > 0,
Post => Result (A'First) = A (A'First)
and then (for all I in A'First + 1 .. A'Last =>
Result (I) = Result (I - 1) * A (I));
The body is the obvious one, with the prefix invariant:
Result (A'First) := A (A'First);
for I in A'First + 1 .. A'Last loop
Result (I) := Result (I - 1) * A (I);
pragma Loop_Invariant
(for all J in A'First + 1 .. I => Result (J) = Result (J - 1) * A (J));
end loop;
GNATprove reports:
medium: range check might fail, cannot prove lower bound for Result (I - 1) * A (I)
which is fair. From the subtypes alone, Result (I - 1) could be as large as Max_Product, and Max_Product * Max_Value is outside Product_Type. The values never actually overflow — the array holds at most 14 elements each bounded by 4, so the true maximum is exactly 4**14 = Max_Product — but the prover has no reason to believe that.
The natural strengthening is a bound that grows with the index:
pragma Loop_Invariant
(for all J in A'First .. I => abs Result (J) <= Max_Value ** (J - A'First + 1));
That states the right thing. The preservation step is where I get stuck. Establishing abs Result (I) <= Max_Value ** (I - A'First + 1) from abs Result (I - 1) <= Max_Value ** (I - A'First) needs
Max_Value ** (n + 1) = Max_Value ** n * Max_Value
and GNATprove doesn’t appear to know that identity for a variable exponent — the assertion is reported as medium: assertion might fail.
My questions:
-
Is there a recognised idiom for this? My instinct is a ghost lemma procedure with the power identity as its postcondition and a null body, in the style of the manual-proof sections of the User’s Guide. I’d rather use the community’s usual approach than invent one badly.
-
Is a bounded
Product_Typesimply the wrong modelling choice here? Switching the result type toBig_Integerremoves every overflow obligation and the postcondition proves cleanly, but it changes what the contract promises. I’d like to know which way people lean when the bound is a fact about the inputs rather than something the caller supplies. -
Is there a way to make the range fact available to the prover without an explicit exponent — for instance carrying a ghost variable holding the running bound, so the arithmetic stays linear?
I’d rather understand this than work around it. Happy to post the full compilable spec and body if that helps.