[autocorres] Arrays in binary search example about l4v

[mbrcknl]

Hi Cornelius,

Thanks for your interest in AutoCorres!

You are right that AutoCorres does not make any attempt to abstract C arrays to more user-friendly HOL types. It might be possible to do something sensible with C arrays, but it's not something we've thought about yet.

I can foresee some difficulties, however. C arrays are barely distinguishable from pointers in common usage. Any well-founded HOL abstraction of an array is going to need to know where to find the end of the array. Unfortunately, that information is lost as soon as you pass an array as a pointer.

At least for now, this means that it is up to the AutoCorres user to assert that particular pointers are arrays of particular lengths and particular contents, and to carry these assertions through the broader development.

You are also right that it ought to be possible to provide a library of predicates with which an AutoCorres user can assert a correspondence between a C array and a HOL data type, together with lemmas which explain how common C array manipulations correspond to operations on the corresponding HOL data type. Again, we just haven't spent much time on this aspect, so what you see is a collection of minimal examples rather than a comprehensive library.

Note that there might be many different ways you might want to abstract an array, depending on how you actually intend to use the array in C! Sometimes, you might want a list, sometimes a set, sometimes a partial function. Sometimes you might not want to abstract at all, because you just want to allocate a region of bytes in which to do horrible things with pointers and casts!

The main achievements of AutoCorres so far are:

• Automatically producing a shallowly-embedded abstraction (as a nondeterministic state monad) from a deeply-embedded low-level representation of the C code (in Schirmer's SIMPL language), together with a proof of refinement.
• Automatically abstracting a low-level byte-array representation of the C heap to a split heap, which makes it easier to reason about pointers to C structures.
• Automatically abstracting signed and unsigned word variables to HOL int and nat types.
• Optimisations which often make the abstract representation significantly simpler than the low-level SIMPL.

I'll think about whether we can clarify the intent of the examples. We would welcome your suggestions. In the meantime, I hope this is of some help!

Regards,
Matthew