search

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
12 stars 10 forks source link

Changes after hax meeting #157

Closed geonnave closed 7 months ago

geonnave commented 7 months ago
geonnave commented 7 months ago

I now realize that hax sometimes does not yield errors, even though the generated .fstar files may contain messages such as something is not implemented yet. So, maybe, in addition to calling cargo-hax and making sure it doesn't error, we should also ensure that the return of find -name *.fst -type f | xargs grep "something is not implemented yet" is empty.

malishav commented 7 months ago

I now realize that hax sometimes does not yield errors, even though the generated .fstar files may contain messages such as something is not implemented yet. So, maybe, in addition to calling cargo-hax and making sure it doesn't error, we should also ensure that the return of find -name *.fst -type f | xargs grep "something is not implemented yet" is empty.

I think that this is a good idea.