diff --git a/README.md b/README.md index ff150c2..ab2c102 100644 --- a/README.md +++ b/README.md @@ -24,7 +24,9 @@ Lean 4 against models extracted from the actual Rust sources: **[`main.pdf`](main.pdf)** — fourteen chapters + interlude + three appendices, full color, built with LaTeX/TikZ from the sources in this -repo (`./build.sh`, tectonic, no root needed). No prior Lean or formal +repo (`./build.sh`, tectonic, no root needed). **Second edition, +published August 8, 2026** (129 pages; the full publication history is +printed in the book's front matter). No prior Lean or formal methods assumed; high-school algebra and a little programming suffice. 1. **Why Verify?** — the carry bug testing cannot find diff --git a/check-book.py b/check-book.py index 4df181f..86d7d42 100644 --- a/check-book.py +++ b/check-book.py @@ -69,6 +69,13 @@ def main(): readme = read(os.path.join(book, "README.md")) chdir = os.path.join(book, "chapters") + # the publication-history block: its CURRENT-edition line is bound to + # measurements below; its historical lines are frozen and exempt from + # the whole-book claim scans, so strip the span for scanning purposes + mhist = re.search(r"% BEGIN PUBHIST.*?% END PUBHIST", main_tex, re.S) + pubhist = mhist.group(0) if mhist else "" + main_scan = main_tex.replace(pubhist, "") + # ── Phase 0: source hygiene ──────────────────────────────────────────── print("=== Phase 0: source hygiene ===") @@ -128,12 +135,44 @@ def main(): bad = [l for l in txt.splitlines() if "??" in l] check(not bad, "no unresolved references ('??') in rendered PDF", bad[0][:60] if bad else "clean") - page_claims = re.findall(r"(\d{2,4}) pages", readme + main_tex) + page_claims = re.findall(r"(\d{2,4}) pages", readme + main_scan) if page_claims: for pc in page_claims: check(int(pc) == pages, f"page-count claim {pc} == built {pages}") else: - ok("no page-count claim in prose (nothing to bind)") + ok("no page-count claim outside the history block (nothing to bind)") + + # publication history: the current-edition line is a live claim + med = re.search(r"\\textbf\{(\w+) edition\} --- published " + r"([A-Za-z]+ \d+, \d{4}): (\w+)\s*\n?chapters, " + r"(\d+) pages", pubhist) + if not (pubhist and med): + fail("publication-history block with parseable current-edition line", + "missing" if not pubhist else "line not parseable") + else: + check(WORDS.get(med.group(3)) == n_ch, + "current edition's chapter count == measured", + f"{med.group(3)} vs {n_ch}") + check(int(med.group(4)) == pages, + "current edition's page count == built PDF", + f"{med.group(4)} vs {pages}") + # committed PDF must carry the current-edition line: this is what + # a GitHub visitor downloads, and it must not lag the sources + if os.path.isdir(os.path.join(book, ".git")): + blob = subprocess.run(["git", "-C", book, "show", "HEAD:main.pdf"], + capture_output=True) + tmp = os.path.join(book, ".committed-main.pdf.tmp") + with open(tmp, "wb") as fh: + fh.write(blob.stdout) + ctxt = subprocess.run(["pdftotext", tmp, "-"], + capture_output=True, text=True).stdout + os.unlink(tmp) + check(f"published {med.group(2)}" in ctxt, + "COMMITTED main.pdf carries the current-edition line " + "(the PDF a visitor downloads is not stale)", + med.group(2)) + else: + ok("committed-PDF binding skipped (no git repo here)") # ── Phase 2: internal countable claims ───────────────────────────────── print("=== Phase 2: internal countable claims ===") @@ -151,9 +190,10 @@ def main(): # stale-total scan is scoped to the front matter, where whole-book totals # live; inside a chapter, "N chapters" is a positional count checked next for stale in ("twelve chapters", "thirteen chapters"): - hits = [f for f in ("main.tex", "README.md") - if stale in read(os.path.join(book, f))] - check(not hits, f"no stale '{stale}' in front matter", ",".join(hits) or "clean") + hits = [name for name, txt in (("main.tex", main_scan), ("README.md", readme)) + if stale in txt] + check(not hits, f"no stale '{stale}' in front matter (history block exempt)", + ",".join(hits) or "clean") # any "spent N chapters" phrase inside chapter chNN counts its predecessors for cf in chapter_files: num = int(re.search(r"ch(\d\d)-", cf).group(1)) diff --git a/main.pdf b/main.pdf index ffd93b0..498ca23 100644 Binary files a/main.pdf and b/main.pdf differ diff --git a/main.tex b/main.tex index 6d851b7..f927df2 100644 --- a/main.tex +++ b/main.tex @@ -37,6 +37,39 @@ claim it makes about a proof, a proof assistant has checked.\par} \restoregeometry \pagecolor{paper}\color{ink} +% BEGIN PUBHIST ==================== publication history ===================== +% The current-edition line is machine-checked by check-book.sh: its chapter +% count and page count must match the built book, and the committed PDF must +% contain it. Historical lines are frozen and exempt from the claim checks. +\thispagestyle{empty} +\vspace*{2cm} +{\small +\noindent\textbf{Second edition} --- published August 8, 2026: fourteen +chapters, 129 pages. + +\medskip +\noindent\emph{Publication history} +\begin{itemize}[leftmargin=1.4em] +\item \textbf{First edition}, July 3, 2026 --- twelve chapters and the + Interlude; expanded the same day with the pen-and-paper program and + in-book solution pathways (53 to 106 pages). +\item July 28, 2026 --- the Attestation Protocol added as a thirteenth + chapter. +\item \textbf{Second edition}, August 8, 2026 --- full didactic overhaul + (seven moves, from a seven-reader audit); new Chapter~13, \emph{The + Second Summit} (SLH-DSA, post-quantum); the Attestation Protocol becomes + the fourteen-chapter book's single finale; \code{check-book.sh} added --- + the script that verifies every countable claim in this book, including + the line at the top of this page, against measured reality. +\end{itemize} + +\medskip +\noindent The complete revision record is the git history of +\code{github.com/saymrwulf/verifying-crypto-with-lean}. +} +\clearpage +% END PUBHIST ================================================================ + % ===================== HOW TO READ ===================== \chapter*{How to read this book} \markboth{How to read this book}{}