Open geonnave opened 7 months ago
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.
Sounds like a good plan, thanks for providing more detail.
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 useheapless::Vec
.Considerations:
no-std
example and it added only 1 KB to the binary size