Strengthen spec for montgomery_reduce()
#292
Conversation
hanno-becker
force-pushed
the
fqmul_proof
branch
from
421eed9 to
0a83f82
Compare
hanno-becker
force-pushed
the
fqmul_proof
branch
from
0a83f82 to
4a2663a
Compare
|
Question: why do montgomery_reduce() and fqmul() have the MLKEM_NAMESPACE macro applied to them? Surely, these functions are common to all parameter sets, so no need to adjust their name according to the value of MLKEM_K? |
|
@rod-chapman Everything's prefixed by the K-dependent namespace to e.g. allow linking together multiple compilations of the lib with varying security levels. It's TBD if/how we want to avoid duplication of symbols for functions that don't depend on K. |
hanno-becker
force-pushed
the
fqmul_proof
branch
from
2f25adf to
2593753
Compare
|
To avoid symbol duplication, we might need to split the code into translation units that do depend on K, and those that don't. The latter would would be compiled exactly once. |
There are two uses of the generic Montgomery reduction `montgomery_reduce()` in the code base: - For modular multiplication with twiddles in `fqmul()` - For Montgomery reduction after accumulation in the base multiplication. Those two uses require different specifications for `montgomery_reduce()`. However, there does not appear to be a mechanism in CBMC to register more than one contract. To remedy, this commit moves the previous `montgomery_reduce()` into a static inline `montgomery_reduce_generic()`, and uses it in the definitions of `montgomery_reduce()` and `fqmul()`. The new `montgomery_reduce()` then makes bounds assumptions according to the use in base multiplication, while the call to `fqmul()` provides stronger input bounds. Accordingly, the post-condition of `montgomery_reduce()` only guarantees coefficients < 3/2q, while `fqmul()` ensures < q. The CBMC contracts an proofs for `montgomery_reduce()` and `fqmul()` are adjusted accordingly. Signed-off-by: Hanno Becker <[email protected]>
fqmul() is documented to require a 2nd input that's "< q/2" in absolute value. This is the correct meaning when reading q/2 as a _rational_ quotient, but it's not when q/2 is read as round-down division: In that case, one would need to say <= instead of <. This commit avoids any confusion by rewriting the documentation in terms of the integral quotient (q+1)/2. Signed-off-by: Hanno Becker <[email protected]>
hanno-becker
force-pushed
the
fqmul_proof
branch
from
2593753 to
b3f89d8
Compare
|
@rod-chapman We could do that, but it's a large restructuring that moves us further apart from the reference implementation. So unless we have a customer telling us about for simultaneous need for multiple security levels and deduplicated symbols, I don't think we should spend any time on this. |
hanno-becker
added
benchmark
|
Agree on the above re: symbol duplication. |
Based on: #289
Fixes #280
There are two uses of the generic Montgomery reduction
montgomery_reduce()in the code base:fqmul()Those two uses require different specifications for
montgomery_reduce(). However, there does not appear to be a mechanism in CBMC to register more than one contract.To remedy, this commit moves the previous
montgomery_reduce()into a static inlinemontgomery_reduce_generic(), and uses it in the definitions ofmontgomery_reduce()andfqmul(). The newmontgomery_reduce()then makes bounds assumptions according to the use in base multiplication, while the call tomontgomery_reduce_generic()provides stronger input bounds. Accordingly, the post-condition ofmontgomery_reduce()only guarantees coefficients < 3/2q, whilefqmul()ensures < q.The CBMC contracts an proofs for
montgomery_reduce()andfqmul()are adjusted accordingly.