mirror of
https://github.com/saymrwulf/verifying-crypto-with-lean.git
synced 2026-07-16 18:32:02 +00:00
mrwulf
1029f0c251
The owner's requirement, now the book's explicit contract (new "ratchet
rule" box in chapter 1): every load-bearing idea is worked at least
twice - once at napkin scale (mod 13, inverses by scanning) and once at
REAL scale, the actual 77-digit Ed25519 constants printed in full with
no digits hidden and no artificial zeros; where raw size genuinely
exceeds paper (a 77-digit square root), the book says so and teaches
witness-auditing instead of pretending.
Socratic audit result: chapters 1-11 already honor the rule (verified
rung by rung - e.g. ch6 pairs the Z/12 clock with 19^-1 mod the real p;
ch7 pairs Pratt-for-97 with costing the real certificate; ch8 runs the
extracted model at the real envelope edge). The gaps were ch12's three
summit rungs, which had NO numeric examples at all. Filled:
- Group law: "running the addition law by hand - napkin curve, then the
real one". Doubling (2,4)->(10,11) mod 13 in full; then the real base
point with x1, y1 printed in 5-digit groups, the first machine step
certified as x1*y1 = q*p + u with the 77-digit witness q printed, and
the student auditing it by casting out nines AND elevens (both clocks
close: 3=3, 1=1). Lands on the real 2B coordinates.
- Scalars: the cycle felt on the napkin curve first (order 16, so
21P = 5P) before the real prime ell.
- Apex: "decompression, run twice". Encode/decode (10,11) as "(11,
even)" mod 13 - x^2 = 3/9 = 9, roots {3,10}, parity picks 10; then
the real compressed base point: all 32 bytes printed (58 66...66),
byte 31 = 0x66 sign-bit read, y_B printed in full, and the
no-shortcuts full-size hand verification 5*y_B - 4 = 4*p, both
78-digit sides printed for digit-by-digit comparison. The square
root honestly declared machine territory, with the witness-checked
certificate named.
- New paper exercise 12.4 (+pathway/solution): encode & decompress
3P = (6,10) solo - the wrong root lands on -3P, one bit doing real
cryptographic work.
Every printed constant machine-verified before typesetting (base point
on-curve, q*p+u exact, 5y-4 = 4p exact, 2B on-curve, toy order 16).
PDF rebuilt: 109 pages, zero errors. Honesty ledger records the
revision.
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 | ||