hash: Add block-only algorithm constructor

[chrysn]

Closes: #12

There's some way to go to provide the top layer, but for a first check, @WilliamTakeshi: If you'd only provide the limited version introduced here for #9, you could just drop all the buffers, and wouldn't need to deal with padding at finalization, right?

[chrysn]

With the 2nd commit I've pulled the padding out of #9. I wouldn't worry about how this is done prettily, as all that code in embedded-cal-software would eventually be replaced with libcrux, but it'll allow you to test doing #9 without any of the buffer and padding management.

[chrysn]

@jschneider-bensch, would this interface work libcrux?

And in particular: Could libcrux implement this in a way that even when using libcrux as a full SHA2 implementation, it could still provide the "bare SHA" (only full blocks, no padding) and "wrapper around bare" parts separately, and still let the proofs run through? I'm not yet sure how critical that is, but I'd rather check now and adjust if needed. If nothing else, splitting also the libcrux version along this boarder will make it easier to opt in to hardware acceleration where it is supported with less configuration effort.

[jschneider-bensch]

In libcrux-sha2, with feature expose-hacl we expose the low level functions that are otherwise wrapped by the high-level init/update/finish API, and we could conceivably implement a full-block oriented hash using these.

Regarding proofs: When we take an implementation exported from HACL (or HACL-rs), as in the case of SHA-2, we don't have a prover in the loop, so to say. The idea here is instead that HACL* is a verified implementation in F*, which can be exported to C, or Rust preserving the verification results established on the F* side, if the pre-conditions for calling any of the functions established there are maintained. So in libcrux, we leave the exported code untouched and give wrappers that ensure the pre-conditions are met and which implement the high-level API. If the low-level functions are called directly, it has to be ensured that all preconditions are met.

I have a basic question here, though: Reading through #9, I understood that the motivation for adding a block-only version is too get rid of the padding and spooling code in the provider, right? Would this then be done generically, independent of the backend?

[chrysn]

Thanks. Yeah, I think we can just pass around the preconditions.

And ad padding, yes, this would be done generically. This PR even contains¹ a very simple stupid but correct-for-the-test-cases implementation of that generic mechanism, and I hope that that Extender struct would rather sooner than later be replaced by formally verified/-fiable. code.

Footnotes

1. Ha: it doesn't, left that added but uncommitted/pushed yesterday evening! Now it's in. ↩

[WilliamTakeshi]

I did some quick tests here:
if we use this limited API, with only full blocks, I THINK I can create a implementation where we can drop the block and block_size from the HashState, but I cannot drop the padding.
Even for full-blocks, the SHA needs the padding to work.

Maybe I am missing something, but I still didn't understand the reason of this more constrained API. Is the block and the padding bad? They break something on the formal verification?

[franziskuskiefer]

@jschneider-bensch, would this interface work libcrux?

As Jonas said, this is certainly possible, but I don't think it's something we want or should do. This would require adding new, less safe APIs.
For primitives like SHA2, the tricky bits are exactly these operations around blocks. Therefore, these are also the most valuable bits to verify. Not using them makes it a little pointless to use a verified implementation.

If we want to have confidence in the implementation here later, we should use libcrux APIs as they are and rather see if we can (want to) add hardware acceleration to that implementation. Doing it the other way around (as proposed here) is not the right approach.

[chrysn]

This PR is exactly about using the verified implementation for the block bits around the hardware accelerated inner ones.

Libcrux APIs need to take in the hardware primitives, that requires having a version where it only does those outer layers and we plug in the inner ones from hardware. When we assume that the hardware is correct, AIU we'll have to annotate the hardware accelerator with the assertions that it is correct, and then the proof can run through. We can sure do with not exposing the inner half of the algorithm, but it'd give less confidence in the whole system compared to when we expose the inner part along with its proof annotations, because we'd be running different paths between when we use hardware acceleration or not.