Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking — Ray Iskander, Khaled Kirah | Kutubxona