openwsn-berkeley / lakers

EDHOC implemented in Rust, optimized for microcontrollers, with bindings for C and Python.
https://crates.io/crates/lakers
BSD 3-Clause "New" or "Revised" License
13 stars 10 forks source link

Improve message buffer access #153

Closed geonnave closed 10 months ago

geonnave commented 10 months ago

This introduces some unwrap calls which should not fail, and I hope it could be guaranteed by hax. If not then it can be reworked.

Deliberately not being exhaustive in the calls to .content[] within parsing routines. In this case, we also expect to have proofs from hax.

chrysn commented 10 months ago

By the way, the MessageBuffer is at this point pretty much a re-implementation of heapless::Vec. If hacspec grows well, it may be possible to just swap that in at some point. (That'd work best when all direct access to content has been removed, which AIU we currently do for efficiency reasons -- thus, it may take some time until we can do that, for may require placement return).