unprovable condition for Available_Space

[kanigsson]

This ticket uses the same reproducer as #974. I'm creating a new ticket as this seems to be an independent issue. When modifying the code by hand to help proof, one check still does not get proved:

rflx-over-repr.ads:905:61: medium: precondition might fail, cannot prove Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld)

The line number is probably off due to local modifications, in any case it comes from this expression in Field_Condition:

             U64 (Ctx.Cursors (F_Length).Value) * 8 >= U64 (Field_Last (Ctx, F_Hash)) - U64 (Ctx.Cursors (F_Count).First) + 17,

Available_Space is defined as follows;

   function Available_Space (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length is
     (Ctx.Last - Field_First (Ctx, Fld) + 1);

note the Ctx.Last. The Valid_Context predicate only provides a condition like this:

                                             Cursors (F_Hash).Last - Cursors (F_Hash).First + 1 = 32

There seems to be something missing that links Ctx.Last with Cursors (Fld).Last for some field Fld. Does that make sense? Or am I missing something?