I've some trouble to see how value types are laid on stack (conceptually, not necessary the real implementation).
First, i may be wrong but it seems that vload do not reference the corresponding Q-type, so i wonder how the verifier knows that it can then access to component of the value type. Then, it seems that value type use one slot on stack, so the components (and the boxed reference if it exists) has to be stored somewhere but there is no corresponding max value type buffer size. Rémi
