Add full type check for SHA3 portable #1157
Conversation
Parrot7483
force-pushed
the
Parrot7483/sha3-type-check
branch
from
8f7a614 to
223bcaf
Compare
franziskuskiefer
left a comment
franziskuskiefer
left a comment
There was a problem hiding this comment.
Sorry for being a little slow on this.
Here a couple first comments. Can you address them and update? Then we can do another round.
| self.buf_len + input_remainder_len <= RATE | ||
| ); | ||
|
|
||
| hax_lib::assert!(input_remainder_len.to_int() + self.buf_len.to_int() <= RATE.to_int()); |
There was a problem hiding this comment.
This requires the unconditional hax_lib dependency for debug builds. Is there a better way to do this?
There was a problem hiding this comment.
I don't think I understand this correctly. Would putting a cfg(hax) be enough? It is only needed for proof.
|
@franziskuskiefer I applied your feedback and also cherry-picked one commit from my AVX/NEON branch adding the correct precondition on the traits and doing some light refactoring (mainly having consistent names for variables). |
franziskuskiefer
left a comment
franziskuskiefer
left a comment
There was a problem hiding this comment.
Thanks, looks pretty good. A couple things and some cleanup, then this can go in.
libcrux-sha3/src/simd/portable.rs
Outdated
| let value = get_ij(s, i / 5, i % 5); | ||
| let bytes = value.to_le_bytes(); |
There was a problem hiding this comment.
Are these changes needed for the proof? If yes, they'd need some explanation to why. If not, we should keep it as is.
Same for the similar change below.
There was a problem hiding this comment.
Yes, if I inline everything F* can't figure out that the bounds are correct every time. Sometimes it works sometimes it doesn't.
I think inlining let bytes = get_ij(s, octets / 5, octets % 5).to_le_bytes() should be possible.
| )] | ||
| pub(crate) trait Squeeze1<T: KeccakItem<1>> { | ||
| #[hax_lib::attributes] | ||
| pub(crate) trait Squeeze<T: KeccakItem<1>> { |
There was a problem hiding this comment.
Why did this lose the 1?
There was a problem hiding this comment.
I want to emphasize that having the Squeeze trait multiple times is because of HAX not supporting &[&mut [u8]; N] or other types with mutables inside. If that would work that would simplify a lot of things in this crate. I will write a comment explaining it.
|
@franziskuskiefer I applied your review. cherry-picked 1064d0d from SIMD branch. Merged main. |
github-actions
bot
dismissed
franziskuskiefer’s stale review
Review re-requested
Parrot7483
force-pushed
the
Parrot7483/sha3-type-check
branch
from
fb88708 to
153b003
Compare
|
I have a tendency to pressing these big green buttons on github messing everything up. sorry. |
2 participants
This PR adds full type checking for the SHA3 portable version for #395
Extract using
hax.py extract --portable, prove usinghax.py prove.Besides prove code the following things where changed:
libcrux-sha3/src/generic_keccak/xof.rsabsorb_fullfunction inlibcrux-sha3/src/generic_keccak/xof.rspreviously did not always consume the internal buffer when it was full. This state could only be reached by misusing the API. The only bug I found.This version contains a few things I would consider "hacks"
hax_lib::fstar::replaceimpl From<u32> for Algorithmdoes not work because of the panic.libcrux-sha3/src/generic_keccak/xof.rsthe#[hax_lib::fstar::options("...")]has no effect. I use anhax_lib::fstar::beforeinstead