The compile-time guard in PoseidonMessageHash::apply that checks the hash output decodes injectively into DIMENSION base-w chunks is too permissive.
Location: src/symmetric/message_hash/poseidon.rs, the const { ... } block in apply (the "Injective decoding to chunks" assertion).
Property it must enforce. Decoding is injective only if the chunk space is at least as large as the hash-output space:
p^HASH_LEN_FE ≤ w^DIMENSION ⟺ HASH_LEN_FE · log2(p) ≤ DIMENSION · log2(w)
Current check: ⌊log2(p)⌋ · HASH_LEN_FE ≤ DIMENSION · ⌈log2(w)⌉. Both roundings are in the permissive direction — it under-counts the left side and over-counts the right — so the condition is necessary but not sufficient.
Counterexample. HASH_LEN_FE = 8, DIMENSION = 240, w = 2 passes the assertion (8·30 ≤ 240·1), yet p^8 ≈ 2^247.9 > 2^240 = w^DIMENSION, so the decoding is not injective — contradicting the assertion's own comment.
Note. No shipped instantiation is affected: the ones in the tree use power-of-two w and satisfy the tightened check (the tightest, HASH_LEN_FE=8 with DIMENSION=32/w=256 and DIMENSION=256/w=2, give 8·31 = 248 ≤ 256; ⌈log2(p)⌉ = 31 for the KoalaBear prime). So this is latent hardening against a future parameter set, not a live bug.
Suggested fix. Upper-bound the left with ⌈log2(p)⌉ and lower-bound the right with ⌊log2(w)⌋:
HASH_LEN_FE · ⌈log2(p)⌉ ≤ DIMENSION · ⌊log2(w)⌋
I have a patch ready that makes this change (keeping all current instantiations valid) and corrects the derivation comment — happy to open a PR if this looks right.
The compile-time guard in
PoseidonMessageHash::applythat checks the hash output decodes injectively intoDIMENSIONbase-wchunks is too permissive.Location:
src/symmetric/message_hash/poseidon.rs, theconst { ... }block inapply(the "Injective decoding to chunks" assertion).Property it must enforce. Decoding is injective only if the chunk space is at least as large as the hash-output space:
Current check:
⌊log2(p)⌋ · HASH_LEN_FE ≤ DIMENSION · ⌈log2(w)⌉. Both roundings are in the permissive direction — it under-counts the left side and over-counts the right — so the condition is necessary but not sufficient.Counterexample.
HASH_LEN_FE = 8, DIMENSION = 240, w = 2passes the assertion (8·30 ≤ 240·1), yetp^8 ≈ 2^247.9 > 2^240 = w^DIMENSION, so the decoding is not injective — contradicting the assertion's own comment.Note. No shipped instantiation is affected: the ones in the tree use power-of-two
wand satisfy the tightened check (the tightest,HASH_LEN_FE=8withDIMENSION=32/w=256andDIMENSION=256/w=2, give8·31 = 248 ≤ 256;⌈log2(p)⌉ = 31for the KoalaBear prime). So this is latent hardening against a future parameter set, not a live bug.Suggested fix. Upper-bound the left with
⌈log2(p)⌉and lower-bound the right with⌊log2(w)⌋:I have a patch ready that makes this change (keeping all current instantiations valid) and corrects the derivation comment — happy to open a PR if this looks right.