Consider using heapless::Vec

[geonnave]

I was not aware of Vec in the heapless crate until recently when mentioned by @chrysn. Now it seems that EdhocMessageBuffer is growing to be more and more like a re-implementation of that. Thus, it may make sense to just switch and use heapless::Vec.

Considerations:

• Binary size: I did a quick test in the no-std example and it added only 1 KB to the binary size
• Hax: need to check if / how it would have an impact there

[chrysn]

My guess at the main difference is that heapless (wohoo, of which there is 0.8.0 now!) would uses MaybeUninit and unsafe, whereas EdhocMessageBuffer is safe at the cost of initial nulling.

A proof that heapless indeed never reads from uninitialized memory would be awesome, but may also not be a priority.

Unless hax just makes magic happen already anyway, a practical option may be to evolve EdhocMessageBuffer to a point where it is a (safe, null-initializing) drop-in replacement to heapless. Then, lakers-shared could have a feature to enable either the built-in (proof friendly and thus known to be safe) structure, or pub use heapless::Vec as MessageBuffer; (which saves flash by reusing an implementation likely used elsewhere, and enhances performance by foregoing the nulling).

On the long run, this path could converge onto using heapless if and when hax manages to prove that heapless::Vec is publicly equivalent to our message buffer.

[geonnave]

Sounds like a good plan, thanks for providing more detail.