Generating Programs for Polynomial Multiplication with Correctness Assurance
summary
Generates verified polynomial-multiplication code by driving a DSL-based program generator with stronger interval analysis and formula synthesis; finds an analysis-driven optimization that eliminates 69% of reductions, tests all smaller variants to establish optimality in the explored search space, and composes NTT plus inverse NTT to produce an efficient, correct multiplier for post‑quantum schemes. Low‑level reductions are brute‑force verified in about one minute and high‑level equivalence is proven via formula generation (≈6 minutes) with checking in ≈6 seconds.
AI-written summary · about
chapters (8)
- 0:00Program generation for cryptography
- 3:18Post-quantum cryptography and NTT
- 8:02NTT code optimization challenges
- 13:54Interval analysis optimizations
- 14:39Proving correctness of generated code
- 19:42Contributions and future work
- 20:52Q&A: Optimizing with constant tables
- 22:21Q&A: Brute-force verification
related talks
45mPrice of Active Security in Multiparty Computation
17mAlgebro-geometric Algorithms for Template-Based Synthesis of Polynomial Program...
51mDistributed Zero-Knowledge Proofs and Applications to Secure Computation
20mHEaaN.MLIR: An Optimizing Compiler for Fast Ring-Based Homomorphic Encryption
22mHow to Synthesize Quantum-Circuit Optimizers
14mVerification of Algorithm and Code Generation for Signal Transforms
15mAssertion-Based Optimization of Quantum Programs
49mCompiling to preserve our privacy