Maybe that is a realy silly question. But how do I prove for platinum? In the gnatprove help I find only the modes until "gold".
Maybe "--mode=all" is the same as platinum? But I can't find anything in the internet. The most tutorials I found even skip platinum proofs.
Thanks in advance!
Stone, bronze, silver, gold, platinum are the Levels of Assurance in your project. They classify what sorts of properties you formally verify.
GNATProve can only two things for you: The flow analysis and proofing, which are performed by setting the modes flow or prove. The other options are just preliminary checks or compatibility checks or abbreviations.
This User Manual may be helpful for you.
Levels of Assurance in your project and Modes in GNATProve are not the same things. But, indeed the desired level requires different modes of GNATProve to be used. But how exactly you use the Modes and for what purpose and for what Level of Assurance depends on you.
Typically when you want to achieve the stone level in your project, you use the mode check_all, which is just a compatibility check, that checks for you, that your code uses only the SPARK subset of the Ada language.
Typically when you want to achieve the bronze level in your project, you use the mode flow (which automatically includes check_all).
The Assurance levels silver, gold, platinum are typically all achieved with the mode prove (which automatically includes flow and check_all).
For your simplification, GNATProve also allows you to pass the desired Assurance Level to the mode parameter. But this is just an abbreviation.
The Level of Assurance silver normally means, that you take your Ada code as is and execute GNATProve in the proof mode in order to verify that you don't have runtime errors or undefined behaviour. Normally this is not as easy as it sounds. You have to add some annotations (aspects, e.g. preconditions in order to specify the range of variables) to the code.
The Level of Assurance gold means that you add more annotations (aspects) to the code in order to express certain consistency or integrity properties. GNATProve in the proof mode then proofs that these properties are true.
The Level of Assurance platinum again means more annotations, but the GNATProve mode is still proof.
You see depending on what annotations you add to the code, GNATProve in the proof mode verifies them for you. These annotations can be simple things (e.g. x < 5), complicated things (e.g. (if c then x < 5)) or even more complicated things with ghost code (e.g. (if c then value_in_expected_range(x)) where you can even use functions that has been only defined for verification purposes and artificially introduced into the code. Ghost code is such a powerful tool that it is often possible to express (parts of) your real requirements as ghost code in an abstract and formal way.
Ghost code enables you to specify aspects on a very abstract way. Assume for example you have a requirement like "On Tuesdays the car shall never drive faster than the laws allow." You could define this with all details in a SPARK annotation. But the requirement is written in an abstract way. You often prefer to write the SPARK annotation at a similar level of abstraction, for example (if weekday(today) = Tuesday) then speed < local_speed_limit(location)). And that is what platinum level stands for. But that would only work if the functions weekday and local_speed_limit exist. If not you have to write them. But if they are only ever used for this SPARK annotation, you can mark them (but you don't have to) as Ghost code, so that the compiler knows, that they don't go into the compilation.
With ghost code you can establish a complete different view to your Ada code. When you have done this exhaustively, you can even replace the implementation (you said by a real performant implementation) and formally prove that the new implementation is still correct.
Ghost functions are not essential. Ghost functions are normal functions. There is nothing special. You don't have to mark them as ghost. Marking something as ghost is a hint to the compiler, that this part of the program is never used. Typically for the Level of Assurance platinum you use such extra functions more often.
In practice it is often not easy to convince GNATProve that something is true. You quite often have to help GNATProve. Ghost functions are one tool for this. I'll give an example. You have an array of 200 elements and you fill it values that are generated by a function calc_val that returns either 12 or 17 or 19.
Then you want GNATProve to verify that all of the elements of the array are in the range 10 .. 20.
This may be too complicated for GNATProve. But if you define a function is_in_range_10_20 and set this as a post for calc_val, for GNATProve it is easyier to verify that all values of the arrays fulfil is_in_range_10_20. That would be ghost code. Functionally this ghost code does not contribute to your problem and it is not very intuitive that you need it. But technically it is a nice way to help GNATProve.