proof of assignment in Verify

[kanigsson]

The Verify function as generated by Recordflux contains this code:

                     Ctx.Cursors (Successor (Ctx, Fld)) := (State => S_Invalid, Predecessor => Fld);

The predicate seems to be difficult to prove for SPARK currently. Previously, the code was duplicated for each field using a case statement, which helped proof but increased code size. This was recently replaced by a for loop:

               for F in Field loop
                  if Fld = F then
                     Ctx.Cursors (Successor (Ctx, Fld)) := (State => S_Invalid, Predecessor => Fld);
                  end if;
               end loop;

For SPARK, this is somewhat similar to the case statement, as the loop is unrolled and we get each case separately. However the loop unrolling has a threshold of 20. For any message with more than 20 fields, the loop is not unrolled and proof breaks down (it would require a loop invariant). This happens in SPDM code (message Alg_Struct).

[treiher]

The naive solution would be using the loop only in cases where there are at most 20 fields, and the previous approach otherwise. Is there a better solution?

[kanigsson]

It seems we can now remove the loop, please check out my pull request.