VER-004: Undocumented NTT primitives representation invariants may cause incorrect computations

[gnosed]

Finding

Finding ID	VER-004
Veridise issue	#1289
Severity	Warning
Likelihood	Not Likely
Impact	Bad

Full tracking: docs/audit/findings/VER-004-ntt-representation-invariants.md (this PR's branch)

Description

The NTT implementation represents field elements as u32 values in scalar helpers and as u16 values in polynomial arrays. A field element has multiple integer representatives congruent modulo Q, while its canonical representative lies in [0, Q). The implementation also uses two polynomial domains: coefficient and evaluation and two field encodings: natural and Montgomery.

Most primitives in ntt.rs rely on specific range, domain, and encoding invariants. When these preconditions hold, the functions produce correct canonical outputs in the documented domain and encoding. These preconditions are not documented consistently.

Impact

Non-canonical inputs may violate arithmetic bounds, resulting in overflow, incorrect values, or non-canonical outputs. Likewise, passing a polynomial in the wrong domain or Montgomery representation may produce values that are valid field elements but do not represent the intended computation. Future refactors or code reuse could therefore pass values with an unsupported range, domain, or encoding. Such misuse can potentially lead to erroneous verification decisions.

Recommendation

For each of the functions document the conditions on the inputs and the resulting guarantees on the result precisely. The following functions should clearly document their input and output invariants:

1. field_add() and field_sub() require canonical x and y using the same encoding, either natural or Montgomery. Their output is canonical and preserves that encoding.
2. field_halve() requires canonical x in either natural or Montgomery encoding. Its output is canonical and preserves the encoding.
3. montgomery_mul requires x and y so that x*y is bounded by 2^16*Q. The result will be canonical.
4. ntt_forward requires a to be a coefficient-domain polynomial with canonical entries using a consistent encoding, either natural or Montgomery. Its output is canonical, remains in the same encoding, and is in the evaluation domain.
5. ntt_inverse requires a to be an evaluation-domain polynomial with canonical entries using a consistent encoding, either natural or Montgomery. Its output is canonical, remains in the same encoding, and is in the coefficient domain.
6. poly_to_montgomery requires f to contain canonical entries in natural encoding. Its output is canonical and Montgomery-encoded. Because the operation is pointwise, it preserves the polynomial domain.
7. poly_sub requires f and g to contain canonical entries and to use the same polynomial domain and encoding. Its output is canonical and preserves the other two properties.
8. poly_prepare_for_mul requires h to be a coefficient-domain polynomial with canonical entries in natural encoding. Its output is canonical, Montgomery-encoded, and in the evaluation domain.
9. poly_pointwise_mul() requires f and g to be evaluation-domain polynomials with canonical entries. Its output is canonical and remains in the evaluation domain. The encoding will depend on the encoding of the inputs.

Developers Response

The developers have been notified of the issue, but not yet provided a response.

Fix

Documentation-only change to contracts/falcon-512-core/src/ntt.rs:

• A module-level "Representation invariants" section defines the three axes once (canonical range, field encoding, polynomial domain) so the per-function docs can reference shared vocabulary.
• Each of the ten primitives named above carries doc comments stating its preconditions and postconditions, matching the recommendation.

No executable code changed. cargo test and cargo doc --no-deps (with -D warnings, to catch broken intra-doc links) both pass.