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

refactor!: Move crypto operations into a trait. #127

Closed chrysn closed 8 months ago

chrysn commented 8 months ago

This is a reroll of #103, which has become quite inconvenient to merge.

As a practical difference, the functions that used to be moved into a CryptoExt trait now just take a crypto first argument -- not much of an ergonomics setback, but easier to understand code.

chrysn commented 8 months ago

There are still quite a few instances of default_crypto() around that eventually should be relegated to tests and example only. The most prominent leftovers are in lib/src/lib.rs that is not generic yet -- but that is probably easier to do once the C API is in the freezer.

chrysn commented 8 months ago

Ready from my PoV -- please review. This would then be a sensible base for the big typestating bout.

geonnave commented 8 months ago

Just to note, I am having trouble with installing and running [hax] on my computer, to run against this PR. I am on it, but the build takes time (and fails after a lot o fime). Once I solve that and the fstar generation works, I would be happy to merge this PR.

geonnave commented 8 months ago

I was finally able to install and run hax in my mac -- and these changes do not affect hax into fstar.

There are still some errors but they were already present at the previous implementation, i.e., the only complaints are due to the recursive order of some elements in the consts crate. I leave the full output below for reference.

Details

``` cargo-hax -C -p edhoc-rs -p edhoc-consts --no-default-features --features="crypto-hacspec, ead-none" --release \; into -i '-c_wrapper::** -edhoc_rs::generate_connection_identifier_cbor -edhoc_rs::generate_connection_identifier' fstar Compiling edhoc-consts v0.1.0 (/Users/geovane/Developer/inria/dev/edhoc-rs-FORK/consts) warning: unused import: `super::structs::*` --> consts/src/lib.rs:225:9 | 225 | use super::structs::*; | ^^^^^^^^^^^^^^^^^ | = note: `#[warn(unused_imports)]` on by default thread 'rustc' panicked at 'attempted to read from stolen value: rustc_middle::thir::Thir', cli/driver/src/exporter.rs:142:22 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace error: The THIR body of item DefId(0:57 ~ edhoc_consts[76f7]::structs::BytesSuites::{constant#0}) was stolen. This is not supposed to happen. This is a bug in Hax's frontend. This is discussed in issue https://github.com/hacspec/hacspec-v2/issues/27. Please comment this issue if you see this error message! --> consts/src/lib.rs:69:33 | 69 | pub type BytesSuites = [u8; SUITES_LEN]; | ^^^^^^^^^^ thread 'rustc' panicked at 'attempted to read from stolen value: rustc_middle::thir::Thir', cli/driver/src/exporter.rs:142:22 error: The THIR body of item DefId(0:59 ~ edhoc_consts[76f7]::structs::BytesSupportedSuites::{constant#0}) was stolen. This is not supposed to happen. This is a bug in Hax's frontend. This is discussed in issue https://github.com/hacspec/hacspec-v2/issues/27. Please comment this issue if you see this error message! --> consts/src/lib.rs:70:42 | 70 | pub type BytesSupportedSuites = [u8; SUPPORTED_SUITES_LEN]; | ^^^^^^^^^^^^^^^^^^^^ note: Writing file "/Users/geovane/Developer/inria/dev/edhoc-rs-FORK/consts/proofs/fstar/extraction/Edhoc_consts.fst" note: Writing file "/Users/geovane/Developer/inria/dev/edhoc-rs-FORK/consts/proofs/fstar/extraction/Edhoc_consts.Cbor.fst" note: Writing file "/Users/geovane/Developer/inria/dev/edhoc-rs-FORK/consts/proofs/fstar/extraction/Edhoc_consts.Common_edhoc_parsing.fst" note: Writing file "/Users/geovane/Developer/inria/dev/edhoc-rs-FORK/consts/proofs/fstar/extraction/Edhoc_consts.Consts.fst" note: Writing file "/Users/geovane/Developer/inria/dev/edhoc-rs-FORK/consts/proofs/fstar/extraction/Edhoc_consts.Helpers.fst" note: Writing file "/Users/geovane/Developer/inria/dev/edhoc-rs-FORK/consts/proofs/fstar/extraction/Edhoc_consts.Structs.fst" warning: `edhoc-consts` (lib) generated 1 warning error: could not compile `edhoc-consts` (lib) due to 2 previous errors; 1 warning emitted ```

geonnave commented 8 months ago

@malishav I am ok with merging this. Do you wish to provide any input?