Program-generation techniques prevail in domains that need high performance, such as linear algebra, image processing, and database. Yet, it is hard to generate high-performance programs with correctness assurance, and cryptography needs both. Masuda and Kameyama proposed a DSL-based framework for implementing a program generator, an analyzer, and a formula generator, and obtained an efficient and correct implementation of Number-Theoretic Transform (NTT) that is necessary for many cryptographic algorithms. This paper advances their study in two ways. Firstly, we systematically develop a generation-and-analysis framework so that program generation is driven by program analysis. As a concrete result, we have found an optimization that was missing in previous studies, and shown that generated program is the most optimal. Secondly, we investigate whether the framework can be applied to other algorithms including inverse NTT. By combining generated programs, we have obtained an efficient and correct implementation for polynomial multiplication, the key for several post-quantum cryptographic algorithms.