eager: Nat.divmod__fastest as a jet

[olydis]

Draft: this jet is not proven. skip_line has runtimeJets_sound; this jet has no theorem yet. Here is the proof plan, also written in implementation/lean/Cpp/README.md:

1. Show the partial's shape. divmod a = △U (△V (△△a)) for every a. explore can decide this with a as the uninspected var 0.
2. Build a bridge between bit lists and Nat (natVal/ofNat, core Lean only, no Mathlib).
3. Do list induction over a's bits through List.foldr__fastest, with the invariant "top bits = q·b + r, r < b".
   • It needs lemmas for is_lte__fastest, sub__fastest, succ__fastest, double and canonicalize, each proved by list induction.
   • explore has to be extended to handle pending frames and several opaque variables.
4. Prove the transition reduce (△U (△V (△△a))) b k → dispatch (△ q r) k and use it as a J of runtime_sound, as DropJet is used.

What changes

• eager-graph-nil-mmap-32.hpp. In the S-rule branch, after the memo lookup, one extra compare: an.u == U. When it matches, divmod() runs:
  • It checks that y is △V (△△a).
  • It decodes a and b into 64-bit limbs. It falls back to the rules unless both are lists of △/△△ with no trailing △ and b ≠ 0.
  • It does shift-subtract long division, builds △ q r with list() (r first, on every compiler), and records the answer for the MEMOIZE frame. That recording is answered(), which skip_line now uses too.
• div__fastest / mod__fastest are △C (divmod a), so they reach the jet after one S step. They need no keys of their own.
• trees/divmod.dag is Nat.divmod__fastest. It is identical in arboretum e3df589 (current main) and in forest's bundle. embed.mjs turns it into jets.hpp and Jets/Trees.lean. U and V are read off it, since divmod = S (K (△U)) (S (K (△V)) K).
• test-jets.cpp:
  • A 1,000-pair differential test against the evaluator without jets. Operands are 0–139 bits. Inputs include trailing △, a cell that is not a bit, a list ending in a stem, and b = 0.
  • Trees that only look like the partial are left to the rules.
  • The jet answers in 1 step, and asking again is a memo hit.
  • The jet survives collection and clear().
  • With jets off, the evaluator matches the one without jets.
  • Mutation check: dropping any one of divmod()'s six input guards, accepting a trailing △, or dropping the trailing-△ strip on its output makes a test fail.
• Review fix (19433db). fork(natural(_q), natural(_r)) left the build order to the compiler. GCC builds r first and Clang builds q first, and the indices decide memo slots. So step counts depended on the compiler: Audio.Wav.33 took 33,342,557 steps under GCC and 33,854,449 under Clang. Main takes 75,030,361 under both. r is now built first. GCC's binary is byte-identical, so every number below still holds, and Clang now matches it.

Measured

All runs are on the same machine. Base is b873b56 (main).

Whole-bundle replay: one runner loads the bundle, evaluates every test, then dumps it. Steps are deterministic.

	base	jet	Δ
arboretum, steps (7 collections each; reproduced exactly by the reviewer)	2,126,197,102	2,089,095,459	−37.1M (−1.7%)
arboretum, runner wall, mean of 4 concurrent base/jet pairs (slots alternated)	149.0 s	148.0 s	−0.7% (per pair −2.8% … +2.8%)
forest, steps, no collections (4 GB budget)	2,103.4M	2,069.7M	−33.7M (−1.6%)
forest, steps, default budget	2,971.2M (10 collections)	2,706.1M (9)	−265.1M, mostly from one collection fewer

Single tests in a fresh runner (median of 3, base and jet alternated):

	base	jet	Δ
:test.Audio.Wav.33	75.0M steps, 5.00 s	33.3M steps, 1.94 s	×2.6
:test.Music.Melody.36	136.3M, 10.37 s	75.4M, 5.20 s	×2.0
:test.Image.Png.Png.30	23.7M, 1.09 s	17.6M, 0.73 s	×1.5

Full builds from empty caches. Each run is one sample. Summed runner steps vary by ±100M from run to run, because tests spread over 4 workers and collections land in different places. So these rows are not a clean measure of the jet; the replay is.

	base	jet
arboretum ./build.sh, wall	65.3 / 65.9 / 62.2 s	63.5 / 58.8 / 61.3 s
arboretum ./build.sh, summed steps	2,266.5M / 2,254.6M / 2,453.1M	2,263.1M / 2,061.8M / 2,129.0M
forest ./build/full.sh, wall	167.4 s	158.7 s

Idle cost on a test with no division, :test.Certify.Size.Test.45 (5.51M steps):

• Instructions (callgrind): apply goes from 393.6M to 406.9M, +2.4 per step. The S-branch compare (cmp + jne) accounts for +2.0 per step.
• Wall time (:test.Certify.Size.Test.43, 24 concurrent pairs): within noise. The median jet/base ratio was 1.010 in one slot order and 0.993 in the other.

Validation

• implementation/cpp/dag-machine/test.sh passes under LC_ALL=C and under LC_ALL=C.UTF-8, at both commits. test-jets.cpp built with Clang also passes.
• lake build --wfail passes.
• Replays: the dumps are byte-identical between base and jet, for both bundles. With RUNNER_JETS=0, step counts equal main's binary with RUNNER_JETS=0: 2,124,623,037 for arboretum and 2,974,074,032 for forest.
• arboretum ./build.sh from empty caches with this runtime, 3 runs: src/ is unchanged, and the lambada exports are identical to base's.
• forest ./build/full.sh: git diff --exit-code --ignore-submodules is clean.
• Differential fuzz through the runner: 2,400 requests over divmod/div/mod, up to 300 bits, about 20% of them not canonical. Jets off and on gave 0 mismatches. Operands of up to 2,000 bits match Python's // and %.
• Structured differential: 39,888 divmod/div/mod requests, 0 mismatches against the rules and 0 against a bit-vector oracle. Operands:
  • 91 patterned values at limb boundaries: 0–193 bits; all ones, 2ᵏ, 2ᵏ+1, alternating, sparse, dense and random.
  • a = q·b + r with r ∈ {0, 1, b−1, random}.
  • a = b·2ᵏ.

Caveats

• Unproven, as stated at the top.
• Smaller saving than the analysis estimated. It estimated 69M / 82M steps per build. The replay saves 37M / 34M. The full builds' step totals are too noisy to pin down.
• Idle cost. About 2 instructions per S-step, paid on every workload, even one with no division (see above).
• Fragile key. The jet is keyed on the exact U and V. Any edit to divmod__fastest, or to anything it uses, turns the jet off silently. That covers foldr, is_lte__fastest, sub__fastest, canonicalize, succ__fastest, double, Pair, Bool.match_ft and fix. The fallback is still correct. A CI canary that checks jets > 0 would catch it.
• Merge order. This touches the same spots as the other jet PRs: the S-branch of apply, collect's mark line, intern_jets, test-jets.cpp, and the generated jets.hpp / Trees.lean. Whichever PR lands second should rebase and rerun embed.mjs. arboretum and forest only benefit once their tree-calculus pin is bumped, which is not part of this PR.

🤖 Generated with Claude Code

https://claude.ai/code/session_018ffv5AybPTpV56D5vuayQr