how to prove this example

[kanigsson]

chat.rflx.txt
main.adb.txt
server.rflx.txt

The attached example generates and compiles fine, but doesn't prove. The first unproved VC is when accessing the Payload_Size field of the Msg (in the Send state). Intuitively this is clear to me, as there is no code which carries the info that the Msg is Valid over to the Send state. How to solve this issue?

By the way, I have introduced the Send state because I don't know how to check for validity of a message in the middle of a state. Maybe there is another solution.

[treiher]

We discussed various options to address similar issues in #691. We considered adding state contracts to carry information from one state to another and a mechanism to check for properties inside a state, but we decided against both solutions, as the specification would become more complex and less readable. In the future, checks that ensure the provability of all VCs will be automatically generated (e.g., if a message field is accessed, a check ensuring the validity of the message before the field access is automatically added). If such a check fails, the exception transition is taken. For some cases this is already done, but many cases are still missing. We plan to solve that issue soon (we will most probably need it for SPDM). Until this is done, the generated code for several examples will be unprovable.

[kanigsson]

Thanks Tobias. I will close this as a duplicate of #691.