mirror of
https://github.com/saymrwulf/verifying-crypto-with-lean.git
synced 2026-07-19 19:01:17 +00:00
saymrwulf
5861c73c22
- pen-and-paper worked examples in all 12 chapters, using the REAL constants throughout: 2^-64 waiting-time arithmetic, headroom budgets, hand type-checking, rfl traces, full goal-state boards, the column-sum audit at 2^54, inverting 19 mod p via Euclid, the x19 fold at real weights, denoting p itself (telescope), the 16p audit (8 fails by 151), the 254+11 inversion-chain bookkeeping, the substitution test, sizing the 28-vs-1000 extraction, cofactor/torsion arithmetic, and the full Bernstein-Lange completeness derivation - CORRECTNESS FIX: ch7 asserted a false factorization of p-1; replaced with the computationally verified p-1 = 2^2 * 3 * 65147 * Q (Q 71-digit prime), witness w=2 verified for all four Pratt conditions - every chapter's exercises now followed immediately by 'Solutions and pathways' (pathway first, then answer), incl. new exercises - NEW Interlude: a complete two-clause verification done entirely by hand, then mapped line-by-line onto the compiled Lean proof - NEW appendices: A pen-and-paper toolkit (8 recipe cards + drills + answers), B guided walkthroughs of every exercise-file hole, C tour of the real repositories; plus glossary, instructor notes, 13-week plan - preamble: worked-example box, solution macros, math-safe inline code Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
211 lines
11 KiB
TeX
211 lines
11 KiB
TeX
% ============================================================================
|
||
% preamble.tex — shared style for "Verifying Cryptography with Lean 4"
|
||
% A didactic identity: warm ink on soft paper, one confident accent, and a
|
||
% small family of pedagogical boxes that each mean exactly one thing.
|
||
% ============================================================================
|
||
\usepackage[T1]{fontenc}
|
||
\usepackage[utf8]{inputenc}
|
||
\usepackage{lmodern}
|
||
\usepackage[margin=2.4cm,headsep=0.6cm]{geometry}
|
||
\usepackage{amsmath,amssymb,amsthm}
|
||
\usepackage{xcolor}
|
||
\usepackage{tikz}
|
||
\usetikzlibrary{arrows.meta,positioning,shapes.geometric,calc,fit,backgrounds,decorations.pathreplacing,shapes.misc}
|
||
\usepackage[most]{tcolorbox}
|
||
\usepackage{listings}
|
||
\usepackage{microtype}
|
||
\usepackage{enumitem}
|
||
\usepackage{fancyhdr}
|
||
\usepackage{titlesec}
|
||
\usepackage{booktabs}
|
||
\usepackage[strings]{underscore} % plain _ works in text; math subscripts unaffected
|
||
\usepackage{hyperref}
|
||
|
||
% ---- palette -------------------------------------------------------------
|
||
% Ink is a deep blue-slate; the accent is a warm coral used sparingly; a
|
||
% calm teal marks "things that are true / proven". Neutrals carry a faint
|
||
% blue bias so nothing reads as unconsidered grey.
|
||
\definecolor{ink}{HTML}{1C2430}
|
||
\definecolor{ink2}{HTML}{51607A}
|
||
\definecolor{paper}{HTML}{FBFAF7}
|
||
\definecolor{accent}{HTML}{E4572E} % coral — the one bold colour
|
||
\definecolor{accentsoft}{HTML}{FBE7DF}
|
||
\definecolor{proven}{HTML}{1E7F5C} % teal-green — proven / correct
|
||
\definecolor{provensoft}{HTML}{E1F1EA}
|
||
\definecolor{warn}{HTML}{B4690E} % amber — pitfalls
|
||
\definecolor{warnsoft}{HTML}{FBEFD8}
|
||
\definecolor{codebg}{HTML}{F3F1EC}
|
||
\definecolor{rule}{HTML}{DDE2E9}
|
||
\definecolor{kw}{HTML}{2B6CB0}
|
||
\definecolor{ty}{HTML}{6B46C1}
|
||
\definecolor{cmt}{HTML}{718096}
|
||
\definecolor{str}{HTML}{2F855A}
|
||
|
||
\hypersetup{colorlinks=true,linkcolor=accent,urlcolor=kw,citecolor=proven,
|
||
pdftitle={Verifying Cryptography with Lean 4},pdfauthor={Fable 5}}
|
||
|
||
% ---- page furniture ------------------------------------------------------
|
||
\pagecolor{paper}
|
||
\color{ink}
|
||
\pagestyle{fancy}\fancyhf{}
|
||
\renewcommand{\headrulewidth}{0pt}
|
||
\fancyfoot[C]{\small\color{ink2}\thepage}
|
||
% single header element: chapter title only (no number prefix), no collisions
|
||
\renewcommand{\chaptermark}[1]{\markboth{#1}{}}
|
||
\fancyhead[R]{\small\color{ink2}\scshape\leftmark}
|
||
|
||
\titleformat{\section}{\Large\bfseries\color{ink}}{\color{accent}\thesection}{0.7em}{}
|
||
\titleformat{\subsection}{\large\bfseries\color{ink}}{\color{accent}\thesubsection}{0.6em}{}
|
||
\setlength{\parskip}{0.55em}\setlength{\parindent}{0pt}
|
||
|
||
% ---- listings: Lean 4 and Rust ------------------------------------------
|
||
\lstdefinelanguage{Lean}{
|
||
morekeywords={theorem,lemma,def,example,by,intro,intros,exact,apply,rw,simp,
|
||
omega,decide,ring,constructor,rfl,have,let,fun,match,with,end,namespace,
|
||
open,import,structure,inductive,instance,class,where,do,return,if,then,else,
|
||
sorry,cases,induction,unfold,calc,show,from,at,using,Prop,Type,Nat,Int,Bool,True,False},
|
||
sensitive=true,
|
||
morecomment=[l]{--},
|
||
morecomment=[s]{/-}{-/},
|
||
morestring=[b]",
|
||
}
|
||
\lstdefinelanguage{RustL}{
|
||
morekeywords={fn,let,mut,const,pub,struct,impl,for,in,if,else,match,return,
|
||
u8,u16,u32,u64,u128,usize,i32,bool,self,Self,use,mod,where,unsafe,as},
|
||
sensitive=true,
|
||
morecomment=[l]{//},
|
||
morecomment=[s]{/*}{*/},
|
||
morestring=[b]",
|
||
}
|
||
\lstset{
|
||
% render the Unicode symbols real Lean code uses
|
||
literate={≠}{{$\neq$}}1 {∀}{{$\forall$}}1 {∃}{{$\exists$}}1
|
||
{→}{{$\to$}}1 {↔}{{$\leftrightarrow$}}1 {∧}{{$\wedge$}}1
|
||
{∨}{{$\vee$}}1 {¬}{{$\neg$}}1 {≤}{{$\leq$}}1 {≥}{{$\geq$}}1
|
||
{ℕ}{{$\mathbb{N}$}}1 {ℤ}{{$\mathbb{Z}$}}1 {ℓ}{{$\ell$}}1
|
||
{×}{{$\times$}}1 {∈}{{$\in$}}1 {∑}{{$\Sigma$}}1
|
||
{α}{{$\alpha$}}1 {β}{{$\beta$}}1 {⟨}{{$\langle$}}1 {⟩}{{$\rangle$}}1
|
||
{↦}{{$\mapsto$}}1 {⊢}{{$\vdash$}}1 {𝔽}{{$\mathbb{F}$}}1
|
||
{₀}{{$_0$}}1 {₁}{{$_1$}}1 {₂}{{$_2$}}1 {²}{{$^2$}}1 {⁵}{{$^5$}}1
|
||
{·}{{$\cdot$}}1 {←}{{$\leftarrow$}}1 {⟦}{{$[\![$}}1 {⟧}{{$]\!]$}}1
|
||
{∘}{{$\circ$}}1 {≡}{{$\equiv$}}1 {∣}{{$\mid$}}1 {⁻¹}{{$^{-1}$}}1,
|
||
basicstyle=\ttfamily\small\color{ink},
|
||
keywordstyle=\color{kw}\bfseries,
|
||
commentstyle=\color{cmt}\itshape,
|
||
stringstyle=\color{str},
|
||
numberstyle=\ttfamily\scriptsize\color{ink2},
|
||
backgroundcolor=\color{codebg},
|
||
frame=single, framerule=0pt, framesep=8pt,
|
||
rulecolor=\color{codebg},
|
||
xleftmargin=10pt, xrightmargin=6pt,
|
||
breaklines=true, showstringspaces=false,
|
||
columns=fullflexible, keepspaces=true,
|
||
aboveskip=1em, belowskip=1em,
|
||
}
|
||
% Inline code: plain styled text (robust in tables/footnotes, unlike lstinline).
|
||
% Also safe inside math mode (wraps itself in \text there).
|
||
% Unicode symbols in inline code are handled by the declarations below.
|
||
\newcommand{\inlinecode}[1]{\ifmmode\text{\ttfamily\small #1}\else{\ttfamily\small #1}\fi}
|
||
\newcommand{\lean}[1]{\inlinecode{#1}}
|
||
\newcommand{\rust}[1]{\inlinecode{#1}}
|
||
\newcommand{\code}[1]{\inlinecode{#1}}
|
||
\DeclareUnicodeCharacter{2192}{\ensuremath{\to}} % →
|
||
\DeclareUnicodeCharacter{2190}{\ensuremath{\leftarrow}} % ←
|
||
\DeclareUnicodeCharacter{2194}{\ensuremath{\leftrightarrow}} % ↔
|
||
\DeclareUnicodeCharacter{2200}{\ensuremath{\forall}} % ∀
|
||
\DeclareUnicodeCharacter{2203}{\ensuremath{\exists}} % ∃
|
||
\DeclareUnicodeCharacter{2227}{\ensuremath{\wedge}} % ∧
|
||
\DeclareUnicodeCharacter{2228}{\ensuremath{\vee}} % ∨
|
||
\DeclareUnicodeCharacter{00AC}{\ensuremath{\neg}} % ¬
|
||
\DeclareUnicodeCharacter{2260}{\ensuremath{\neq}} % ≠
|
||
\DeclareUnicodeCharacter{2264}{\ensuremath{\leq}} % ≤
|
||
\DeclareUnicodeCharacter{2265}{\ensuremath{\geq}} % ≥
|
||
\DeclareUnicodeCharacter{22A2}{\ensuremath{\vdash}} % ⊢
|
||
\DeclareUnicodeCharacter{00B7}{\ensuremath{\cdot}} % ·
|
||
\DeclareUnicodeCharacter{2115}{\ensuremath{\mathbb{N}}} % ℕ
|
||
\DeclareUnicodeCharacter{2124}{\ensuremath{\mathbb{Z}}} % ℤ
|
||
\DeclareUnicodeCharacter{2113}{\ensuremath{\ell}} % ℓ
|
||
\DeclareUnicodeCharacter{00D7}{\ensuremath{\times}} % ×
|
||
\DeclareUnicodeCharacter{2208}{\ensuremath{\in}} % ∈
|
||
\DeclareUnicodeCharacter{2211}{\ensuremath{\Sigma}} % ∑
|
||
\DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}} % ≡
|
||
\DeclareUnicodeCharacter{2223}{\ensuremath{\mid}} % ∣
|
||
\DeclareUnicodeCharacter{27E8}{\ensuremath{\langle}} % ⟨
|
||
\DeclareUnicodeCharacter{27E9}{\ensuremath{\rangle}} % ⟩
|
||
\DeclareUnicodeCharacter{1D53D}{\ensuremath{\mathbb{F}}} % 𝔽
|
||
\DeclareUnicodeCharacter{2080}{\ensuremath{{}_0}} % ₀
|
||
\DeclareUnicodeCharacter{2081}{\ensuremath{{}_1}} % ₁
|
||
\DeclareUnicodeCharacter{2082}{\ensuremath{{}_2}} % ₂
|
||
\DeclareUnicodeCharacter{00B2}{\ensuremath{{}^2}} % ²
|
||
\DeclareUnicodeCharacter{2075}{\ensuremath{{}^5}} % ⁵
|
||
\DeclareUnicodeCharacter{2713}{\ensuremath{\checkmark}} % ✓
|
||
\DeclareUnicodeCharacter{2717}{\ensuremath{\times}} % ✗
|
||
\DeclareUnicodeCharacter{207B}{\ensuremath{{}^{-}}} % ⁻
|
||
\DeclareUnicodeCharacter{00B9}{\ensuremath{{}^{1}}} % ¹
|
||
\DeclareUnicodeCharacter{00B3}{\ensuremath{{}^{3}}} % ³
|
||
\DeclareUnicodeCharacter{2070}{\ensuremath{{}^{0}}} % ⁰
|
||
\DeclareUnicodeCharacter{2074}{\ensuremath{{}^{4}}} % ⁴
|
||
\DeclareUnicodeCharacter{2076}{\ensuremath{{}^{6}}} % ⁶
|
||
|
||
% ---- pedagogical boxes: each means ONE thing ----------------------------
|
||
% BIG IDEA — the load-bearing concept of a section.
|
||
\newtcolorbox{bigidea}[1][]{enhanced,breakable,colback=accentsoft,
|
||
colframe=accent,boxrule=0.4pt,arc=3pt,left=10pt,right=10pt,top=8pt,bottom=8pt,
|
||
fonttitle=\bfseries\color{paper},coltitle=paper,title={\faLightbulb\ The big idea},#1}
|
||
% TRY IT — a hands-on invitation to run something.
|
||
\newtcolorbox{tryit}[1][]{enhanced,breakable,colback=codebg,colframe=ink2,
|
||
boxrule=0.4pt,arc=3pt,left=10pt,right=10pt,top=8pt,bottom=8pt,
|
||
fonttitle=\bfseries\color{paper},coltitle=paper,title={\faTerminal\ Try it yourself},#1}
|
||
% PITFALL — a trap, with its tell.
|
||
\newtcolorbox{pitfall}[1][]{enhanced,breakable,colback=warnsoft,colframe=warn,
|
||
boxrule=0.4pt,arc=3pt,left=10pt,right=10pt,top=8pt,bottom=8pt,
|
||
fonttitle=\bfseries\color{paper},coltitle=paper,title={\faExclamationTriangle\ Pitfall},#1}
|
||
% AHA — an intuition that clicks.
|
||
\newtcolorbox{aha}[1][]{enhanced,breakable,colback=provensoft,colframe=proven,
|
||
boxrule=0.4pt,arc=3pt,left=10pt,right=10pt,top=8pt,bottom=8pt,
|
||
fonttitle=\bfseries\color{paper},coltitle=paper,title={\faStar\ Aha},#1}
|
||
% CHECKPOINT — end-of-chapter self-check.
|
||
\newtcolorbox{checkpoint}[1][]{enhanced,breakable,colback=white,colframe=ink,
|
||
boxrule=0.6pt,arc=3pt,left=10pt,right=10pt,top=8pt,bottom=8pt,
|
||
fonttitle=\bfseries\color{paper},coltitle=paper,title={\faFlagCheckered\ Checkpoint},#1}
|
||
|
||
% Poor-man's icons (fontawesome may be absent): draw tiny glyphs with text.
|
||
\providecommand{\faLightbulb}{\raisebox{-1pt}{\small$\ast$}}
|
||
\providecommand{\faTerminal}{\raisebox{-1pt}{\small\ttfamily>\_}}
|
||
\providecommand{\faExclamationTriangle}{\raisebox{-1pt}{\small$\triangle$}}
|
||
\providecommand{\faStar}{\raisebox{-1pt}{\small$\star$}}
|
||
\providecommand{\faFlagCheckered}{\raisebox{-1pt}{\small$\bowtie$}}
|
||
|
||
% ---- math shortcuts the whole book uses ---------------------------------
|
||
\newcommand{\F}{\mathbb{F}}
|
||
\newcommand{\Z}{\mathbb{Z}}
|
||
\newcommand{\N}{\mathbb{N}}
|
||
\newcommand{\Fp}{\mathbb{F}_p}
|
||
\newcommand{\Zmod}[1]{\mathbb{Z}/#1\mathbb{Z}}
|
||
% double-bracket "denotation" delimiters without stmaryrd
|
||
\newcommand{\denote}[1]{\ensuremath{[\mkern-3.3mu[ #1 ]\mkern-3.3mu]}}
|
||
|
||
% WORKED EXAMPLE — pen and paper, with the real numbers.
|
||
% Distinct look: white page, thick left margin rule like a notebook.
|
||
\newtcolorbox{worked}[1]{enhanced,breakable,colback=white,colframe=ink2,
|
||
boxrule=0.4pt,leftrule=2.6pt,arc=1pt,left=10pt,right=10pt,top=8pt,bottom=8pt,
|
||
colbacktitle=codebg,coltitle=ink,
|
||
fonttitle=\bfseries,title={\pennib\ Pen and paper: #1}}
|
||
\providecommand{\pennib}{\raisebox{-1pt}{\small$\angle$}}
|
||
|
||
% exercises
|
||
\newcounter{exc}[section]
|
||
\newcommand{\exercise}[1]{\refstepcounter{exc}\smallskip\noindent%
|
||
{\bfseries\color{accent}Exercise \thechapter.\theexc.}\ #1\smallskip}
|
||
|
||
% solutions — immediately after each chapter's exercises.
|
||
% Every solution leads with the PATHWAY (how to find it), then the answer.
|
||
\newcommand{\solhead}[1]{\medskip\noindent%
|
||
{\bfseries\color{proven}Solution #1.}\ }
|
||
\newcommand{\pathway}{\par\smallskip\noindent{\itshape\color{ink2}Pathway.}\ }
|
||
\newcommand{\answer}{\par\smallskip\noindent{\itshape\color{ink2}Answer.}\ }
|
||
\newcommand{\solutionsintro}{\noindent\begingroup\small\color{ink2}%
|
||
Attempt every exercise before reading on --- a pathway teaches
|
||
ten times as much after you have been genuinely stuck. Each solution
|
||
below starts with the \emph{pathway} (how you find the answer) and only
|
||
then the answer itself.\endgroup\par\medskip}
|