Summary
With the addition of the nttunpack proof (#955), nttunpack_order/nttunpack_unorder are now defined in common/mldsa_specs.ml. The AVX2 NTT order is the composition mldsa_avx2_ntt_order i = bitreverse8(nttunpack_order i), and ideally mldsa_avx2_ntt_order should be defined directly in terms of nttunpack_order.
However, the NTT/iNTT proofs currently pattern-match on the expanded arithmetic form of mldsa_avx2_ntt_order during simulation, so redefining it in terms of nttunpack_order breaks them. A decomposition lemma (MLDSA_AVX2_NTT_ORDER_DECOMPOSITION) has been added alongside the original definition as a stopgap.
TODO
- Refactor
mldsa_avx2_ntt_order to be defined as bitreverse8(nttunpack_order i)
- Update the NTT/iNTT proofs to work with the new definition (may require changes to how pattern matching works during simulation)
- Remove the standalone decomposition lemma once the definition is canonical
Summary
With the addition of the nttunpack proof (#955),
nttunpack_order/nttunpack_unorderare now defined incommon/mldsa_specs.ml. The AVX2 NTT order is the compositionmldsa_avx2_ntt_order i = bitreverse8(nttunpack_order i), and ideallymldsa_avx2_ntt_ordershould be defined directly in terms ofnttunpack_order.However, the NTT/iNTT proofs currently pattern-match on the expanded arithmetic form of
mldsa_avx2_ntt_orderduring simulation, so redefining it in terms ofnttunpack_orderbreaks them. A decomposition lemma (MLDSA_AVX2_NTT_ORDER_DECOMPOSITION) has been added alongside the original definition as a stopgap.TODO
mldsa_avx2_ntt_orderto be defined asbitreverse8(nttunpack_order i)