Unable to prove SPDM spec

[jklmnn]

I tried to prove our current spec for SPDM. The proof was done with the generated code, spec and project file in spdm.tar.gz. The results are included in spdm.log.

[kanigsson]

I can reproduce this. SPARK just slowly eats all memory. The --memory-limit switch doesn't help because it's SPARK itself (and not the provers) that eats the memory. This requires SPARK work to check where the inefficiencies arise.

[kanigsson]

@jklmnn Could you try again with the change I merged on #811? I would be curious to know if gnatprove proceeds any further.

[jklmnn]

I ran the prove again with the commit 0c040681337d4c8a7a9a4dd0231289cc72391c5c from SPDM and dd4eb1b from RecordFlux. This is the result:
spdm.tar.gz.

The general memory usage seems to have improved, with -j48 it's most of the time using ~130GB (instead of >250GB before). However there is a single gnatwhy3 process running eating the whole 1TB until the proof stops.

[kanigsson]

Great, thanks! I can see that the proofs of the various Reset_Dependent_Fields procedures still take ages. I think we can apply to the body of the procedure the same optimization that I applied to the postcondition - replace the large body by a loop. I will create a new ticket and try that this week.

[kanigsson]

@jklmnn Let's try again :-) The changes on #840 should speed things up, please let me know how this goes.

[jklmnn]

spdm.tar.gz
As far as I could tell it took even less memory than the last time. However it also took longer (the reason might also be that it crashes later). The log size is roughly the same, but still full of out of memory errors. Unfortunately I didn't look at the right times so I can't tell you if there was a process eating up all the memory at the end. For most of the time I think we were even in a 1GB/process boundary.

[kanigsson]

I can still see the old code generation there ... can you please make sure you have RecordFlux commit 9bd0260 and try again?

[jklmnn]

I forgot to pull the latest commit. spdm.tar.gz is hopefully up to date now.

[kanigsson]

Thanks. Forgot to say that I am now able to generate the code myself from the SPDM repo directly.

[senier]

Not a RecordFlux ticket.