[olydis]

Draft: these jets are not proven. skip_line has runtimeJets_sound; add and mul have no theorem yet. Here is the proof plan, also written in implementation/lean/Cpp/README.md:

1. Show the partials' shapes for every a.
   • mul is S (K (△U)) K, so mul a = △U (△△a). explore can decide this with a as the uninspected var 0.
   • add a = △ (△ (△C Z(a))) K, with Z([]) = N and Z(h:t) = △ L(h) (△ (△ (h:t) △) (△△ Z(t))). This needs list induction over a, because _zip_rest a is unrolled one layer per cell.
   • Already proven here: addPartial_check, which shows that addPartial (the tree C, K, N, L(△) and L(△△) are read off) is add [△, △△]. It is checkRun under decide +kernel and takes under a second.
2. Build a bridge between bit lists and Nat (core Lean, no Mathlib).
3. Prove the arithmetic:
   • add: ripple-carry induction through _zip_rest, _add and _carry/succ. explore has to be extended to handle pending frames and several opaque variables.
   • mul: induction over a's bits through List.foldr (s ↦ 2s + h·b), using add's lemma and one for double.
4. Prove the transitions reduce P b k → dispatch r k and use them as Js of runtime_sound, as DropJet's are used.

What changes

• eager-graph-nil-mmap-32.hpp. In the S-rule branch, after the memo lookup, there are two compares:
  • an.u == U leads to mul(). It reads a under the K, decodes a and b into 64-bit limbs, multiplies them schoolbook-style, and builds the result with list().
  • y == K && un.u.u == C leads to add(). It reads a off the first layer of Z(a), decodes a and b, walks Z(a) down a comparing every layer (5 loads per bit, no allocation), and adds the limbs.
  • Both fall back to the rules unless both operands are naturals without trailing △s.
  • answered(), limbs() and natural() are eager: Nat.divmod__fastest as a jet #62's, verbatim.
• trees/add.dag, trees/mul.dag come from arboretum e3df589. They are identical in forest 452c3f0's bundle. trees/addPartial.dag is add [△, △△]. embed.mjs turns all three into jets.hpp and Jets/Trees.lean.
• test-jets.cpp:
  • A 1,000-pair differential test against the evaluator without jets, for each of add (up to 140 bits) and mul (up to 70 bits). Inputs include trailing △, cells that hold no bit, and lists that end in a stem (the last two not as mul's b, where the rules take up to 48M steps).
  • 9 trees that only look like partials (one per guard) are left to the rules.
  • Each jet answers in 1 step, and asking again is a memo hit.
  • The jets survive collection and clear().
  • With jets off, the evaluator matches the one without jets.
  • Mutation check: each of 21 mutations (a dropped guard, carry or mark, or swapped Ls) makes a test fail.

Does add's O(|a|) key pay? Yes

Each test below runs alone in a fresh runner. Times are runner seconds, the median of 3, with the configurations alternated. "mul only" is this PR with add's compare removed.

test	base	mul only	add + mul	add on top of mul
Music.Melody.36	139.0M, 10.78 s	96.8M, 7.79 s	79.1M, 5.93 s	−17.7M, −1.86 s
Audio.Wav.33	73.1M, 5.01 s	50.3M, 3.63 s	43.6M, 3.11 s	−6.7M, −0.53 s
Audio.Wav.31	53.1M, 3.63 s	38.3M, 2.40 s	33.3M, 2.06 s	−5.0M, −0.34 s
Random.Test.3	117.1M, 8.82 s	86.6M, 6.19 s	85.9M, 6.44 s	−0.7M, noise

• Every step that add removes is worth about an average step (68–105 ns, against 62–80 ns/step overall), so the walk costs about nothing.
• I also prototyped building add a natively, which would skip the O(|a|) rules for the partial too. It changed arboretum's replay by +0.4M steps and the times above by noise, because the partials are mostly memo hits. It is not included.

Measured

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

	base	mul only	add + mul
arboretum bundle, whole-load replay, steps (7 collections each)	2,126.2M	2,079.1M	2,058.6M (−67.6M, −3.2%)
forest bundle, replay with no collections	2,212.4M	2,110.6M	2,031.3M (−181.1M, −8.2%)
arboretum ./build.sh, empty cache, wall (n=1)	65.8 s (2,253.2M steps)	–	61.6 s (2,047.8M)
forest ./build/full.sh, wall (n=1)	140.4 s (3,259.0M steps)	–	134.1 s (3,060.2M)

Jets fired per replay: 197,275 (arboretum) and 248,605 (forest). In a count over the arboretum replay (an earlier build of the same jets), mul declined none of its 90,691 candidates, and add declined 816 of the 105,990 whose key matched.

Review rerun: the step counts, dump hashes and cachegrind counts on this page reproduce exactly. arboretum ./build.sh from empty caches, base and head alternated: 67.1 s, 64.6 s → 58.6 s, 60.1 s.

What a key costs where it never fires

Certify.Size.Test.50 runs no add or mul. Instructions under cachegrind:

• base: 420.4M.
• Same trees interned, no compares: 427.6M. This is layout only, from 1.1% more steps.
• mul's compare: 437.0M (+2.2%).
• Both compares: 440.7M (+3.0%).

In time, the median of 5 for heavier certify tests sits within noise:

• Certify.Size.Test.43: 1.86 s base, 1.83 s with both jets.
• Certify.Size.Test.47 (94 jets fire): 8.82 s base, 8.99 s with both jets (+2.0%), and +0.7% over the same layout without the compares. Review rerun, median of 3 alternated: 8.51 s → 8.43 s.

One thing I learned on the way: reducing add [△, △△] at intern time made GCC clone apply(), which cost 4% more instructions on Certify.Size.Test.50 (456.5M against 438.4M). That is why the pieces now come from the committed addPartial tree.

Validation

• implementation/cpp/dag-machine/test.sh passes under LC_ALL=C and under LC_ALL=C.UTF-8.
• lake build --wfail passes, including addPartial_check.
• Replays: the dumps are byte-identical between base, mul only, and add + mul, for both bundles. With RUNNER_JETS=0, the arboretum replay takes 2,124,623,037 steps, step for step equal to main's.
• arboretum ./build.sh from empty caches with this runtime: src/ is unchanged. submodules/lambada shows the build's exports, identical to base's.
• forest ./build/full.sh: git diff --exit-code --ignore-submodules is clean, and submodules/arboretum shows only the tree-calculus checkout.
• Review stress, against the evaluator without jets: 3,834 distinct add/mul pairs at 0–4,097 bits (limb edges, all-ones carries), with and without collections, all equal and all answered by the jet; add of 70,000-bit operands, whose sum list() lays as a run, equal too.

Caveats

• Unproven, as stated at the top.
• Bundle and build totals swing with memo layout.
  • Interning add's and mul's trees without any compare moves forest's replay by −26.2M steps and arboretum's by −4.8M.
  • Production-GC builds move by ±100M steps or more in certify/snat requests (the review's two base arboretum builds: 2,449.9M and 2,274.5M).
  • Forest's "mul only" vs "add + mul" difference (−79.3M here; +26.1M in an earlier build of the same jets that differed only in arena layout) is inside that noise. The isolated tests above are the reliable measure of add.
• Fragile key. The jets are keyed on the exact trees. An edit to add, mul or anything they use turns them off silently, and the fallback is still correct. That covers _zip_rest, _add, _carry, succ, _add_3bits_k, Pair, Bool.match, List.foldr, double and fix. A CI canary that checks jets > 0 would catch it.
• Merge order. This touches the same spots as eager: Nat.divmod__fastest as a jet #62 (divmod): the S-branch of apply, intern_jets, collect's mark line, test-jets.cpp, and the generated jets.hpp / Trees.lean. answered, limbs, natural and the test helpers tree, kids and bits are eager: Nat.divmod__fastest as a jet #62's code, verbatim (only kids's comment differs). Whichever PR lands second keeps one copy and reruns 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