Hacspec compatibility: suggestions from Karthik

[geonnave]

Here are some changes suggested by @karthikbhargavan to enable translation into fstar using hax:

• [x] use chunk instead of step_by
• [x] use for instead of loop or while with break
• [x] add traits for structs
• [x] use if instead of match with ranges

The items above are being addressed in PR #81.

In addition, there are other issues that arise when running cargo hax into fstar, but these are not straightforward to fix from the edhoc-hacspec side:

• do not call RNG code from hacspec code, as in the case of p256_generate_key_pair. This code is not being called from edhoc-hacspec, so it should not really be a problem. According to @karthikbhargavan, they might add a flag to hax so that it treats certain functions as opaque items.
• lines such as output.len = 1; and output.content[0] = ead_1.label;. This is not straightforward to fix since it would require re-thinking our buffer mechanisms.

[geonnave]

This is basically solved now:

• PR #81 needs a review before merge
• the branch hacspec in the original repo has the fixes from PR 81 and can successfully generate fstar code

[geonnave]

Solved in #81