Paper 2026/1223
Neon NTT - (Auto)formalised
Abstract
This document provides a machine-checked Isabelle/HOL formalisation of the modular-arithmetic core of the Neon NTT paper of Becker, Hwang, Kannwischer, Yang, and Yang. We develop parametric theories of Barrett and Montgomery reduction and multiplication; the equivalence of Barrett and Montgomery arithmetic; the doubling- and rounding-Montgomery variants; and correctness and bounds theorems for Neon assembly kernels, against a hand-written model of the word arithmetic underlying the relevant Neon instructions. The development is a directed auto-formalisation: definitions, theorem statements, and proofs were produced by Claude Opus 4.7 and 4.8 using AutoCorrode's LLM-Isabelle integration layers. The human author set the architecture, chose abstractions and proof strategies, often nudged the model toward shorter or cleaner proofs, and controlled which output entered the development. This document is auto-generated from the Isabelle sources through Isabelle’s document preparation system, eliminating drift between prose and formal artifact.
Metadata
- Available format(s)
-
PDF
- Category
- Implementation
- Publication info
- Preprint.
- Keywords
- Isabelle/HOLFormal VerificationAuto-formalisationLLMsModular ArithmeticBarrett Reduction
- Contact author(s)
- beckphan @ amazon co uk
- History
- 2026-06-10: approved
- 2026-06-10: received
- See all versions
- Short URL
- https://ia.cr/2026/1223
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2026/1223,
author = {Hanno Becker},
title = {Neon {NTT} - (Auto)formalised},
howpublished = {Cryptology {ePrint} Archive, Paper 2026/1223},
year = {2026},
url = {https://eprint.iacr.org/2026/1223}
}
