add intro in doc

Author: TomWambsgans

AGENTS.md

@@ -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).
 
-- `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`.
+- `doc/` is one LaTeX project (root `doc/main.tex`, build with `cd doc && latexmk -pdf main.tex`, output in the gitignored `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`. If latexmk fails oddly (a bibtex error, or a missing `main.log`) right after inputs are renamed or `refs.bib` is edited, `rm -rf doc/.build` and rerun; it has not reproduced on unchanged inputs.
 - `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:
@@ -88,6 +88,8 @@ The third is worth understanding before touching the verifier. `guests/recursion
 - **Prover and verifier derive the layout identically** from announced sizes. Changes to `placements_of`, `col_kappas` or the schema land on both sides, and `col_kappa_sources` stays in lockstep with `col_kappas`.
 - **A failed guest `assert` surfaces as a write-once memory conflict**, not an assertion message, so disassemble around the reported `pc` (`DBG_DISASM`).
 - Guests are single-file; the compiler skips `from snark_lib import *`, which exists only so editors accept the file as Python.
+- **One symbol, one meaning, across the whole document.** All notation is defined in `doc/preamble/macros.tex`; define a new macro there rather than inline, and check the letter is free first. Annex B's symbols were deliberately renamed away from the letters WHIR/Ligerito/BCHKS25 use (rate is `\rate`, not `\rho`, which is a sumcheck point) and its "Symbols" table is the map back, so reintroducing a paper's letter silently collides with the main matter.
+- **Doc labels are an API.** `crates/pcs` cites `thm:rbr` and `thm:mca-johnson` by name and several crates cite `doc/main.tex` sections, so renaming a label breaks those pointers with nothing to catch it. `doc/body/NN-*.tex` prefixes match section numbers, so inserting a section renumbers the rest.
 - **No em-dashes or en-dashes in prose**, anywhere a human reads it: docs, LaTeX, comments, commit messages. Restructure with a comma, colon, parentheses, or two sentences.
 - **Never hard-wrap prose in Markdown or LaTeX.** One paragraph is one line; let the editor wrap it. Artificial line breaks make every later edit a reflow, so diffs show rewrapped lines instead of changed words. Applies to `.md` and `.tex` alike; code blocks, tables and list items keep their own line.
 

doc/body/01-introduction.tex

@@ -0,0 +1,12 @@
+\section{Introduction}\label{sec:intro}
+
+Ethereum's consensus layer currently uses BLS signatures, its execution layer ECDSA, and its data availability layer KZG. All three are based on elliptic curves, which do not survive a quantum computer~\cite{shor}. Hash-based cryptography, both signatures and snarks (the hash-based ones are sometimes called STARKs~\cite{stark}), is a promising candidate for Ethereum's post-quantum transition:
+\begin{itemize}[itemsep=1pt,topsep=3pt]
+\item BLS $\to$ XMSS~\cite{rfc8391} (stateful signatures are far less an issue with the consensus than at the execution layer, because equivocation is already forbidden, and the slot can be used as the nonce). But XMSS dosn't have native aggregation as BLS, we need a snark to do it.
+\item ECDSA $\to$ SPHINCS+~\cite{sphincs}. Drawback: dozens of time bigger. Again, we need aggregation via a snark to mitigate signature size increase.
+\item KZG $\to$ Reed--Solomon encoding each blob, a Merkle root over the codeword, and a snark proving that the root commits to a correct encoding.
+\end{itemize}
+
+\vspace{4mm}
+
+leanVM-b is a candidate as the snark machinery required above. It's a verifiable virtual machine (commonly a zkVM, for "zero-knwoledge virtual machine", though leanVM-b is not (yet) zk). It is based on binary fields, inspired by \cite{DP26} and \cite{Flock26}, currently using BLAKE3 as hash function.