If I have a code base at SPARK Bronze level and for example I have a procedure that just does say a reasonably complex calculation. I could put said procedure into it’s own package and verify it at Silver or an even higher level. As far as I can see you can’t do that with a nested package or single procedure within a package. What Ada SPARK achieves already dumbfounds me so any more complexity might not be desirable, especially when breaking it into packages isn’t much of a problem. However, I thought it might be worth asking the question of how difficult it would be for SPARK to support verifying one procedure at say Silver whilst the rest of the code base is at Bronze?
(if english sounds weird, i use translator…)
I am not a SPARK expert, but I have actually done exactly that: isolating functions or procedures into their own packages to validate them separately and achieve 100% verification.
The real problem arises later on. When you integrate the code back into the main project and run gnatprove again, SPARK immediately starts generating warnings or errors, since the rest of the codebase lacks that same strict level of verification. The system will report potential overflows, division-by-zero errors, or other edge cases, given that data coming from the “Bronze” section is neither guaranteed nor protected by strict subtypes, preconditions, or postconditions.
I assume that you were running gnat prove at a higher level on the whole code base in which case you would get lots to improve upon?
The procedure/package proven to Silver would still hold e.g. to AORTE (absence of runtime errors) for all possible inputs.
I am just asking if a convenience feature of doing that within a codebase is problematic or a quite straight forward feature for gnat prove to implement. Such as via with SPARK Mode => Silver on a procedure body.
I assume that it’s a lot more complicated and problematic than it would seem but maybe not, perhaps it’s just an additional run of gnat prove and some accounting?
Edit: I guess then there is the Gnat Studio integration etc., so quite possibly problematic.
(Again… if english sounds weird, i use translator…)
That’s right, integrating with GNAT Studio adds complexity, but the real
problem is more logical than technical.
You mentioned that a Silver procedure would maintain AoRTE for all inputs
that satisfy its Pre. The drawback is that this guarantee only holds if the
caller strictly adheres to that precondition.
I’ve done that and tested the code by sending data that shouldn’t be there,
or by doing things designed to make it fail, and it has failed when I
thought it was impossible for it to fail.
In my case, I always write complete contracts with Global, Depends, Pre, and
Post, and I run gnatprove at --level=4 from the beginning. I gradually write
and test until the entire codebase passes verification. with the goal of achieving Gold/Platinum.
The real problem arises during integration. Since the rest of the existing
code is “Bronze” level and unverified, gnatprove has no mathematical way to
guarantee that data from those Bronze sections meets the strict
preconditions I defined for my procedure. This is precisely why the tool
throws an unproved-precondition obligation at the call point (the boundary
between Bronze and Gold/Silver), forcing me to refactor the surrounding
code. This is why mixing levels in an advanced, pre-existing project is so
tricky.
Even if they implemented a handy feature like SPARK_Mode => Silver in the
body of a procedure, gnatprove would still fail to discharge the Pre at
integration points unless they inserted pragma Assume everywhere to force
the system to blindly trust that Bronze-level calls send valid data.
Right. I see what you mean now. Though if the calculation does not require any Pre and just say an integer input (possibly even with a restricted range) then there would still be a benefit of guaranteeing that e.g. no integer overflows could occur within just that calculation and making that easy to do within a codebase might be very beneficial 
You’re absolutely right, but only to a certain extent. Adding restricted subtypes to a function doesn’t automatically solve the integration problem unless the mathematical boundaries have been perfectly synchronized beforehand.
Let me show you a concrete example from my code to illustrate the difference.
Case 1 : When you perform the discrete calculations in advance:
package Math_Functions with SPARK_Mode is
subtype mxb is Positive range 256 .. 256;
max_byte : constant mxb := 256;
subtype Byte_Length is Positive range 1 .. 256;
subtype Sesgo_Free is Positive range 128 .. 255;
function Byte_Division (Div : Byte_Length) return Byte_Length;
function Unbiased_Secure (Len : Byte_Length) return Sesgo_Free;
end Math_Functions;
With the body implemented as simple expression functions:
function Byte_Division (Div : Byte_Length) return Byte_Length is (max_byte / Div);
function Unbiased_Secure (Len : Byte_Length) return Sesgo_Free is
(Sesgo_Free (Len * Byte_Division (Div => Len) - 1));
In this case, I spent time performing the calculations before writing the code. Since I know the exact limits of the character set, I mathematically proved that for every possible value of Byte_Length (from 1 to 256), the formula will yield a result strictly between 128 and 255.
Because the input and output domains are perfectly synchronized, I can completely eliminate the Pre and Post contracts. GNATprove easily verifies that a runtime error is mathematically impossible, and unverified Bronze code can execute without issue.
Case 2: The danger of relying on subtypes without considering the mathematics
Now, imagine I don’t do the preliminary mathematical work and instead write this:
package Math_Functions with SPARK_Mode is
subtype mxb is Positive range 256 .. 256;
max_byte : constant mxb := 256;
subtype Byte_Length is Positive range 1 .. 1000; -- Expanded just to be "safe"
subtype Sesgo_Free is Positive range 128 .. 255; -- The rigid output range
function Byte_Division (Div : Byte_Length) return Byte_Length;
function Unbiased_Secure (Len : Byte_Length) return Sesgo_Free;
end Math_Functions;
If the unverified Bronze function passes a value greater than 255 (which Byte_Length legally allows), or if the internal calculation produces a result outside the output range, the system will instantly fail with a runtime Constraint_Error. Subtypes alone do not magically fix an incorrect mathematical formula.
You might argue, “Well, we can solve Case 2 simply by adding a robust precontract to protect the function.”
But here’s the detail people often forget: SPARK (pre/post) contracts are completely invisible to executable code at runtime unless you explicitly compile with assertions enabled (-gnata or Assertion_Policy(Check)).
If you disable assertions in production to maintain the speed of the legacy Bronze system, a robust precontract won’t prevent incorrect input from being filtered out. The program will completely skip the precheck, execute the calculation, and inevitably encounter a Constraint_Error on the output subtype.
Therefore, your idea of using restricted ranges to easily achieve Silver safety only works if the discrete math behind your input and output subtypes is already 100% flawless. If the domains don’t match perfectly, you’ll be forced to enforce strict pre-contracts (which will cause problems for whoever calls the Bronze function) or write manual defensive conditional statements within the body to limit the data.
I haven’t ran your code through gnat prove but I believe gnat prove will warn you of any potential overflows for all possible inputs to your function if this function was it’s own package and checked at silver level. So to avoid gnat prove warning you then you would need a pre condition or a type that is sufficiently restrictive. The pre is saying trust me or rather flow analysis but the type is saying trust the compiler.
You don’t need to run it;
you can check the same project I uploaded a few days ago, which is where I use it.
Summary of SPARK analysis
=========================--------------------------------------------------------------------------------------------------------------------------------
SPARK Analysis results Total Flow CodePeer
Provers Justified Unproved--------------------------------------------------------------------------------------------------------------------------------
Data Dependencies 32 32 .
. . .
Flow Dependencies 21 21 .
. . .
Initialization 20 20 .
. . .
Non-Aliasing . . .
. . .
Run-time Checks 620 . . 620 (CVC4 89%,
Trivial 7%, Z3 4%, colibri 0%) . .
Assertions 105 . . 105
(CVC4 97%, Trivial 2%, Z3 1%) . .
Functional Contracts 103 . . 103
(CVC4 89%, Trivial 2%, Z3 10%) . .
LSP Verification . . .
. . .
Termination 24 . .
24 (CVC4) . .
Concurrency . . .
. . .--------------------------------------------------------------------------------------------------------------------------------
Total 925 73 (8%) .
852 (92%) . .
max steps used for successful proof: 33855
gnatprove -PC:\Users\epriv\Desktop\Resume\default.gpr -U --output=oneline --ide
progress-bar --proof-warnings --report=all --level=4 -j4 --steps=1000000 -
prover=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
math_functions.adb:4:16: info: division check proved[#10]
math_functions.adb:7:52: info: range check proved[#14]
math_functions.adb:13:22: info: range check proved[#18]
math_functions.adb:14:22: info: range check proved[#4]
math_functions.adb:14:27: info: float overflow check proved[#5]
math_functions.adb:14:27: info: division check proved[#17]
math_functions.adb:14:47: info: float overflow check proved[#6]
math_functions.ads:13:08: info: data dependencies proved[#3]
math_functions.ads:14:18: info: postcondition proved[#12]
math_functions.ads:14:62: info: division check proved[#11]
math_functions.ads:20:08: info: data dependencies proved[#1]
math_functions.ads:21:18: info: postcondition proved[#16]
math_functions.ads:22:53: info: range check proved[#15]
math_functions.ads:28:08: info: data dependencies proved[#2]
math_functions.ads:29:18: info: postcondition proved[#13]
math_functions.ads:35:08: info: data dependencies proved[#0]
math_functions.ads:37:10: info: postcondition proved[#21]
math_functions.ads:37:41: info: range check proved[#20]
math_functions.ads:38:43: info: range check proved[#7]
math_functions.ads:38:48: info: float overflow check proved[#8]
math_functions.ads:38:48: info: division check proved[#19]
math_functions.ads:38:67: info: float overflow check proved[#9]
processprng_wrapper.ads:26:23: info: overflow check proved[#0]
And if you delegate the types to the compiler and compile with -gnatp, that ignores any exceptions. What do you do in that case, delegating trust to the compiler and the type?