docs: merge doc.tex, pcs.tex and ring-switching.tex into one LaTeX project

`misc/` becomes `doc/`, a single project with one PDF output (39 pages):
`doc/main.tex` inputs `preamble/`, the nine spec sections from `body/`, then
ring switching and the PCS as annexes A and B. Section text is unchanged;
only notation, redundant definitions and structure moved.

Notation is now defined once, in `preamble/macros.tex`, and every named
object has one meaning across the whole document:

- multilinear extensions are `\widetilde` everywhere, freeing the hat for the
  additive NTT's normalized subspace polynomials;
- annex B's symbols that collided with the spec are renamed through semantic
  macros, so changing a glyph is a one-line edit. Annex B opens with a table
  mapping all 31 renames back to the names WHIR/Ligerito/BCHKS25 and
  `crates/pcs` use;
- genuine unifications rather than substitutions: `m_i` becomes the stack's
  `M_i`, the batching challenge is `\lambda` on both sides, claim counts join
  the pool's `J`, and a claim is `(W, c)` throughout;
- bound and index variables stay short and shared, which the annex says.

Redundant definitions collapsed: the fields were defined three times, `eq`
and the weighted claim twice. Phi, its 64-term soundness argument and the
weight-evaluation formula lived in both ring-switching.tex and doc.tex's
appendix; they now appear once in annex A, and the flock instantiation
(packing into q_pkd, the incoming claim, the coordinate transpose) is
section 3.3, keeping the `sec:ringswitch` label. The `sec:state` label
collided and annex B's copy is now `pcs:proof`; all other labels are
preserved, so the `thm:rbr` and `thm:mca-johnson` references in
`crates/pcs` still resolve.

Three bibliographies become `doc/refs.bib` with `alphaurl`, folding the
duplicate keys for Diamond-Posen, Ligerito and WHIR, and keeping the flock
paper and the flock implementation as separate entries.

CI: `pdf.yml`, `pcs.yml` and `ring-switching.yml` become one `doc.yml` that
publishes `leanVM-b.pdf` to the existing `spec-latest` tag and fails a PR on
any undefined reference. The `pcs-latest` and `ring-switching-latest` release
tags now have nothing rebuilding them.

Verified by a clean rebuild: no undefined references or citations, no
multiply-defined labels, no overfull boxes. `cargo check --release` passes on
the three crates whose comments moved from `misc/` to `doc/`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Author: TomWambsgans

.github/workflows/pdf.yml .github/workflows/doc.yml.github/workflows/pdf.yml renamed to .github/workflows/doc.yml

@@ -1,21 +1,19 @@
-name: Spec PDF
+name: Documentation PDF
 
 on:
   push:
     branches: [ "main" ]
     paths:
-      - 'misc/doc.tex'
-      - 'misc/images/**'
-      - '.github/workflows/pdf.yml'
+      - 'doc/**'
+      - '.github/workflows/doc.yml'
   pull_request:
     paths:
-      - 'misc/doc.tex'
-      - 'misc/images/**'
-      - '.github/workflows/pdf.yml'
+      - 'doc/**'
+      - '.github/workflows/doc.yml'
   workflow_dispatch:
 
 concurrency:
-  group: pdf-${{ github.ref }}
+  group: doc-${{ github.ref }}
   cancel-in-progress: true
 
 jobs:
@@ -29,8 +27,11 @@ jobs:
       - name: Compile LaTeX
         uses: xu-cheng/latex-action@v3
         with:
-          working_directory: misc
-          root_file: doc.tex
+          working_directory: doc
+          root_file: main.tex
+      - name: Fail on an undefined reference or citation
+        run: |
+          ! grep -qE 'Reference .* undefined|Citation .* undefined|multiply defined' doc/.build/main.log
 
   build-pdf:
     if: github.event_name != 'pull_request'
@@ -42,13 +43,17 @@ jobs:
       - name: Compile LaTeX
         uses: xu-cheng/latex-action@v3
         with:
-          working_directory: misc
-          root_file: doc.tex
+          working_directory: doc
+          root_file: main.tex
+      - name: Name the artifact
+        run: cp doc/.build/main.pdf leanVM-b.pdf
       - name: Publish PDF as release asset
         uses: softprops/action-gh-release@v2
         with:
           tag_name: spec-latest
-          name: Latest spec PDF
-          body: Auto-built from `misc/doc.tex` on every push to `main`.
+          name: Latest leanVM-b PDF
+          body: |
+            Auto-built from `doc/main.tex` on every push to `main`.
+            Contains the specification, Annex A (ring switching) and Annex B (the PCS).
           make_latest: false
-          files: misc/doc.pdf
+          files: leanVM-b.pdf

.github/workflows/pcs.yml

@@ -4,7 +4,7 @@
 
 A minimal (zero-knowledge Virtual Machine, which is actually not ZK in the real sense, i.e. it's only a snark, not a zk-snark).
 
-- `misc/doc.tex` describes the machine ISA, the snark that proves it.
+- `doc/` is one LaTeX project (root `doc/main.tex`, build with `latexmk -pdf main.tex`, output in `doc/.build/`) describing the machine ISA and the snark that proves it. Sections live in `doc/body/`, ring switching and the PCS are annexes in `doc/annex/`, and every symbol is defined once in `doc/preamble/macros.tex`.
 - `crates/lean_compiler/zkDSL.md` documents the (pythonic) zkDSL (that compiles to the ISA that our VM runs, and that our snark proves).
 
 Primary goal:
@@ -78,7 +78,7 @@ The same verification algorithm is written out three times, in three languages.
 The third is worth understanding before touching the verifier. `guests/recursion.py` is not Python that runs; it is the zkDSL, which `lean_compiler` lowers to the VM's seven-opcode ISA (`XOR`, `MUL`, `SET`, `DEREF`, `JUMP`, `BLAKE3`, `PACK64X2`) over write-once memory. So every verifier step, sponge absorption, sumcheck fold, Merkle path, field inverse, becomes VM instructions that the prover then proves the execution of, which is why the guest is ~500k instructions and why its opcode mix is what the recursion benchmark reports. Two consequences:
 
 - The guest is **generic in the inner proof**: its placeholder map depends only on the inner bytecode size, so one compiled bytecode verifies inner proofs of different sizes and PCS rates (`recursion_2to1_mixed`, `recursion_generic_many`).
-- It does not verify *quite* everything in-circuit. Three claims on fixed polynomials (stacked bytecode, and flock's A0/B0) are deferred, bound to the guest's public input, and discharged natively by `RecursiveProof::verify`. Sumcheck is used to merge and further deref those 'postponed' claims in recursion, moving `n` such inner claims to a single outer one (explained in doc.tex).
+- It does not verify *quite* everything in-circuit. Three claims on fixed polynomials (stacked bytecode, and flock's A0/B0) are deferred, bound to the guest's public input, and discharged natively by `RecursiveProof::verify`. Sumcheck is used to merge and further deref those 'postponed' claims in recursion, moving `n` such inner claims to a single outer one (explained in `doc/`).
 
 `recursion_2to1` is the fast end-to-end check; `recursion_soundness_binds` is the adversarial one, tampering each hint stream in turn and requiring rejection.
 

.github/workflows/ring-switching.yml

@@ -1,11 +1,11 @@
 <h1 align="center">leanVM-b</h1>
 
 <p align="center">
-  <img src="./misc/images/banner-b.svg" alt="leanVM-b">
+  <img src="./doc/images/banner-b.svg" alt="leanVM-b">
 </p>
 
 <p align="center">
-  <a href="./misc/doc.tex"><img src="https://img.shields.io/badge/Specification-source-blue?style=for-the-badge&logo=latex&logoColor=white" alt="Specification source"></a>
+  <a href="./doc/main.tex"><img src="https://img.shields.io/badge/Specification-source-blue?style=for-the-badge&logo=latex&logoColor=white" alt="Specification source"></a>
   <a href="https://github.com/leanEthereum/leanVM-b/releases/download/spec-latest/doc.pdf"><img src="https://img.shields.io/badge/main-PDF-blue?style=for-the-badge&logo=latex&logoColor=white" alt="Latest main-branch PDF"></a>
 </p>
 

AGENTS.md

@@ -4,7 +4,7 @@ The zkDSL is a Python-syntax language that compiles to the leanVM-b ISA — seve
 instructions (`XOR`, `MUL`, `SET`, `DEREF`, `JUMP`, `BLAKE3`, `PACK64X2`) over the binary
 field GF(2^192), with write-once memory and all indices carried "in the
 exponent" as powers of a fixed generator. For the underlying VM and proving
-system, see [`misc/doc.tex`](../../misc/doc.tex).
+system, see [`doc/main.tex`](../../doc/main.tex).
 
 Source files use the `.py` extension and are **valid Python**: they import the
 [`snark_lib`](snark_lib.py) stub, which defines `GEN`, `log`, `mul_range`,

README.md

@@ -29,7 +29,7 @@
 //! end, as the recursion guest does. That is what a recursive verifier needs.
 //!
 //! The eq point is the caller's, not a fresh one — the bus's GKR point `ζ` — which
-//! is what lets the forms' sums settle the bus. Batching derived in `misc/doc.tex`
+//! is what lets the forms' sums settle the bus. Batching derived in `doc/main.tex`
 //! §sec:air. Both sides take `n = max τ_t` from the announced heights; a recursive
 //! verifier certifies that maximum with one hinted `g`-power (§recursion), so there
 //! are no rounds in which no table has joined.

crates/lean_compiler/zkDSL.md

@@ -1,4 +1,4 @@
-//! Whole-program assembly over GF(2^64) (`misc/doc.tex`): the instruction tables
+//! Whole-program assembly over GF(2^64) (`doc/main.tex`): the instruction tables
 //! sharing the state / memory / bytecode buses, bound to one field-valued
 //! commitment and verified oracle-free. Addresses, the program counter, and read
 //! counts are g-powers, so every increment is a free ×g. Machine-word arithmetic
@@ -50,7 +50,7 @@ const MAX_LOG_MEM: usize = 32;
 
 /// Each per-opcode table holds at most `2^MAX_LOG_ROWS` rows (executed
 /// instructions of that opcode). Together with `MAX_LOG_MEM` and the bytecode
-/// cap these are the instance caps from “Counts must not wrap” in `misc/doc.tex`: at `ord(g) = 2^64−1`
+/// cap these are the instance caps from “Counts must not wrap” in `doc/body/05-memory-and-bytecode-lookups.tex`: at `ord(g) = 2^64−1`
 /// the memory-soundness and count-non-wrap counting arguments are theorems only
 /// for instances whose total read-flush count stays far below `2^64`, so the
 /// verifier rejects any announcement exceeding them before running a reduction.

crates/lean_vm/src/constraints.rs

@@ -1,4 +1,4 @@
-//! leanVM-b — arithmetization of a minimal zkVM (see `misc/doc.tex`).
+//! leanVM-b — arithmetization of a minimal zkVM (see `doc/main.tex`).
 //!
 //! Machine words are `c0 + c1*y + c2*y² ∈ E = K[y]/(y³ + y + 1)`.
 //! Addresses, pc/fp, read counters, and logical indices live in

crates/lean_vm/src/cpu/mod.rs

@@ -1,4 +1,4 @@
-//! Per-instruction tables (`misc/doc.tex`, “The instruction tables”). Each opcode is one [`Table`] impl that declares,
+//! Per-instruction tables (`doc/body/06-instruction-tables.tex`). Each opcode is one [`Table`] impl that declares,
 //! in one place, its committed columns, how to fill them from the trace, its bus
 //! interactions (flushes), the read-count columns that feed the count channel,
 //! and its degree-2 constraint. Column indices here are *local* (`0..n_committed_columns`);
@@ -642,7 +642,7 @@ mod jump {
     pub const RBC: usize = 22;
     // Local witness columns (committed, never flushed): the inverse hint `w`
     // (192-bit: c⁻¹ in E) and the taken indicator `b = [c ≠ 0]` it certifies
-    // (the `JUMP` table in `misc/doc.tex`). `b` is a single K-lane (0/1).
+    // (the `JUMP` table in `doc/body/06-instruction-tables.tex`). `b` is a single K-lane (0/1).
     pub const W_LO: usize = 23;
     pub const W_HI: usize = 24;
     pub const W_TOP: usize = 25;
@@ -818,7 +818,7 @@ impl Table for Pack64x2Table {
 
 // ---- BLAKE3 ------------------------------------------------------------------
 
-/// `BLAKE3` (“BLAKE3” in `misc/doc.tex`): one standard compression. The four 128-bit message
+/// `BLAKE3` (“BLAKE3” in `doc/body/06-instruction-tables.tex`): one standard compression. The four 128-bit message
 /// chunks are addressed *independently* at `aa0, aa1, ab0, ab1`
 /// (`= fp·g^{ins[i]}`), each a single cell — no forced contiguity between
 /// chunks, so a caller hashing e.g. `(tweak, pp)` need not copy them into