mirror of
https://github.com/saymrwulf/verifying-crypto-with-lean.git
synced 2026-07-23 19:32:40 +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> |
||
|---|---|---|
| .. | ||
| appendix-repo-tour.tex | ||
| appendix-toolkit.tex | ||
| appendix-walkthroughs.tex | ||
| ch01-why-verify.tex | ||
| ch02-meet-lean.tex | ||
| ch03-propositions-as-types.tex | ||
| ch04-tactics.tex | ||
| ch05-numbers-and-automation.tex | ||
| ch06-modular-arithmetic.tex | ||
| ch07-primality-certificates.tex | ||
| ch08-rust-to-lean.tex | ||
| ch09-denotation-bridge.tex | ||
| ch10-verifying-a-field.tex | ||
| ch11-honesty-and-axioms.tex | ||
| ch12-the-pyramid.tex | ||
| glossary.tex | ||
| interlude-by-hand.tex | ||