From 311f60d4d0fbd7be93da8c262bd0c2f59418fc53 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 8 Aug 2026 14:16:30 +0200 Subject: [PATCH] =?UTF-8?q?move=207:=20the=20book's=20button=20=E2=80=94?= =?UTF-8?q?=20check-book.sh=20+=20check-book.py?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The only source of 'ALL GREEN' for this repository. Rebuilds the PDF, then verifies 93 countable claims printed in the book against reality measured at run time: - source hygiene: inputs<->files both directions, contiguous ch01..ch14, every chapter (and the interlude) ends on its checkpoint, per-chapter exercise count == solution count with hand-typed numbering N.1..N.k - built PDF: >=100 pages, zero unresolved references, any page-count claim in prose must equal pdfinfo - internal congruence: chapter-count words in README/ch01 vs measured N ('spent twelve chapters' in ch13 is checked as a positional count, not grepped as stale — the spelling-vs-property lesson, applied to the checker itself); week-plan heading == max table row; the discussion-exercise roster parsed from prose == measured set; the SLH-DSA arithmetic recomputed from scratch (digest split 21/7/2, sig 7856, fixed 254, per-layer max 510 by brute force, worst 3824, checksum digit examples) and each value required present in ch13 - cross-repo congruence: 19 leaves derived by property (six-digit filenames + index fields — the entries/ glob counts 25); every nineteen/19 claim in prose parsed and compared; leaves 13-16 subjects + 44 certs; leaves 12/17 = 61; leaves 0-11 = 16; leaf 18 = 11 certs, apex cone kernel-3+5 oracles, ht cone f,h,t_l, four kernel-3-only plumbing certs, all cones exact; first dual-signed head at size 14; final head size == leaf count; ch13 parameter card == the const-generic arguments parsed out of the extracted Funs.lean; ch07's 71-digit Q == P25519.lean digit for digit Fails closed: a missing sibling repo is a FAILURE, not a skip; BOOK_LOCAL_ONLY=1 skips cross-repo loudly and never prints ALL GREEN. --selftest mutates copies of the sources seven ways (count drift, deleted solution, one Q digit, leaf-count drift, arithmetic drift, stray box after a checkpoint, plan/heading divergence) and requires each to be caught BY ITS OWN CHECK, plus an unmutated control that must pass. Full run: ALL GREEN (93 checks). Selftest: 8/8. Co-Authored-By: Claude Opus 4.8 --- README.md | 24 ++++ check-book.py | 372 ++++++++++++++++++++++++++++++++++++++++++++++++++ check-book.sh | 111 +++++++++++++++ main.pdf | Bin 696668 -> 696669 bytes 4 files changed, 507 insertions(+) create mode 100644 check-book.py create mode 100755 check-book.sh diff --git a/README.md b/README.md index a97858e..ff150c2 100644 --- a/README.md +++ b/README.md @@ -87,6 +87,30 @@ lake build Solutions # compiles all solution files as a check Chapters 2–4 need no Mathlib at all — you can start them with any Lean 4 install while the cache downloads. +## The button + +Like every repository in this estate, the book has one command that earns +its claims — and it is the only source of the words "ALL GREEN" here: + +```bash +./check-book.sh +``` + +It rebuilds the PDF from the committed sources and then verifies ~90 +countable claims printed in the book against reality measured at run +time: chapter and week-plan counts, exercise↔solution pairing per chapter, +every chapter ending on its checkpoint, the recomputed SLH-DSA arithmetic +(digest split, signature size, the 3,824-call worst case), the +transparency log's 19 leaves and per-leaf certificate counts, leaf 18's +axiom cones, the first dual-signed head at size 14, the extracted +SLH-DSA-SHA2-128s parameter card, and chapter 7's 71-digit Q — digit for +digit against `P25519.lean`. Numbers are parsed out of the prose and +compared to measurements, so editing either side alone turns the button +red. Cross-repo checks need the sibling estate repos checked out next to +this one (`BOOK_LOCAL_ONLY=1` skips them, loudly, and never prints ALL +GREEN). `./check-book.sh --selftest` mutates copies of the sources seven +ways and proves each mutation is caught by its own check. + ## Building the book The repo's own recipe (tectonic, user-space, no root — installs itself on diff --git a/check-book.py b/check-book.py new file mode 100644 index 0000000..4df181f --- /dev/null +++ b/check-book.py @@ -0,0 +1,372 @@ +#!/usr/bin/env python3 +"""check-book.py — the measured half of the book's button (see check-book.sh). + +Every check compares a claim PRINTED IN THE BOOK against a value MEASURED +from the sources, the built PDF, or the sibling repositories at the moment +it runs. No expected value is carried in this file when it can be derived; +where the book's prose states a number, the number is parsed OUT OF THE +PROSE and compared against the measurement — so editing either side alone +turns the button red. + +Populations are derived by property, never by glob or label (the log's +entries/ directory contains convenience copies; leaves are the files whose +names are six digits AND whose index field matches their position). + +Exit 0 only if every applicable check passed. A check that could not +measure (missing sibling repo without BOOK_LOCAL_ONLY=1) is a FAILURE, +not a skip: a gate that read nothing must not look like a clean gate. +""" + +import json +import os +import re +import subprocess +import sys + +FAILS = [] +PASSES = [] + + +def ok(label, detail=""): + PASSES.append(label) + print(f" ok {label}" + (f" [{detail}]" if detail else "")) + + +def fail(label, detail=""): + FAILS.append(label) + print(f" FAIL {label}" + (f" [{detail}]" if detail else "")) + + +def check(cond, label, detail=""): + (ok if cond else fail)(label, detail) + + +def read(path): + with open(path, "r", errors="replace") as fh: + return fh.read() + + +WORDS = { + "one": 1, "two": 2, "three": 3, "four": 4, "five": 5, "six": 6, + "seven": 7, "eight": 8, "nine": 9, "ten": 10, "eleven": 11, + "twelve": 12, "thirteen": 13, "fourteen": 14, "fifteen": 15, + "sixteen": 16, "seventeen": 17, "eighteen": 18, "nineteen": 19, + "twenty": 20, "forty-four": 44, "sixty-one": 61, +} + + +def main(): + book = os.path.abspath(sys.argv[1] if len(sys.argv) > 1 else ".") + no_pdf = os.environ.get("SKIP_BUILD") == "1" + local_only = os.environ.get("BOOK_LOCAL_ONLY") == "1" + estate = os.environ.get("ESTATE_ROOT", os.path.dirname(book)) + ltl = os.environ.get("LTL_DIR", os.path.join(estate, "lean-transparency-log")) + fips = os.environ.get("FIPS205_DIR", os.path.join(estate, "fips205-slhdsa-verified")) + p25519 = os.environ.get("P25519_FILE", os.path.join( + estate, "dalek-ed25519-verified", "verification", "Proofs", "P25519.lean")) + + main_tex = read(os.path.join(book, "main.tex")) + readme = read(os.path.join(book, "README.md")) + chdir = os.path.join(book, "chapters") + + # ── Phase 0: source hygiene ──────────────────────────────────────────── + print("=== Phase 0: source hygiene ===") + + inputs = re.findall(r"\\input\{(chapters/[^}]+)\}", main_tex) + missing = [i for i in inputs if not os.path.exists(os.path.join(book, i + ".tex"))] + check(not missing, "every \\input'd chapter file exists", + ",".join(missing) or f"{len(inputs)} inputs") + on_disk = {f"chapters/{f[:-4]}" for f in os.listdir(chdir) if f.endswith(".tex")} + orphans = sorted(on_disk - set(inputs)) + check(not orphans, "no orphan .tex under chapters/", ",".join(orphans) or "none") + + chapter_files = [i for i in inputs if re.search(r"chapters/ch\d\d-", i)] + nums = [int(re.search(r"ch(\d\d)-", c).group(1)) for c in chapter_files] + n_ch = len(chapter_files) + check(nums == list(range(1, n_ch + 1)) and n_ch > 0, + "chapter files contiguous ch01..chNN in input order", f"N={n_ch}") + + for cf in chapter_files + ["chapters/interlude-by-hand"]: + src = read(os.path.join(book, cf + ".tex")) + envs = re.findall(r"\\end\{([a-z]+)\}", src) + check(envs and envs[-1] == "checkpoint", + f"{cf.split('/')[-1]}: last environment is checkpoint", + envs[-1] if envs else "no environments") + + for cf in chapter_files: + num = int(re.search(r"ch(\d\d)-", cf).group(1)) + src = read(os.path.join(book, cf + ".tex")) + n_ex = len(re.findall(r"\\exercise\{", src)) + sols = re.findall(r"\\solhead\{(\d+)\.(\d+)\}", src) + n_sol = len(sols) + label = f"ch{num:02d}: exercises == solutions" + if n_ex == 0 and n_sol == 0: + ok(label, "none (allowed)") + continue + good = (n_ex == n_sol + and all(int(a) == num for a, _ in sols) + and [int(b) for _, b in sols] == list(range(1, n_sol + 1))) + check(good, label, f"{n_ex} exercises, solheads {[a+'.'+b for a, b in sols]}") + + isrc = read(os.path.join(book, "chapters/interlude-by-hand.tex")) + i_ex = len(re.findall(r"Exercise I\.\d", isrc)) + i_sol = re.findall(r"\\solhead\{I\.(\d+)\}", isrc) + check(i_ex == len(i_sol) and [int(x) for x in i_sol] == list(range(1, len(i_sol) + 1)), + "interlude: exercises == solutions", f"{i_ex} vs {len(i_sol)}") + + # ── Phase 1 leftovers: claims about the built PDF ────────────────────── + print("=== Phase 1b: built-PDF claims ===") + if no_pdf: + print(" (skipped: SKIP_BUILD=1 — build phase runs in check-book.sh)") + else: + pdf = os.path.join(book, "main.pdf") + info = subprocess.run(["pdfinfo", pdf], capture_output=True, text=True).stdout + pages = int(re.search(r"Pages:\s+(\d+)", info).group(1)) + check(pages >= 100, "PDF built and non-trivial", f"{pages} pages") + txt = subprocess.run(["pdftotext", pdf, "-"], + capture_output=True, text=True).stdout + 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) + 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)") + + # ── Phase 2: internal countable claims ───────────────────────────────── + print("=== Phase 2: internal countable claims ===") + + m = re.search(r"(\w+(?:-\w+)?) chapters", readme) + check(m and WORDS.get(m.group(1)) == n_ch, + f"README chapter count == {n_ch}", m.group(0) if m else "no claim found") + + ch01 = read(os.path.join(book, "chapters/ch01-why-verify.tex")) + m = re.search(r"the next (\w+)\s*\nchapters|the next (\w+) chapters", ch01) + word = (m.group(1) or m.group(2)) if m else None + check(word is not None and WORDS.get(word) == n_ch - 1, + f"ch01 'the next N chapters' == {n_ch - 1}", word or "claim not found") + + # 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") + # 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)) + for word in re.findall(r"spent (\w+) chapters", + read(os.path.join(book, cf + ".tex"))): + check(WORDS.get(word) == num - 1, + f"ch{num:02d} 'spent {word} chapters' == its {num - 1} predecessors") + + m = re.search(r"A (\w+)-week plan", main_tex) + plan_word = WORDS.get(m.group(1)) if m else None + weeks = [int(x) for x in re.findall(r"^(\d+)\s+&", main_tex, re.M)] + ranges = [int(b) for _, b in re.findall(r"^(\d+)--(\d+)\s+&", main_tex, re.M)] + max_week = max(weeks + ranges) if (weeks or ranges) else 0 + check(plan_word == max_week and plan_word is not None, + "week-plan heading == max week row", f"{plan_word} vs {max_week}") + check(f"{m.group(1)}-week" in main_tex.replace("A " + m.group(1), "", 1), + "instructors paragraph agrees with plan heading") + + m = re.search(r"Chapters ([\d, ]+ and \d+) carry one", main_tex) + if not m: + fail("discussion-exercise roster claim parseable", "pattern not found") + else: + claimed = set(int(x) for x in re.findall(r"\d+", m.group(1))) + measured = set() + for cf in chapter_files: + num = int(re.search(r"ch(\d\d)-", cf).group(1)) + src = read(os.path.join(book, cf + ".tex")) + if re.search(r"\\exercise\{\(Discussion\)", src): + measured.add(num) + check(claimed == measured, "discussion-exercise roster == measured", + f"claimed {sorted(claimed)}, measured {sorted(measured)}") + + ch13 = read(os.path.join(book, "chapters/ch13-second-summit.tex")) + n, h, d, hp, a, k, w, ln2, m_dig = 16, 63, 7, 9, 12, 14, 16, 3, 30 + length = 2 * n + ln2 + split = ((k * a + 7) // 8, (h - h // d + 7) // 8, (h + 8 * d - 1) // (8 * d)) + check(sum(split) == m_dig and split == (21, 7, 2), "digest split recomputes", + str(split)) + sig_bytes = n * (1 + k * (1 + a) + d * (length + hp)) + check(sig_bytes == 7856, "signature size recomputes", str(sig_bytes)) + fixed = k * a + d * hp + d + 1 + 1 + k # H paths + T's + Hmsg + FORS leaves + best = 0 + for csum in range(0, 32 * (w - 1) + 1): + sh = csum << 4 + digs = [(sh >> 12) & 0xF, (sh >> 8) & 0xF, (sh >> 4) & 0xF] + best = max(best, csum + sum((w - 1) - x for x in digs)) + worst = fixed + d * best + check(fixed == 254 and best == 510 and worst == 3824, + "oracle pricing recomputes (fixed/per-layer-max/worst)", + f"{fixed}/{best}/{worst}") + + def see_saw(csum): + sh = csum << 4 + return ((sh >> 12) & 0xF, (sh >> 8) & 0xF, (sh >> 4) & 0xF) + check(see_saw(480) == (1, 14, 0) and see_saw(479) == (1, 13, 15) + and see_saw(256) == (1, 0, 0), "checksum worked examples recompute") + + for token, why in [("7{,}856", "signature size"), ("254", "fixed oracle calls"), + ("510", "per-layer max"), ("3{,}824", "worst total"), + ("(1, 14, 0)", "csum 480 digits"), + ("(1, 13, 15)", "csum 479 digits"), + ("57{,}344", "FORS forest"), ("231", "H count"), + ("$21 + 7 + 2 = 30$", "digest split")]: + check(token in ch13, f"ch13 prints {why}", token) + check(len(str(2**255 - 19)) == 77, "'77-digit prime' recomputes") + + # ── Phase 3: cross-repo congruence ───────────────────────────────────── + print("=== Phase 3: cross-repo congruence ===") + if local_only: + print(" (SKIPPED: BOOK_LOCAL_ONLY=1 — cross-repo claims NOT verified)") + else: + # the log: leaves by property, not by glob + entdir = os.path.join(ltl, "entries") + if not os.path.isdir(entdir): + fail("lean-transparency-log present", entdir) + else: + leaf_files = sorted(f for f in os.listdir(entdir) + if re.fullmatch(r"\d{6}\.json", f)) + leaves = [json.load(open(os.path.join(entdir, f))) for f in leaf_files] + idx_ok = all(lf["index"] == i for i, lf in enumerate(leaves)) + n_leaves = len(leaves) + check(idx_ok, "leaf indexes contiguous and match filenames", + f"{n_leaves} leaves") + + for where, src, pat in [ + ("title page '19 entries'", main_tex, r"(\d+) entries and counting"), + ("preface 'nineteen pieces'", main_tex, r"lists (\w+)\s*\npieces|lists (\w+) pieces"), + ("ch01 tryit '19 entries'", ch01, r"(\d+) entries, each one"), + ("ch14 'nineteen leaves'", + read(os.path.join(book, "chapters/ch14-attestation-protocol.tex")), + r"log's (\w+) leaves")]: + mm = re.search(pat, src) + val = None + if mm: + g = next(g for g in mm.groups() if g) + val = int(g) if g.isdigit() else WORDS.get(g) + check(val == n_leaves, f"{where} == measured {n_leaves}", str(val)) + + def certs(i): + return leaves[i]["leaf"]["attestation"]["certificates"] + + def comp(i): + return leaves[i]["leaf"]["attestation"]["subject"]["component"] + + ed = {"dalek-ed25519-verified", "anza-ed25519-verified", + "risc0-ed25519-verified", "betrusted-ed25519-verified"} + check({comp(i) for i in (13, 14, 15, 16)} == ed, + "leaves 13-16 subjects are the four ed25519 forks") + check(all(len(certs(i)) == 44 for i in (13, 14, 15, 16)), + "'forty-four certificates each' == measured", + str([len(certs(i)) for i in (13, 14, 15, 16)])) + check(27 + 13 + 4 == 44, "27 main + 13 scalar + 4 apex == 44") + check(comp(17) == "ltl-accumulator-verified" + and len(certs(17)) == 61 and len(certs(12)) == 61, + "'sixty-one' accumulator certificates == measured (leaves 12, 17)") + check(all(len(certs(i)) == 16 for i in range(0, 12)), + "'sixteen' early-leaf certificates == measured (leaves 0-11)") + + s18 = leaves[18]["leaf"]["attestation"] + check(s18["subject"]["component"] == "fips205-slhdsa-verified" + and s18["subject"]["kind"] == "slh_dsa", + "leaf 18 subject is fips205-slhdsa-verified / slh_dsa") + check(len(certs(18)) == 11 and "eleven certificates" in ch13, + "'eleven certificates' == measured", str(len(certs(18)))) + by_name = {c["name"]: c for c in certs(18)} + for want in ("fips205.chain_free_loop_eq", "fips205.xmss_loop_eq", + "fips205.ht_loop_eq", "fips205.wots_csum_loop_eq", + "fips205.slh_verify_128s_accepts_iff"): + check(want in by_name, f"leaf 18 carries {want}") + kernel3 = {"propext", "Classical.choice", "Quot.sound"} + apex = set(by_name["fips205.slh_verify_128s_accepts_iff"]["observed_axioms"]) + oracles = {f"verify_mono.oracle.{x}" + for x in ("f", "h", "h_msg", "t_l", "t_len")} + check(apex == kernel3 | oracles, "apex cone == kernel-3 + five oracles") + ht = set(by_name["fips205.ht_loop_eq"]["observed_axioms"]) + check(ht == kernel3 | {"verify_mono.oracle.f", "verify_mono.oracle.h", + "verify_mono.oracle.t_l"}, + "ht cone is f,h,t_l (the book's table row, by property not name)") + plumb = sum(1 for c in certs(18) if set(c["observed_axioms"]) == kernel3) + check(plumb == 4, "four kernel-3-only plumbing certificates", str(plumb)) + check(all(c["status"] == "proven" and c["axiom_status"] == "clean" + and set(c["observed_axioms"]) == set(c["expected_axioms"]) + for c in certs(18)), "leaf 18: all proven, clean, cones exact") + + heads = [json.loads(l) for l in + open(os.path.join(ltl, "sth-history.jsonl")) if l.strip()] + dual = [hd["tree_size"] for hd in heads + if hd["signatures"].get("slh_dsa", {}).get("status") == "signed"] + check(dual and min(dual) == 14, + "'since tree 14' dual-signed heads == measured", + f"first dual head size {min(dual) if dual else None}") + check(heads[-1]["tree_size"] == n_leaves, + "final head size == leaf count") + + # fips205 parameter card + funs = os.path.join(fips, "verification", "gen", "SlhVerify", "Funs.lean") + if not os.path.exists(funs): + fail("fips205-slhdsa-verified present", funs) + else: + fsrc = read(funs) + mm = re.search( + r"def verify_mono\.slh_verify_128s.*?types\.SlhDsaSig " + r"(\d+)#usize (\d+)#usize (\d+)#usize (\d+)#usize (\d+)#usize " + r"(\d+)#usize.*?slh_verify_internal_free (\d+)#usize (\d+)#usize", + fsrc, re.S) + if not mm: + fail("fips205 entry-point parameters parseable") + else: + A, D, HP, K, LEN, N = (int(mm.group(i)) for i in range(1, 7)) + H, M = int(mm.group(7)), int(mm.group(8)) + W = int(re.search(r"def W : Std\.U32 := (\d+)#u32", fsrc).group(1)) + repo = {"a": A, "d": D, "h'": HP, "k": K, "len": LEN, + "n": N, "h": H, "m": M, "w": W} + card = {"a": a, "d": d, "h'": hp, "k": k, "len": length, + "n": n, "h": h, "m": m_dig, "w": w} + check(repo == card, "ch13 parameter card == extracted entry point", + str(repo)) + for sym, val in card.items(): + tok = f"{sym} = {val}" + check(tok in ch13 or f"= {val}" in ch13, + f"ch13 prints {sym} = {val}") + + # the 71-digit Q, digit for digit + if not os.path.exists(p25519): + fail("P25519.lean present for Q comparison", p25519) + else: + psrc = read(p25519) + mq = re.search(r"theorem prime_(\d{60,})", psrc) + ch07 = read(os.path.join(book, "chapters/ch07-primality-certificates.tex")) + mb = re.search(r"Q = ([0-9\\a-z{} ]+?),\s*\n?\\\]", ch07, re.S) + q_repo = mq.group(1) if mq else None + q_book = re.sub(r"\D", "", mb.group(1)) if mb else None + check(q_repo is not None and q_book == q_repo, + "ch07's printed Q == repository's Q, digit for digit", + f"book {len(q_book or '')} digits, repo {len(q_repo or '')} digits") + check(q_repo is not None and len(q_repo) == 71 and "71-digit" in ch07, + "'71-digit' claim recomputes") + + # ── verdict ──────────────────────────────────────────────────────────── + print() + total = len(PASSES) + len(FAILS) + if FAILS: + print(f"RED: {len(FAILS)} of {total} claims diverge from measured reality:") + for f in FAILS: + print(f" - {f}") + sys.exit(1) + if local_only: + print(f"LOCAL CHECKS GREEN ({total} checks) — cross-repo claims NOT " + f"verified (BOOK_LOCAL_ONLY=1). This is not ALL GREEN.") + sys.exit(0) + print(f"ALL CLAIM CHECKS GREEN ({total} checks)") + sys.exit(0) + + +if __name__ == "__main__": + main() diff --git a/check-book.sh b/check-book.sh new file mode 100755 index 0000000..6c7de81 --- /dev/null +++ b/check-book.sh @@ -0,0 +1,111 @@ +#!/usr/bin/env bash +# check-book.sh — THE button for verifying-crypto-with-lean. +# +# This script is the only source of the words "ALL GREEN" for this +# repository. It rebuilds the book from the committed sources and then +# verifies that every countable claim printed in the book matches reality +# measured at run time: chapter counts, the week plan, exercise/solution +# pairing, the recomputed SLH-DSA arithmetic, the transparency log's leaf +# and certificate counts, the first dual-signed head, the extracted +# parameter card, and the 71-digit Q — digit for digit. +# +# Phases +# 0 source hygiene (check-book.py) +# 1 build (tectonic via build.sh; fails on TeX errors) +# 1b built-PDF claims (pages, unresolved refs, page-count claims) +# 2 internal congruence (counts and arithmetic inside the book) +# 3 cross-repo congruence (log + fips205 + P25519 siblings) +# +# Environment +# BOOK_LOCAL_ONLY=1 skip phase 3; verdict is downgraded, never ALL GREEN +# ESTATE_ROOT parent dir of the sibling repos (default: ../) +# LTL_DIR / FIPS205_DIR / P25519_FILE override individual siblings +# +# Modes +# ./check-book.sh full run +# ./check-book.sh --selftest adversarial self-test: mutates copies of the +# sources and asserts the button turns RED +set -euo pipefail +cd "$(dirname "$0")" +HERE="$(pwd)" + +selftest() { + echo "=== SELFTEST: the button must go red for the right reasons ===" + command -v python3 >/dev/null || { echo "python3 required"; exit 1; } + # the mutated copy keeps the REAL sibling repos: only the book is mutated, + # so a red verdict proves the mutation was caught, not that a repo was lost + local ESTATE; ESTATE="${ESTATE_ROOT:-$(dirname "$HERE")}" + local tmp out pass=0 fail=0 + run_copy() { + tmp="$(mktemp -d)"; mkdir -p "$tmp/chapters" + cp main.tex README.md "$tmp/"; cp chapters/*.tex "$tmp/chapters/" + } + run_mutated() { # $1 description, $2 mutation cmd, $3 expected FAIL substring + run_copy + ( cd "$tmp" && eval "$2" ) + out="$(SKIP_BUILD=1 ESTATE_ROOT="$ESTATE" python3 "$HERE/check-book.py" "$tmp" 2>&1)" \ + && { echo " FAIL mutation NOT caught: $1"; fail=$((fail+1)); rm -rf "$tmp"; return; } + if echo "$out" | grep -q "FAIL.*$3"; then + echo " ok caught for the right reason: $1"; pass=$((pass+1)) + else + echo " FAIL red, but not on the expected check ('$3'): $1"; fail=$((fail+1)) + echo "$out" | grep " FAIL" | head -3 + fi + rm -rf "$tmp" + } + # control: the unmutated copy must pass (proves the harness can go green) + run_copy + if SKIP_BUILD=1 ESTATE_ROOT="$ESTATE" python3 "$HERE/check-book.py" "$tmp" >/dev/null 2>&1; then + echo " ok control: unmutated copy passes"; pass=$((pass+1)) + else + echo " FAIL control: unmutated copy should pass but is red"; fail=$((fail+1)) + SKIP_BUILD=1 ESTATE_ROOT="$ESTATE" python3 "$HERE/check-book.py" "$tmp" | grep FAIL || true + fi + rm -rf "$tmp" + + run_mutated "chapter-count claim drifts (fourteen -> thirteen)" \ + "sed -i 's/fourteen chapters/thirteen chapters/' README.md" \ + "README chapter count" + run_mutated "a solution deleted (ch13 solhead 13.6 dropped)" \ + "sed -i 's/\\\\solhead{13.6}/% gone/' chapters/ch13-second-summit.tex" \ + "ch13: exercises == solutions" + run_mutated "one digit of the 71-digit Q changed in ch07" \ + "sed -i 's/740582127325613583022312264370627886761/740582127325613583022312264370627886762/' chapters/ch07-primality-certificates.tex" \ + "printed Q == repository" + run_mutated "leaf-count claim drifts (nineteen leaves -> twenty)" \ + "sed -i \"s/log's nineteen leaves/log's twenty leaves/\" chapters/ch14-attestation-protocol.tex" \ + "ch14 'nineteen leaves'" + run_mutated "worst-case arithmetic drifts (3,824 -> 3,689)" \ + "sed -i 's/3{,}824/3{,}689/' chapters/ch13-second-summit.tex" \ + "ch13 prints worst total" + run_mutated "a chapter stops ending on its checkpoint" \ + "printf '\n\\\\begin{aha}\nstray box after the checkpoint\n\\\\end{aha}\n' >> chapters/ch05-numbers-and-automation.tex" \ + "ch05.*last environment is checkpoint" + run_mutated "week plan and heading diverge (heading says fifteen)" \ + "sed -i 's/A fourteen-week plan/A fifteen-week plan/' main.tex" \ + "week-plan heading" + + echo + if [ "$fail" -gt 0 ]; then + echo "SELFTEST RED: $fail defect(s) in the button itself"; exit 1 + fi + echo "SELFTEST GREEN: $pass/$pass (control + 7 mutations, each caught on its own check)" + exit 0 +} + +[ "${1:-}" = "--selftest" ] && selftest + +echo "=== Phase 1: build ===" +./build.sh +command -v pdfinfo >/dev/null && command -v pdftotext >/dev/null || { + echo "FAIL: poppler-utils (pdfinfo/pdftotext) required"; exit 1; } + +python3 "$HERE/check-book.py" "$HERE" + +echo +if [ "${BOOK_LOCAL_ONLY:-0}" = "1" ]; then + echo "VERDICT: build green + local claims green; cross-repo NOT verified." +else + echo "ALL GREEN — the book builds and every countable claim matches" + echo "measured reality (sources, PDF, transparency log, extracted code)." +fi diff --git a/main.pdf b/main.pdf index 3caae07a4fa30880c47ece1f2160230fdb2acd45..ffd93b0516029b7c327620e9734e1493bc664037 100644 GIT binary patch delta 11112 zcmai)WmMGP7w$=EkOnCw1SE!L7`jA|6zOj1K{~(0P*Oicx&)+K(h(RMk(QEf7`kB? z>iU0i@7w$Cyx42)z1FkOXFcaxXR-U$QunJ+7$yu0h7H4k;liH4@L>2bf<{89JEm}p zhdZIu6F>s|X|>m>Bwyf)9VZ^A#|LN|q%C9LSDaz(4 zi9Rz)2Tc+EMc|Lt%wT(M@W}N8Dk2@%GVtLe6g!}^=w@i>!H{xX{lGF-w%rsFm|gLzPNa^V#RSb$I8D9V%Q=1>%oTMtZ)3m~!;w`2QWg2MSI*QMXYyg6*lgmx zgPx^OnoT?Du;7$&Wc{7f7pRxjg&v83K?H5-rCMW-E~<{5W>men4eQ*D0BLyxCR znt;PKgZS=W5zCy`EFSL zYl$#dCAo1sDn5+9*5?wts$x)V&Zms8br{+>$cD7QEK8Tm(rM(UpcK z?;;TyNrh=cm8~HKe94x#%Dgr}`}WKArT@fUA*<8QC#$}zE8_AA?fy|GvXJ`TD)92H zby~oSU5eio24#m%Mu)eYp9NWex)??X;JIch65`AlMpQDiCbU+J3%RJ4*XN4ld=cgC z0Mlgg#+a;M8ma^r;jw!VkTAw<>_fFiaYSQEi+#z-3ydJDd(7?e-*_GM0E?y=Ucx48 z(Y4N1u6VosafJZW%i_}0n6=$$xsP1YY)caJW&Hc^n=D2krY+D)nyP6?Rnmj!Ow45? zmb{`G6VJWw3yR67!Os5U`N2*pX}Jf=QPA=t5y%^ z&HJ@Ui93^AWq!W>KR4qIZI(K%2}jXo!+HIbL4yw5<&nIB42qhPyFUtz-bvz!N=&WM zarX|GnsSO|@;{5kj<(V3G{@`5L6~vdnt^ND{8jq}znne^ezZPj2Uy2D4bR3CI4xMb znG%vbkvw4^CepuUbP3~%ScbeAT%8V#It_bqzY`yF@|~@N*X(h%aY9K@0BTFra|lj) z0?Cn|fUDmB&buTyPhZ$#-wAINVKP4mgJLWC(6u{+%vsZFXin0#kSP4lisH4k8PwtVvWXn@;glHvBs zW%pg(>y`rkf)U2ZkMVzuxXdCo9C-&Q^|Fj-E?=c(&7SN*=mbfg(4aI`qO|7z3}db# zLk52Bfb;B^%**l2Z}`pqH0bz&SugIz%>U}08eZ*wdaVQyD41WUfg1{2h8RB*Y-#lA zFBy?J*@{Gj^=txfS+m~wwE|ceyy4~W9eiqowinB-*PXsdD~S#y?KSjdo4h&Cwd%?h z3T-TFdRk@+D(8-6Cb_}SiqEs6(oTL{eG6qsbfgz?PgCd0&^1eRe=o3M{K_knFTu_r zmU;x+w1+oqO3butGqj8&22Ppvf?Iy?gtAawPavbCkr%)ntx?rzlHcLVkvOS(-0$$<$Lf&%o7$FtzdDOhoOW?jV|Nt3|TS5qNLtw-e|2# z8w^f=mZ}B>vS~*dmk4WX<|Fq%5vbu*{z{upmDA^%OvVa=R%1Qxb2;m|+tfviy?DvR zsa4EwTUF9Bk1gm^JEgNS4o#slrfoXVp|rjn7sn~u_jDubTflao$+C7K965eg8<6ef;AJ!sOt>SL+Pi!G~!JLk9xyF`&!a!4mI5C zp!_#ngmzy#hWw|NKTG%8{9-b46nkSX>BB;c=65gb0_{v=?A3^jzY3embE>^dO_P0_ zWcN-4hsZ5r6Pf#YD$OO|k)^^+LxWI)o zs72Ph&JQEBjvvmEC_e#&%>C{5zOBf{!C*G9?j-n3eYYmC?;r@$maA1_HRR(htkR_1 zA=w&iPF!2F^OUACD9|U-gxfHYPhrG}FL6I5)4g`~#* zDc+wt$ySo}*poTRq@S%41HH8m3bR+yMd9WgF$-|ZiqgKjmOFc}`S96-H6+J$l_?Hz z^hjReeSN-mh&*P@z%sB0mOE|F$>W&bzn}-PQO4thvKc;)=Ett5-gd8}hxn-I4V>2#b1Y%5l;9M`ktM%{N>jxx*V< zbGCvA{?KpGfK%_rJq%7&7I3BatvMjqV*P%xlj{7&3oIA1y|MnOS#9`r#GH4CaBJ=e z=Z&@0oxZw*oY|=jxMu{S_|5C1s1!?le~SM@g%o`}=r`+|j~y9_4xX06I^Ggl>Lr!$ zo*%W*B}Vz}4B1JTq99B;(IM|Y>C#)Q&E@w=4SV`OyTt&lk!@#b;nBY7{l{O&#V`*% zb!VuHZc3d2uMTA~g*16vA*YArz~-SJek!j1ZpGd|Y5aWe2tEV||Dcb@L@j-?LGvW? zQmc4Q7eaXV;?H#)T4AU~j)0=J!Ms&w{~G#^wjM)0Pu^Om(VNX}`~NH+g9FXt&y7w= z5_eK2Y;zu)FzPTX&JKe(SAdc0v(lT82VNkLWi$FlCnN`fgP*(Uel~f>3#22)WVa*k zoI~;~HkCs%Ew*NF1RjN1w#0A1`I{{_BKceALCL@nVn_B2K`H24-&p&fvc|8)yZHae zWDeXBfXTbwzLeZSWT8B~8R4bDZMI?XC%Aj?yi;>N2uk?9+*6LT5d6XI4 znVrP4l{HegT6D+#`_u&_XL%6er8d_%AF9Oa z>Vo8<(wz;;cIsHx=3>e32)=cqP0tzh`{Otl?4Akj_(DLHE<~;%^1D~0qGNlGGPdJC zoQBcX^4MN6=aBbTg4}^dnMt(b7F`l_<_YIWeJu3DqtQL*YZpNt*fLYN0vka>e9wqS0pIML zyOnZDnC9po4z;?K@aB&3T09JlG90vvBGR2jX64>1Bcosc0A#UX{H82{TUvS3u+)N8jB4U%yYJZOGH>~= zfR=M@gH%q;vyl|riNp7cVllr?AM#WM^oyT@ijqFY%BIte<|I84zZNh|aw~x?$5>3%jG4KugJ_;m1@$WBs6|CowkDrXTE<+-T54%NX3{J1P<^veYXLT z`^rp&Gb8eZbQ62E^jn)NR3vz0BIwQFEPL=G|E|!W;2?sN!fnmb0&_N4D%;-lro^$d z#bMzmXk~iluDOi$Tb}sUg_ryOF+&mI2-9mI7L_0n;SMT;_s=qR*wpplR_J$MB>G?3 z1r1;WTkyQ=V_-h;=B^R_yy@QuZVvwSQqcB+@Ig~-^!st(i zP;Rhn9nnkYs?>_pkBH)6#FX zzb)80b8wJhKzK1r2LH8L&Mps+SvrvVm|1!ZA{+J5vbZ)nyRU8Bj6;#PJN-rIynfam z>Uwf|yF)nXu)r6z&!c40Vi)@~b;V0>WzIjiIet^)C-G8|^joLlYo{8WDE^JtqQA%W z?C>d6XHT|`F1PBAgUnmXvlw&R0j4EPF2E1#2ub%)OrI!QV zUvB3GhLjUON~^w?how+Jm<87Kh4k( zcVj#_=m_YTSN=mIC3!z?lD1c_yMlT%I#B&Kk-2`RnV-OXrJbDlMBG&$fM2sc+`gPu zD75=|by2jd`Y?dLDs0wJX5d#UI1U2C->l8@p5`Gbof!(v&YNE#g_fDeqK3|?U^Q2* zwztTehqx4GhMk=INU>1@ouNfgvI0u(LlyH8OGJ+Be;C<5;%VWP2h2|PY8LX}r|7B~{YNMasF(~a zhgNpGvLSBmz()in8LamdPjiK)*YnwafJ|F^Mi5J_IU}$0=N7_xCl3?X@2zGFnn3g- znpMRc{EI=Qo6}uWwj+3fjdJf2luD2a?-O>zk2cx|vKnXhtI`1AK|O3SAmWr%`#!I8Wi12dhLW(Mm! z+ea^VK=KKYX2$57MD1cS&Fqr?b9cY1d7bHHv6k^mQHcabBu_lt-STr)+nfjw(E8|f z+vkDHWM=;mLdJLNZk4Rz=&%2BOa6)TtFKOOJ(_#izUnogmi_(mmg?j3OG9nnYoD>a zj@DahoWZ}fD8g{FL+HI zb6Er!5@6U=a$W}9{rrv8PaD7uV=m`Ohn-*2@)x?&arG@0yV5UHl8$WaXhZ;CPRfei zNlD~Ms>MpzW328Zo}ZAT{>tj$x60rsJQhSV5Q`^ElM)h-*81kV{3Elet*9+strmCFoMZFRN{MJ>Kaw4@1jKZ;&3IkFkwu@JI* z!*b9ptQRrFRNW3<}~Rw$|1XVgh0U*4AKQYjI&~8(SeEL3^;Mu)VOYt*wmI z|F0swJdV%?cp*oHStw30@z0j3#w2nTvcby=#V3@h6)yNEvgKlyC1Y5h6P*73D|{Ni z@fYa#$jMBt@_0FK<4srPo{8=6Mo13xn7F z*ycfrphE0*)KE3)C(0P)f8ef6eFJjNFE-wK9u*>u@GP(%gOQnZm23+{EywB6&6~ud zf~5{(oKx1NKTA~_HMD1Jbw9i}zpnJJ;&o0IsH%odvpQXWcI(Kln;c5TNHWlU3S}Lp zDFu8Yf20T|OX?>{TD?F-k{NWMC1#O-$6wK~W_oAnVay^vC^jKB7rM#p zrT7=WzpKBFz=bfoYr78jA78s>>PTFOHmtB*@F=YU|6=;UaxEP^;2Po%e-DWQqs+iP z_sE($2KDeIE1?5ST}!RML|0M4mKGU=lYk}U08iKw0ArBCB33QIuv-ZhX)4l)OemNU zQ>9yH{Q~Y#Q|2ofsBC09A%F1!{3J1QW7Q9gsR>K56w4tl?JS2r%OQ2>%oM;I4R2Uu zEIYJfo^l?HBwAHy#pjQDyZWwGJqL4kn3}}Js`i6~ffr6YRt>DulG&7GwzCNeFqx8x zcP0q1xP@o0(X>*#MJ!lhE@Bd`X&U1Ab}g;PqlzRJk|z)6j@Dd~&KPN9gga8o6A@08 zf#uAl6~2}%#>br@9`>UGH<^fr8|+Q3&qh(6Pye-`;B?O!+_~@HCQFvp@D?>CnvH9? zmrUW!uu6$m%~RfQmwu(`p^^e{Ck9<7CQE=u?apz1_}%M61Rs>WV!>ornR|+eYUa{_ z%#A&1*%zadErV?fmcpEaUt-Te7W9vk9y79$07(@^URgeMW29`hGRPMc; ztQfbi`Rvd2d9epI=vxhtJQAScZ^mAi%%5jeFMmb9XSYc^74G={pmCRO`m=f1gp~~t z$kci3vMrWrfRxl8d(3;I$&xbcZ<}(h+M&F!Ck0DVI{T<0bS&$7COD{;Y*reNknBfm zoydOeaR^*&)RJI!%pU`~ryoT%C4#;DzeP$7_!e2jEb@v?n~1txa_E8JSREApS$0BN zvh%~vLN6{D$_&V5dXh>~e-FIj30C?3=~wzh|KrE>%asiS72s()<&kSokWIz+=T-MD zHVLE-POCAkP6&0o{Cb>GGd`9`UH}$hy z1^1ZCv{sW01S3KKr!uDUQC2;q^J8|cS_e7&Srutfujr3|6O)4dPy4+Ty3(h))iXu&Q8YhE zN;_KlAM*#lY|W_yyqP#&*ngkydH2OuuFI-FOmk(stILot;fO_!^j_{Nr`%N)Xozvn z5iDUfQ_ZsEXAJx1x|UF9@*`)~(St$4X0rGF`U~0`3N4YR>ow1gg1e<$g$ZmwPaO6x zO*vO+oV$u9J85|Z{*_-Okk)v))-mG6J{kA(JqA%OE4Ro|8EKCl8eDwrvJd!7A9ciWL{?%4msK*hcduX@|KGKLbp#53 zdDEw#tUH{MOf2)P*46$=W-&5zykM)~9Pzn0d)Wl5AnA zn7#Ue=|**&m9Jrc_$qslvq7azS+E~8?{E)jplxa?Vr(}gK?-QgH zP7y)Q_hu;0@t=LS?Ke*Th@_yVD{bk7WgZ!eA?Wmuq)p{*S)TGSt%ccSGM z2YmvCw4QFr8a_S`DM!6?rju>@g^oS}#evSr`dMVA(b1;Ct*Dp5PC|2vF5CE- zmB^x#3{=`f`XKL6eWtb0?B5>MQ)(~q>F|YSV};9?dhN>_+Q;f(U_R(RsFckDp}Xl` zBnrF^@*Tk+@V#cpmUz3Jhk7+q26P(G(^Kd4AV3`}+jNgDh?WQcyXf`Xo}Km zRhD9ftiSb|2>jI|VWchjk z?gx}_zZTNwo(JVVzNLM9F6w7?$IYf8vz0CeLbrZ z3?^HSCRs6>bp6!!*-yb7k#c zSBr*f+G>M){X5(emGk46iw~)`ck3Ygh4o*}$0yk9vX2ueTA`{(X2dHrHsIjNKE5xk zOX3{He`?SyY@%oWy#vUut|*co=Xn^@kh}mMVnJ{sEBv;aEoaMwX=M=GCTi zL1nj-b`k}ybLWTCN4?=@z|5hgda&7h93DMSApl&bga&qu^!`^KJ!5NDrWs5}#LyX4 zM;;%MU`6?tN-RaLaTgDJ!eXHaX#w&k%)nphA+2LOz>)0X zuj4s*lEOaDK9ZxFQhKEh_k0=fFj$AD9wu!C`pa+?7HsuOJw?vpyrn~KC;w1pvd6s_ zr$3+aK$tM8>W+R}Gb;BQjNKi;>RB9HLITSTLq4xkFh9O|4yG%WnYxw5S;7#51yCza zcxdPM33yRn0e6X+<#`S-851{3&`%w3&;(VT^n=X$8|t0(k$LzHYgBi<;AajHlj=VD zh-LhiPOQ6nBx@_J10xzksyAe2BPlw-OZw<_D}e)r@wF)~CxaQuUZ7y6x-%VF6W?y8 zR-YE!UF*NBJs`b%#QL*ej{FWqry7!6()XpzUfb~n zyc`C)jG|{GYaN=HcZ3dbFPT;_nyRlN9lQj{8NqZvN zapV9RWkAuWT;C+#OKRV?-hYstszqaZ0SsrNR>TkTe)#|NS>6=zZDlwhz03~6SxRZI z?v?m7bNxZk^bMhib=p z&Hrg?-?~Ys1cEtE*hhme9Lp?}nQV}H;?et1=EBR|CBjR_3+Ed;2Tqk)@-NMIT&-9; z+{Os0RPfk13mDEIP4Xx)1+=^ljHU;JCjRY0PJ%@jvy*%l5jEt5Kvcp#al0(o6lsIG2j(G-Cbr)?m84;Uj)QC&+n_V*^51U}5C3zh z;8H*(3+_s%aPbQ1fj*D?AC_qN+Bi0L>tatAtJba`8~vi26mWT}!PRK{08 zd0j{C5-~}ii{ZQKC4U?~@4mN$B>cHH6;=;cMZOluw*ht~r@_Y2Q#L5A@f|JeG*810vlYX=_j%&1c3Agho)_5Xi#z8e`8y zT9t)&u5MM=Sm?dSOt&`}VlaNn+?{J!fYg> zAD|ec;0rkv{$9GR6dY@`J2TX+OU8R!lo|N90>b3>8%R?}p`7rdfLA$D!noC*aQXuT zb;okCBMQQ17*(WtNUPtOiu&ImAQkiQACY)%hMTh`+0hd(oH-hD1t8^x#;?^i~bOeYTxC2BO zu`dq|qh>fO$393H=dYT!;sCf)^eJw|*Sac*$~8zUxy1mVi6v&Dz1MKj#*IG;Kwniy zqWgDUt|{8$i-dKV6!(^vV>&RKRt8m8BFGA^B+(+`8_1Y9$B#72xQBTAJy9r=36DC0 z#L?8OE*kBHWuLMJ_Cst7e{C`jYo(;Na3=-?UhW7aa)?dQf0lW#pPYFW@#-el1pUXPG5NGO1_ z=kn&-6JG_f08iDAJB^#*T;O*^ zt2wCetl=`|3hsiH1}uHY9km11nLM3968L+l6Xq%UNs=a*r*w+1O8Kmu|I$42P0{O0X2cX}{g7V75Z~DMoJE{buLsE;N8PT;)8#2{ zodlX15>3^ojRu&0$kjzkDVP+EvRt}%L-eN*!i~|nUmr98^&M@9`&kbLv6|(Coacq! z3d8ofqwSp)04Df<@xr9l|BV++G5*C1Q2ybthE*3Z-e|RpDEsK4+)fEI68aPz7^Lka^WVom>WU8cVIrN zcm#uYH{c&d!C!i^OkL){Yu*6{mT8KI&T6X!ex!L}#oD(qJleP6JK6@sd#`%;Png?q zk2_Vg4X|Y*k|copxL#)zmcHD*>lO)pE&`D*r^@itd=$^yI|nZ@jO1&LAyM}SLz36> zW;Xgndldp^W+j!sAe}GkUc^W6eO*3p{>N03g&x1Zq$P@G^u;{2UL=4XSs71}S9?m0 zhFTaLT?S$#x$Th`pd^ig^S?1TMxyhRwE>oVBF;_^DB;wl#GLl*n0kcgsydj+EtF_Y zDuc-T@HcBK&ff2oE$!JdBs_T<$~QGl4!^Qt;|(=g6)US0^66~Xp0z=$VVIE@>~nct zhSx-b3AMU6v<;|`^jR?BHg2@YWsA2N!B@nFMfBDQ>D0=;dsli$KH)O}M#JE9(c(yZ z(fQnkxajKxvl+=ul<3!o8B>-$_upt)S`PslF&H1aHhhS=z8L4|erZpi0%gZpY4Ub8 zo4s=3&Fa`lwHr^@tL*B;bj#dGea<%mH?;aKDXU+JD=9fL0(Ajg6L!!m0Iu>Lb>!mYX#hag@vi#Eb)Fl`_4=jyg4|Okqdekm>uTuZo{n zX{N2VBuiiaw<{FMS)4LREpB7s}DAed(yrW=$wvCr86zFTKnV%N`@^kuRU$pHvjfg*M z&-m(-rH%jPs*HZ~;kSHcwAu$_+s7XEFXs)@4r@?9O$ASP6M%g<+-4R0FCPm}S$hv= z%1a-=`*oi~0D8ma`_0?FD~`gL?njE}>ObLVyZfNrrlbblQms#FA{ZYYU2aOQb8}{S{U=GBkJsj;sUn!r*FpAZ2KpqJCQSg2rp+% zJEKJ~n3d_vnKWzQ7lrnlem;|2-MLfYRUZHcUcqTwwg;znHES_@qGr;=y$qrFnZWTu z+kkGk;=v@%i7Ul$B6zB*`K`021Y;V{HFtaq?q?>$-Q_vY!6cnFONN)X$rGzMLh%}+N`)X+(|9yPoH` z87RoT=~andiU_Lf1b!x2>m$I9eKUvaF$z1Q(s6dgp7BS-sF%Z8)i~d9h_lxU?3T(e z#ER*fe^VIu-R$_~&#h`(X~@?>W6wP1t&(iRDDgT#>5L0a{xTS*uvz#k<+vQkdIj=Q z>xlY*(WM57>G;fx^Z7e+!nDifP z(LwhTR_b*+z)IpFPhay@vQpNQU9~T6ua$Ikhhm1X6J_E<5ot}1^M?NQ0QT;ou)>2sCc`i{{$HpSSMbY?R>%vmsr?9;JULzd7FsM-a5N-lW>0^Nfb(n z<|5k4@RwhB1K-2YFjvCD+q#xnOBZ`ZvgNdIp`zlLq4T)|EX2;EX*zEV2s}?zsx#3B z34;i2mt~qhF&l^MJITHG50v=CIJT+omm*m`E@OCP+(^18uvU%Z(oA|#iq4aGFJJfa z=cl(Luh9l^gW@VI|B;WIH`;R3zgHCj6KU)Z#+X(`UN_XTGY*`TkARrXq+x&kjnbeZ zO2XU*N_LL?TZ$#?xU~8*08@oCwlq_L9y9_K!z^6Tr^-Jeon-tQ7L;evRcLzSLXAOb zc}F zz0G+0n$`4zlgIv43xgz!<*lgyWr0nwwK`h5l%?x1PDpc65#%QRhM1Ufc>p3iRT@rO zafx64N0o`YqyKFF_q} zku&L(ig&HXh;ZYcL|RL#m~ps-1)(38UF}Nk>y8qN8LNm-wB3|bwR=aRvF1tv`ri%x z79yX~Pg-vX-+Tt*xG0&A3!gkmw5~puRvM!Ah?6>&KV=FuNfEjol4tA+h^lj7s0m?U zWE5}~z~)`nbbeg|R#u4MDs`a4G5Di+O}Q3hYl=IW%SlDJW01McKt0ixL1>hbHdKp)G-Bd^{^Q17Re_+nC=>Y$lK#Ehyj3OSRbOs%IbE*OdFSv!0jJ9s zcWDM9$+=q2AJxUaIU9sT3f$f@O(XxMg=C~4^NB!P~Uiru4xB98SvRx9c z$GIsJl<3P&J~B7A+L0mYK7x&MNIoy7tdB(ZjORL@jt5ADb?}iiy=HB$Sm6W8{!ah0 z&3;PKAF;|R9azE9%(=?F3bhW_0?mGzvMP&0zHah*YUhM6r8>E?o@O0GU3h4J6ZV~x zcHnaoFcpZ)@$oz72?eH!M#q-Ov~p-BaliJx04(_w5-*xfKDR$8#M{X6wP`T(Z%V|& zsDDABV9yj1+r=Lh>Mzn;5G{YQ>GaQA65h?MC6>WL@;=QgO_8ZkS1@L~rs3Vw++$*U zoMivg;Jc04PPCki0`o+@F1qJNhJF$hbXML5m?q)scN|!X$QF`%?4~;{{jgY{c;l9K zLh4>f3#&PhjvC^H7vygn5oXvX>d9o0slm>Vkn@%Q6@)boe51J8?`jLc%bWZMj;x^{ z3>QBnb&vFa9(*;pE$BWaf~@KN+5E6sS!7JG)gqXMa1uca^wOu$Hr}^nk#f`ekGwYp z%>PIw&IJ3*-pb;Y_kCS1loDRPe}C=f|K?9?=@9=#&Kk{jed0`I*6xs1;$~}qC0!xy zO=Z^PMzHW$J%kT4Nu9fKbCUd>cw2YAPH2>jYhWX&cM5NI|Ib}zTVCw1r_z)OR@~?Q z0g~?~>WNr+@+^ay>SX#fe&J0yulLaY1nTIhrG$rq6_`jr72dS9mDEu-&RF~A!-?G; z&NX`I$a<+~>Gh27>82o!Q{+7P<|Na2rAWJiUS3_??ZhAWpYw#ux0e~0vz2W=vHz8W2-&%L!LUM~=5=KI&TKypB~n)78Q^EV zhB5n$adnR4kXmz2rAkE?yM9k&ZAv6SmRadTxM4@N%wuSNGXa=6zqQtNxeT&nXuqL;`ZuJD7@zfJ(=OEhQ_z8L>WTF3h@%pQGAq3<^DeO=drOj)eIN-w!L?wEJL7ZF$ zz8Y?#nzJSne+_)$esz+NOVmV@sr>U0!ZQcok_0*HmQ^Bo)FZx5MmFF0iRAxD_e`7a z)jhkpY@`TgpGx)*yiP8Z5#b>EC-JuwxfE|T8Y;!LjM`8f8O&R z@?nTLJiJ^!mjY|Pb&aL=1pYNVm&n_<&uiz(5{VHO%hLYXG+TiyW)c04n(mG@|E*-5 zBx{;F1H&!h(3}LkJf~jj>DWkx2fSxxh|@u|z}wUpZpM`-^Z|3IOe=~!SyUvsx<24a zr9_CMzgEoM`T6(B9G0&kT4R<*JKIB(#t_mNVz&1FrGZ&4Odttzg>-;_ETiyD*sM>H%==RI>0PZAEYK_ zV};)Y&RV~^PBNIw1iDSd8%$TL!`5&eiJjlOp6P~iP&(Vb)}@eM*w2h3QN3_KS#NBV z(sY)Ym|Z#GC*v+rJLh=kElb@>^8900uLEV0AfX*^0(X zyW!e!`Qm4_H{Wd|sDIe65z&3kY@5)1>id^4i2Gz}Dup!Y#`J3Otl9Y(qVCRZ?w*mQd503`}qqdcoILq5J2@RH3%?_=PT4yKmQD*)t#(h34)8+KWJx(k8 zN6S~o<9^K&y#m$vRlCXZ^6RU&cf*xRUa@bU1EK5_8>>XsP^3ic3Ed$iy!xwfw{1ZP zJsjC*)ehZ#xGTJ}R8Xu_P(OOhc^;Q~$3UM%GrujhCH%6ng(mt=A@z<=_r{|Fmiyd? zzmx9gBiecA zz+ghpiuyFUiG(wSmO;B57N3}aefrEP<~XdT>>z@4%+Az38q_N|g`R*}Vz1#+gk*@9 zYdOHl4kJdNxs*Bka0U8jPg^o7Dy~&sOIZ+ZFfWfbm3Yo3Cg^aP%t&zS3ma;Bfm?r2 zULCzOXgMazD6rngD<2P`b+{dSz4+lT0PO7FjYl@F&n|{!1f%%`Zk~s#)IYoO_>!h3 zWX%wKk7^&dSoS4?-xAI&xV?L>@>j}Y-p|*vP=GyPR#5q$k<_zYkt#9)o|OA!HUZy4n=SJ z-|fl!^U5ZN=B%>L6amBfL6~DGKxMNco6|9!)<kI0A)0%Lmbrdf$$^sE{QVO5XJr6#Yf@_=WG$R)MJfiUKwR6870}pZNp3&w{ zj>}N_2gktA=%j_JP)~zPrdoK&T1lm&|%LVGbz=a}Bf4%73^>6mH zJO%Fk95-Df&8s3^Od0R$TAzc1Q2LQH;1O!g$vGSSud(2}z(K`k*sE2vXw@X6tRY5<1L&u`}hO~zye zeI6I~FO;=TR7-5W114jmcze zyF;lrh{N}wP9_qRjurJ__-rcK2-+i%V7S7h% z^WPgL(zD^T)6v}7R1f&oe^G%Cnje(P+>uEP1DhGrSAYH10dC$>gEyY+MJ!AHD9c10s9=#j-)gWovfGU;3G4K`hr5W=IwX*9Q0E`3v7eryp{>J?cS~4$%#g*w=OH;c#&X=d z66$IG3Y?kU3s)XTnVHz>n-+Z42>8^WLs*%!+K_(R$CQ3Besmj%a61TcmZzCp?_O`L z5IPRUc_n(q*Au~N;AW$3rNL*V?(&+ed7`tPTnj9!0gP(HcLMGLPlT6WEwl~49%gY% zrY@N&Lwe?Be5kfbHuRNG|03FE^ERZtvjr+za4Q_BoW#-W;pKXvFE%Xa@!;`|A+hy~n9A~reZ zac*bI-}=wNbp3=#o}TsZvF?T4?}z%(vRKTRYoM$^h(RefH$|#gG)|sZNcqD6wEH2E zVcdue!xKGt_F*|W9>WBi+&GG%92h2k`VAp91R*z zgMf*x0)Jq)u zlG_Gd6?!r{*mJt%js8ggFg>>R5PXLUSm^wHA|F!N_-|qTBjd=;uA+sGbqf_)ZaX6y z+aY$`(*cy-P!H1ivfakWy#aa-{H8A7?rKemW5+S-9P|Wy8dsPW(6-HBMn9FHA*4!^ zE~AIa-4IgM`z0gVuqJW~`?(B<4kTvYaFF1ysfA%4FG(GgOJ`oq$e8S4x-NyXVx`xN zNkHck%V;EyO5#7nvn`d*S}6U(bS;!qXTqz-cBl$DfLPg@3wH8hI<}-?B=y=*2R%!P z-riL4bOsEwWa$~&ZGGC$qYb!WRS=m8>I#%mdObRQa*@3^5y20_>+J#6rR3Tj(B-!VOAtQkPUw^}S-7$d z4I^$W%r%Q$$F#k@q`>WnI(Z|3v;;ix1|rUgH8S7{k;{9+J)i**&BLr1aDvF>VR&t7 zfrzGJR+x8`x-;ZJEP`P~o6pM9BUC6 z@PWv$Jt5jqYa?)vG21X|BXN(FwPsr*NZb%?Gt1iq#2s?wCku|4r>cs`15A6Z0CI57E`rL4B(cqi}%-$ zj?pImrfe5G=7ewFQlVq=2Ua6ML=W4q(zL28kbR9*l>+r>p40tAeJwzQ=3ImdoVTc7 zk#VIrF4-S{3W)9@y1XA({TP&Ocg&vKrF$k|TEE2>%<;L<;qwjJDLqxgDB)1%!~OdA z1t0>A!KARdT^=%qRKE+R0idXQPv|eORdUm(-D~#?qBOIi@<7=YBdfQUC43uvX%*~R zJNw|=0Bx?QP^?Sd0f+0ErnfhAPGu+RMie)q!`D{FKTtvUh&{5cj|1IqSsq%3JF(4Z zosd#kwj(2j@g!q<)eT>+=bJhw2DZ6_1S;bpAnU${G1o&&fnfcASJ&X>zH0h?ZL#)n`eB?q zsaf1Xs;<^fr;g<8XDtVBKFEJ5`@`*JK51+Vy2VCs=>#~7t^=~Gj~%XiFyCkB8kS?)OBE{9 z(b!gzD^wg57+vREykfk@CpT>Mz5mt%DK=!0<#azlyP!LKB6R%u>#)#G;$`P18Tr4z zfJErB-a*9%nVMg0)mBe$zuhs~T1@^wV%3WHyGW<(W3sf2<#YtZTWE=)Jn=5ENF((7 z5ZB$O3E-7O++C-9`7L*S-Bp>4>6&7SC@QtkM3Kr0+^!0Gum+HAnlO#jiZpFfR%s0R zPxtN@tRNG)@9|tLX3poz|LH0n%zudI-h^v$iHzIFq-8%ZP=F=FcWD<`QWQz@NxTNd z2IM@a|ND=M?58S-l^V}L`aj3p2TtWC(pSMA~L4jpd zL;6e097G;Ve>gs$&!i9Ocl|U->}{UsF`zAegN_q_} z$XYD%zgktH7|lV37laO7uQDh3IrYOVxqjbPm7Dgi8D;9Pzxe$Pdz;&$2}O7>u=jOK zJ4JN2t4k+g*Jd-|p&*CsQTUBVE?f;o7bv@iaTy3(G;|82I_XsRc&pN*(q%;|iOTe- z>m@>C2e$h6N?8e<{7b7}V6Lv12^!jUp@7~7JGlC=%s1{mY}MG_>RGL;vjhTR2vsB} zu~_H;-T}*?5Vcic6LL1O7QjdUxc-5%zPHh@1?YN{?(~RL6FmkhxWqggCK=hhNJ5@6 zQ^7x@MYGG=CH1v-WP(6EJxA+WK6gxJ0>y!e)s`oom3~}#if%ojk3K{_oafB%XO1F! zPmq1ocIUt3$vjSd!JgM*yuhiUni|gT=}F>AYx^+z=%fx{Mi*bBPTP^aOzsav*Qta5 zBAtwTSlEvc&r$l`Ro50f1=s6oK_BB0Vn}0jH?maC3@wTxLXKpk=2&R=b;nPw5)?P{ zkyJtN(1a+43&YBPH!@vps5#ek-G{PCIEPhy4~~a&x3S-l; z-1fHr<;3FEi`zxbb!D$5%$BG+YnLTlu0B9ziH57+w?Y2!iR^$*gV-Tv=YSo7_`dDb zw^98du5}QVJo@PpQ~3b1Fv(R^x3xzW>79B}`i+@Y(d@KuA^oP*d&cc)&nx<9un|hj ziyJl-l!vmBFKGYeKZ`ps^~9Uph^_u#Fe_t}J{jVHCCU8>gHm?_+a9QL`u&Rzf*>Gt zWWr!tjEEHGsUH$2#`u73v|-m6YY5tgeEj)1A%W-tY{q!8yFiroN<2XF;csBR%J!Q6$Fov_)FR{XibnIpe?Y{wa zF$YD=F3$q_f)tX)m_ld@Vrh{Meda*kTYmxvt{@YFOVor?eQYkoK3$Puy3gzS5g~a* zc}MJd0ecmvIKh#Hu{3)_*{P&`GE*1b`A}&Wr6cif9{ILUJ@`q8sp! zhpliky?j(5EK`IRY*({5T-)_36)!`m&NUFZUkNVxz7rzEUbEJpj6b^|&H@q}Y3lqe zr=6LmK4jruGFg!|*ImVgKnQ=*3#Zp~hV@cd5DIO(Dp`duZjjthLWtH903rmvyYh6* zIi#iZGQe$UIeg(8BL6xX!aXI}h6gSjP=MZI%SHDRh2SdmEhmR!TJdt%cFWu z7~su3aB7TgQ7F7g)nYJUvi)*orheoJ2!EIIR3P!C!FOHpv_VJrf z7Q}c)c*40ok4trxA9xXT%JnkL(4m011wUV+$M@_1+UDgmT7dOd&Pq2v=2bX8oEdD% zDFYjO?iU94yLtfp*%8y@LZC7o)()Ww#R;k;xU}$(h7vKnl*bFfyVOKwctJ6I?v3K1 zI6l)SKfQ`Vm4ADg3thZoa)_xPa6xgg{P)gz_1+(ZVfB-$_$qh))MtB~O*TJM#TjEN+TN95fz&&V* zj+^9azzK*rCb@&e7@p>q)F`=ecZjkP4)^6;BO9b$G0fg3M>l(#en*4+$-#Fi>}zFH zAh(|u*2YUDiWpp5-m&tKm6F*9g>c}>Q7GBB*6ZFa-hUw!rb9(<_eguuD zOfl6aY2MVHh2EWZH^bxoyp;w89nlU7{tXl0R>w!#cmy7i9`PHaSr?uPXF|*#h68lW zLo*Jh#HrgCcGE{TczKqN-Mb@2TtP5z=m$E+lv%twv1kg2cqs1b&Nd@#CZpEMCttsI zcsl9R|&vN z_)|*YHP7_mdp3IY7Vv*EdWA((sn7a{K`VDs(YG{7e``?H>Y3L$IePFVsPVh}G{; z>vW9@XGEJ6`lTTvsE?ImT~;j7VzA?(PCAth?C$In?bUs05zyywa<(AA&#Sexa8&gxcLc z>CYx@t~*wp4i6-~6<7iAF7ImDe@E-BPP}TGD$m^5vr@cxcfd@#y@&EC@Ogs9pIiQP zyi1-E+UmnsN3%^^s@taz;$&2v27}khPA_xoM<0xkE15yH5$}v|@ZTb! z4||?^;BUr1Wimp^E)h*5y~Fef{N?0QFIYH)e9p5fg{)b3hN7xR2v%g-nIdx$R3=t_ zeu|kgmF3M?V%yNUr=S<4#pLBIBu$REZeT=4lfE50AtAbE z5?fpG!TrvJkeLTny67D!TYOj{myDRSc~l(`m6qT$q%cNHn2fszju}j{0ZS{&&4$ty zZxv>@MBy9JQQq{ZH3aoNCa7<0l`zx)XbpF-@{8^IdW5M+BOW%NfXGQ>V4LKir-1#d z2icn!StMRXP$nh*j zHFE%UmT~cw1m`KX9Nu)_+scqZ>dKIQuSz~#AL=a<6H*UY=PAY9eAx7c?UWVzIr3Rg z7_}Z?7ND%Qdve05_iF{3dH%|RX*ayo8mp3TAwn3}DDsWoV%B_A2d|cK=05L_s|EsB z{B3Km%70xXk4)|Nef+!VN4H*We~iyU8JK56jJ>cp`R0=Twiv2_AOR1ALRcpvB8#9z zzvg8-P}~fNlWngJ5C~T%rbEHu`P`+L{-!GkYbxqs6B9(c^U9+02f1KO$C(}doCI%& zyB)PTmXA*q^kL~qD{K~QYLZj0W1RVWH1-(U-A9w){zvJ29mlEmkNG;z(_R0XRrQ83t{N&1 zlc4bVcuK9C=y^9zknk*mgJ5U9sUshoNb!3|H+G`E>H4dPGEO7EFV+E?HL@BFCDp)u zKIe4{>)I|ZocmoxBDSJyQ%4Q9VyKJH4{SwrKf;~z-X1#7LwPUxWA~WyKK5NU)jiL; zOcmvQdmnEG&DOz676tF}*^2-C z7jnQ?Jon1T;dSLSW6hn$i}U9B2TpMSQZkRl@r62o28&aCOST42!_oW8d?cs%P0_qE zhq%NKbTQ@F!!n`~LMO*vEbUiYNCNJA^O(YT+1g>UbSjLN<4dMne)efe z6phO9AJ@mg_2WP&%rP_jsfAgfF)o{dCalHL+(!yh{Q`P-olFq!IrIZhG;>f9iWY|9 rkB_+hZrgxe5LU54PjJM%1wxbYKO+ETiWd{I5{O6>a&oHbsuBJ#*rD+}