Use quantifiers over message fields instead of large conjunctions

[kanigsson]

Context and Problem Statement

Currently, Recordflux generates predicates and postconditions that contain large conjunctions, where each conjunct expresses some property for a given record field. An example is the postcondition of Reset_Dependent_Fields, but there are many others. gnatprove has a lot of trouble with these large expression, and I believe this is the biggest source of inefficiencies when processing the generate code (see also #767).

Considered Options

O1

Given that message fields are already explicit in SPARK code via an enumeration type, it seems possible to replace the large conjunctions by much smaller quantified expressions. A quick experiment on the dhcp example lead to a large reduction of processing time (from 6 to 4 minutes, ignoring prover time, by replacing just one large conjunction). Impact on provability needs to be assessed.

O2

TBD.

Decision Outcome

TBD

[kanigsson]

I have done some more experiments but they are not conclusive so I'm closing the issue now and will open new issues when necessary.