I think the proposed change is beneficial, give me one more day and I will report back on the state of the hacspec cleaning.

This is targeting remove-hacspec now, given that that's the way forward and much easier with this PR -- every change made against main would need manual rebasing after #106 is merged anyway. I'm having trouble building locally with the remove-hacspec branch so far (from psa-crypto-sys); until I've managed to resolve that, I may be a bit force-pushy while I iron out bugs CI finds.

Applying this to all the remaining hex parts, I think I'm done, except that I have questions / notes:

• A few of the arguments could take an array reference instead of a slice; this would move some checks from runtime to build time. I chose not to do that because I hope that on the long run there will be the option for algorithm agility, and then we need flexibility again.
• ID_CRED_x have fixed lengths. That appears odd to me, but I won't change unrelated things in here.
• The low-level functions such as r_process_message_3 take CRED_x as a reference into an array and an extra length instead just as a slice. Is there any good reason for this? If not I'd change it in here right away, and it's a justifiable change in this PR because there was at least a (bad) reason for doing it before, being that the hex string had to be turned into a stack allocated buffer, which went away. (It's a bad reason because even then a slice could have been passed in, but at least the allocation made sense, so it may have not been caught by an earlier refactoring).
• There is trouble with f-star generation. Could you help me out here?

Responding to some comments:

I'm having trouble building locally with the remove-hacspec branch so far (from psa-crypto-sys)

Just to make sure, this is how I call it as of today in the remove-hacspec branch: cargo test --package edhoc-rs --package edhoc-crypto --package edhoc-ead --no-default-features --features="cb-psa, ead-none" --no-fail-fast.
You could also try cb-hacspec instead.

There is trouble with f-star generation. Could you help me out here?

Don't worry about it, we will likely skip this test from CI until the hacspec side is adjusted.

@chrysn remove-hacspec has been merged, targeting main should be fine now :)

Way ahead of y... oh, that comment came in 4 minutes before I rebased, so things all have their proper sequence :-)

I've also given converting the CRED_x buffers into slices a try; that leaves only comments with on likely need for change from my side. It works in the first tests, but the big question is whether there is anything hax doesn't like about it.

(And the build issues, but that's a combination of "I don't have the right PSA sources installed" and "some examples don't respect the crypto- features and pull in PSA crypto unconditionally", which I think I can address separately).

Regarding the compilation for PSA, I've easily made it work on Ubuntu but not on MacOS. As a result, when I'm on the Mac, I cargo test it within a multipass Ubuntu VM.

The changes look great! Some notes:

C example

I don't know if I got it right but should it be updated as follows?

Use

static const uint8_t ID_CRED_I[] = {0xa1, ... };

Instead of

static const uint8_t ID_CRED_I[] = "a104412b";

Impacts on hax

@W95Psp could you give a quick look? Here's one example of the kind of change we're looking at:

fn compute_mac_2(
    prk_3e2m: &BytesHashLen,
    id_cred_r: &BytesIdCred,
    cred_r: &[u8],  // <--- this type changed from `&BytesMaxBuffer` (note that `type BytesMaxBuffer = [u8; MAX_BUFFER_LEN]`)
    th_2: &BytesHashLen,
) -> BytesMac2 {

Good catch on the C side; fixed. (That's why I like statically typed languages :-D).

Looks good to me! The only unknown is the use of &[u8] with hax, but since hax only targets lib/src/lib.rs, that means only cred_X are impacted, which would be easy to modify if needed.