docs(paper): one-contribution axis, industry-reader content, discovery discussion

Three passes over the paper (plus glosses across the docs), driven by a
professor-style structural review and an industry-reader review (crypto
protocol companies, hardware companies). No measurement changed; two
overclaims corrected.

Axis: the contribution is now stated once — a more efficient NTT core,
proven correct — with the K-RED butterfly, psi-fold ROM and verification
as its components, in two instantiations (streaming retrofit, own-FSM
core). Title: 'FoldNTT: A Formally Verified Multiplier- and Twiddle-Lean
NTT Core for Proth Primes'.

Structure (professor review): whole-core ~1% Fmax now leads the timing
paragraph (the -26% butterfly number is framed as the module-level gap
it dilutes from); a Correctness guarantee paragraph opens §5 and the
obligations table is split into proven vs simulated; the bug story is
told three times instead of seven; §6 folded into §4.3; Table
'algebraic fact -> hardware saved' opens §4; a worked K-RED trace
(v=5555 -> r=5496, hand-checked) follows the fold equations; §2/§7
positioning de-duplicated; Lemma statements already in Appendix A.

Industry readers: §4.3 gains the fold-economics boundary — F stays 2-3
and cost tracks the signed-digit weight of k, with a planner-derived
table (Falcon/Kyber/Dilithium/BabyBear/Goldilocks; Goldilocks k^F = 1
needs no ROM scaling) and an explicit 30-64-bit / RNS evaluation
boundary; MIT license stated (upstream cfntt_ref is MIT too); a
'what a hardware team can lift' artifact map in Reproducibility;
absolute-MHz open-flow hedge; 'generator supports parallel BFU'
corrected to 'construction supports'; PWM double-pass cost stated;
qualitative energy paragraph (no quantitative claim); explicit
not-a-constant-time-certification sentence; reusable-harness paragraph.

§8 is now Discussion: it documents the discovery process — the Visioned
Vibe Coding loop (formally verify -> regenerate the RTL-grounded 3D
model -> VLM critiques the renders -> design change -> verify before
accepting) built on visually-3d — with Figure 2, a five-panel strip of
the model at v1/v31/v32/v36/v37 composed from the published revision
history, and keeps the no-generality/no-ablation caveat. The README
gets the same strip and a short 'How it was found' section.

Builds: single-column PDF and IEEE two-column (10 pages) both clean —
zero LaTeX errors, zero missing glyphs, no overfull >30pt; ieee/build.sh
learns the ../../assets path fixup for figures.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Author: grandchildrice

README.md

@@ -7,19 +7,35 @@
 
 [![verify](https://github.com/NyxFoundation/FoldNTT/actions/workflows/verify.yml/badge.svg)](https://github.com/NyxFoundation/FoldNTT/actions/workflows/verify.yml)
 
-A formally verified NTT accelerator for Falcon / Proth primes, with an
-on-board Basys 3 demo and a Vivado-free toolchain.
-
-The name comes from the two core ideas, both of which fold something: K-RED
-folds modular reduction into shift-adds (one multiplier per butterfly instead
-of three), and the ψ-fold twiddle ROM folds the table in half (a shift-add
-derives the other half). Every module is proven equal to its mathematical
-spec with z3 + SymbiYosys, and the whole core runs end-to-end on a real FPGA.
+FoldNTT is one thing: a more efficient chip design for the polynomial
+multiplication at the heart of post-quantum cryptography, proven correct.
+
+The contribution in one sentence: because the cryptographic prime
+q = 12289 = 3·2¹² + 1 has a special algebraic shape, and because the table
+of precomputed constants has a mirror symmetry, most of the multiplication
+hardware and half of the constant storage can be replaced by a few
+shift-and-add gates, so the chip computes exactly the same transform with
+one hardware multiplier instead of three and half the stored constants, at
+the same speed, and every step is machine-proven equal to the mathematics.
+
+No hardware background is needed to see why this matters. Multiplier
+circuits are the scarcest resource on these chips, and computing the
+remainder after division by q is normally what consumes them. The prime's
+shape makes that remainder computable with shifts and additions (the K-RED
+trick), and the symmetry w[N/2+j] = ψ·w[j] means half the constant table
+is redundant: one shift-and-subtract recreates it. Proving every step
+equal to the mathematics, instead of testing a few examples, is also what
+exposed a real bug in the original design's inverse transform (reported
+upstream).
+
+The name: both ideas fold something. K-RED folds the remainder step into
+shift-adds, and the ψ-fold ROM folds the constant table in half.
 
 FoldNTT began as a formal-verification study of the released CFNTT radix-2
 accelerator ([xiang-rc/cfntt_ref](https://github.com/xiang-rc/cfntt_ref), Chen
-et al., TCHES 2022). That study found a bug in the inverse transform; the
-project became an own-FSM architecture that fixes it with fewer multipliers.
+et al., TCHES 2022). That study found the inverse-transform bug; the project
+became an own-FSM architecture that fixes it with fewer multipliers, running
+end-to-end on a real FPGA (a Basys 3 board) with no vendor software.
 
 ## Architecture
 
@@ -76,6 +92,22 @@ twiddle ROM is [`psi-fold-rom/`](psi-fold-rom/), and the FSM + RAM + on-board
 self-test are [`ntt-core/`](ntt-core/). The paper's Fig. 1 in [`docs/`](docs/)
 shows the same butterfly at gate/register level.
 
+## How it was found
+
+The two folds came out of a recursive loop we call Visioned Vibe Coding:
+formally verify the design, render it as a 3D floor-plan model
+([visually-3d](https://github.com/NyxFoundation)), show the renders to a
+vision-language model, turn its observations into design changes, and
+verify again before accepting anything. The ψ-fold was spotted in the
+render itself: after K-RED shrank the arithmetic, the twiddle ROM was
+visibly the largest block left, and half of it turned out to be
+mathematically redundant.
+
+<p align="center">
+  <img src="docs/assets/discovery-timeline.png" alt="3D model at five points of the discovery loop" width="100%"><br/>
+  <sub><i>The model across the loop's 37 revisions: first draft (v1); matured CFNTT floor plan, Barrett with 3 DSP (v31); the K-RED butterfly lands (v32); the ψ-fold is spotted (v36); FoldNTT final (v37). The full revision history, with the verification verdicts between steps, is published with the gallery.</i></sub>
+</p>
+
 ## Inventions
 
 | Folder | Invention | Verified | Result |
@@ -123,6 +155,7 @@ openFPGALoader -b basys3 ntt-core/build/design.bit   # LED1 = self-test PASS
   bug (missing per-stage halving) was found by verification, reported upstream.
 - **Open toolchain** synthesis → place-and-route → bitstream with no Vivado
   (yosys + openXC7 nextpnr-xilinx + prjxray).
+- MIT-licensed throughout (the upstream `cfntt_ref` submodule is also MIT).
 
 See [`docs/`](docs/) for the paper and [`docs/venue-assessment.md`](docs/venue-assessment.md)
 for the submission strategy.

docs/assets/discovery-timeline.png

@@ -2,13 +2,15 @@
 
 ## §sim: system-level RTL simulation (DONE)
 
-`verification/fullcore/run_stream.py` drives the invented RTL
-(`compact_bf_v2` + `modular_mul_kred` + `tf_rom_fold`) through a full N=1024
+`verification/fullcore/run_stream.py` drives the invented RTL (the
+register-level hardware source code:
+`compact_bf_v2` + `modular_mul_kred` + `tf_rom_fold`) through a full N=1024
 NTT and INTT under iverilog. On every tested vector, the RTL `NTT(x)` equals
-the reference `DIT_NR_NTT` on the real twiddle table, and
+the reference `DIT_NR_NTT` on the real twiddle table (the precomputed
+constants the transform multiplies by), and
 `INTT(NTT(x)) == x` exactly. The issue-#7 halving fix and the 9⁻¹-scaled
 folded ROM therefore compose into a correct transform at the system level,
-not merely per butterfly.
+not merely per butterfly (the transform's small multiply-and-add step).
 
 This closes the gap the module proofs leave. fv_bf_v2 proves the butterfly
 matches the spec for every input; `run_stream.py` shows that the specced
@@ -17,7 +19,7 @@ whole transform on real gates (iverilog).
 
 Caveat: cfntt_ref's exact banked-memory schedule is not reproduced, because
 the released `fsm.v` is empty (upstream #4). A reconstructed FSM
-(`fsm_recon.v`) driving the banked datapath is included but not yet
+(control state machine, `fsm_recon.v`) driving the banked datapath is included but not yet
 cycle-accurate. It is future work and off the critical path, since the
 inventions are drop-in with identical latency. See
 `verification/fullcore/README.md`.
@@ -26,7 +28,8 @@ inventions are drop-in with identical latency. See
 
 All numbers come from `yosys` generic synthesis (`synth -flatten -noabc`),
 reproducible via `kred-butterfly/cost_report.ys` and the ROM comparison. Cell
-counts are technology-independent gate counts, not LUTs.
+counts are technology-independent gate counts, not LUTs (the FPGA's
+logic cells).
 
 | Block | reference | proposed | Δ |
 |---|---|---|---|
@@ -56,7 +59,8 @@ real 7-series primitives resolves both. Per module, flattened
 
 Reading, and why the per-FPGA numbers matter:
 
-1. DSP 3 → 1 holds on real primitives: −67% DSP per butterfly and −27% FF
+1. DSP (the FPGA's dedicated multiplier blocks) 3 → 1 holds on real
+   primitives: −67% DSP per butterfly and −27% FF (register cells)
    on the multiplier. NTT accelerators are almost always DSP-bound, since
    many parallel butterflies compete for the scarce DSP blocks. This is the
    saving that matters, and it scales ×d.
@@ -65,7 +69,8 @@ Reading, and why the per-FPGA numbers matter:
    On a LUT-bound design the trade could be neutral-to-negative; on the
    usual DSP-bound design it is a clear win. We report both directions.
 3. The ROM's −79% was generic gates, not FPGA. Mapped to primitives, the
-   ROM stays in distributed LUT-RAM (yosys does not infer BRAM for
+   ROM stays in distributed LUT-RAM (yosys does not infer BRAM — an
+   on-chip memory block — for
    1023×14 here), so `tf_rom_fold` is only −20% LUT (241 → 192), with
    fold7 adding CARRY4. The defensible ROM claim is the −50% stored bits,
    which converts to a BRAM saving only when the table is large enough to
@@ -109,7 +114,9 @@ Whole-core reading:
 
 ### Timing proxy: logic depth (open flow, no PnR needed)
 
-Fmax needs PnR, but yosys' longest-topological-path (`ltp`) gives a
+Fmax (the highest clock frequency the routed design sustains) needs PnR
+(place and route: mapping the logic onto the chip's physical fabric), but
+yosys' longest-topological-path (`ltp`) gives a
 technology-mapped logic-depth proxy that already answers the paper's two
 timing questions. Per module (post-`synth_xilinx`, LUT/carry levels):
 
@@ -136,8 +143,9 @@ The first fold7 used three chained conditional subtractions (−4q, −2q, −q)
 LTP 31. Since `7x ∈ [0, 7q)`, we replaced them with six parallel constant
 comparators that select `m·q` from precomputed multiples, followed by a
 single subtraction: LTP 31 → 26, LUT 214 → 192, CARRY4 23 → 18, still
-DSP-free. The new datapath was re-verified end-to-end: z3 `VERIFIED`, the
-shipped-ROM equivalence miter, the full-transform sim, and the mutation
+DSP-free. The new datapath was re-verified end-to-end: z3 (an automated theorem prover) `VERIFIED`, the
+shipped-ROM equivalence miter (a circuit comparing the two
+implementations output-for-output), the full-transform sim, and the mutation
 sweep all pass. A pipelined fold7 (one extra register) would remove the
 depth from the ROM read entirely at +1 latency; we keep the combinational
 version to preserve the drop-in 1-cycle ROM interface, and flag the

docs/evaluation.md

@@ -18,6 +18,10 @@ pandoc --from gfm+raw_attribute --to latex -s \
 
 python3 "$here/fix_longtables.py" "$here/paper_ieee.tex"
 
+# image paths in paper.md are relative to docs/paper/; we compile one level
+# deeper, so point them one directory further up
+sed -i 's|{\.\./assets/|{../../assets/|g' "$here/paper_ieee.tex"
+
 cd "$here"
 xelatex -interaction=nonstopmode paper_ieee.tex >build.log 2>&1 || true
 xelatex -interaction=nonstopmode paper_ieee.tex >build.log 2>&1 || true