refactor!: Move crypto operations into a trait.

[chrysn]

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]

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]

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

[geonnave]

Looks good to me, just left a minor comment below.

[geonnave]

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]

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]

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