You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
We need to implement the various functions in Section 7.4.
The spec overloads these to apply both to individual values and to vectors (mapping the individual function to each element of the vector). Since we can't overload names in cryptol, we'll use the same naming scheme that we used in ML-KEM: appending _Vec to the name for the vector functions.
That said, I think we might not need both versions of the function in every case. E.g. it looks like Power2Round is only used in the vector case; we might be fine to just define it for that case at the top level and have the Algorithm 35 be a sub-function (e.g. defined in the where clause). Decompose seems to only be used in the subsequent high/low bits and hint functions in this section, so maybe it doesn't need to be defined for vectors.
The IPD versions of these all look pretty good, so this should mainly be a docs update PR.
Audit use cases of these functions to determine which top-level function signatures we need.
Implement and update docs for Power2Round
Implement and update docs for Decompose
Implement and update docs for HighBits and LowBits
Implement and update docs for MakeHint and UseHint
The text was updated successfully, but these errors were encountered:
We need to implement the various functions in Section 7.4.
The spec overloads these to apply both to individual values and to vectors (mapping the individual function to each element of the vector). Since we can't overload names in cryptol, we'll use the same naming scheme that we used in ML-KEM: appending
_Vec
to the name for the vector functions.That said, I think we might not need both versions of the function in every case. E.g. it looks like
Power2Round
is only used in the vector case; we might be fine to just define it for that case at the top level and have the Algorithm 35 be a sub-function (e.g. defined in the where clause).Decompose
seems to only be used in the subsequent high/low bits and hint functions in this section, so maybe it doesn't need to be defined for vectors.The IPD versions of these all look pretty good, so this should mainly be a docs update PR.
Power2Round
Decompose
HighBits
andLowBits
MakeHint
andUseHint
The text was updated successfully, but these errors were encountered: