# Proving a cumulative-product loop with a bounded result type — is there a standard idiom?
**URL:** https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4715
**Category:** Help
**Tags:** spark
**Created:** [September 3, 2026, 12:59pm UTC](https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4715 "2026-09-03T12:59:24Z")
**Posts on this page:** 7
**Page:** 1
### Author:  [@Tonyg](https://forum.ada-lang.io/u/Tonyg)
#### Post date: [September 3, 2026, 12:59pm UTC](https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4715/1 "2026-09-03T12:59:24Z")
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:
```ada
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:
```ada
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:
```ada
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:
```ada
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
```ada
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:
1. 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.
2. Is a bounded `Product_Type` simply the wrong modelling choice here? Switching the result type to `Big_Integer` removes 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.
3. 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.
---
### Author:  [@Irvise](https://forum.ada-lang.io/u/Irvise)
#### Post date: [September 3, 2026, 3:27pm UTC](https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4715/2 "2026-09-03T15:27:36Z")
> [@Tonyg](#):
>
> gnatprove --level=2
Maybe you already thought about this but… You could try to increase the level to 4, which adds more solvers, gives them more time and I think it enables counterexamples. They are not only useful when something wrong is detected, they can also give tips as to what you should do to help the provers. Try that first. If it does not help, remove the `Loop_Invariant` and see what tip `gnatprove` proposes.
Best regards,
Fer
---
### Author:  [@damaki](https://forum.ada-lang.io/u/damaki)
#### Post date: [September 3, 2026, 4:16pm UTC](https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4715/3 "2026-09-03T16:16:37Z")
Did you mean to duplicate your [other post?](https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4713) kkson had already [replied there](https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4713/2).
---
### Author:  [@Tonyg](https://forum.ada-lang.io/u/Tonyg)
#### Post date: [September 5, 2026, 9:00am UTC](https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4715/4 "2026-09-05T09:00:02Z")
are you sure it gives me more solvers, I think I,m not using it right.
---
### Author:  [@JC001](https://forum.ada-lang.io/u/JC001)
#### Post date: [September 5, 2026, 9:55am UTC](https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4715/5 "2026-09-05T09:55:49Z")
I’ve generally used
```ada
--level=4 --prover=all
```
`level`, IIRC, controls how much effort is put into proving a VC; `prover`, which provers are used.
---
### Author:  [@damaki](https://forum.ada-lang.io/u/damaki)
#### Post date: [September 5, 2026, 11:46am UTC](https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4715/6 "2026-09-05T11:46:52Z")
You might find [Section 7.1.2 of the SPARK User’s Guide](https://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_run_gnatprove.html) useful to learn more about the levels. `--level=0` uses one prover (CVC5). `--level=1` and above enables all provers:
> - `--level=0` is equivalent to `--prover=cvc5 --timeout=1 --memlimit=1000 --steps=0 --counterexamples=off`
>
> - `--level=1` is equivalent to `--prover=cvc5,z3,altergo --timeout=1 --memlimit=1000 --steps=0 --counterexamples=off`
>
> - `--level=2` is equivalent to `--prover=cvc5,z3,altergo --timeout=5 --memlimit=1000 --steps=0 --counterexamples=on`
>
> - `--level=3` is equivalent to `--prover=cvc5,z3,altergo --timeout=20 --memlimit=2000 --steps=0 --counterexamples=on`
>
> - `--level=4` is equivalent to `--prover=cvc5,z3,altergo --timeout=60 --memlimit=2000 --steps=0 --counterexamples=on`
---
### Author:  [@Tonyg](https://forum.ada-lang.io/u/Tonyg)
#### Post date: [September 5, 2026, 3:19pm UTC](https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4715/7 "2026-09-05T15:19:59Z")
Thanks. Level 2 already runs all three provers, so level 4 is more time and counterexamples. I had that wrong.
The fix was on the duplicate. ksson said replace `**` with a table of the powers of 4. Keeps the invariant linear. Trying that.
The benchmark question goes in its own topic.