eager: answer Quoted._whnf natively, a jet not yet proven

[olydis]

Draft: this jet has no Lean soundness proof. The repo's convention is one theorem per jet. runtimeJets_sound covers skip_line's jet only, not this one. Nothing in implementation/lean says this jet answers what its tree does. The only evidence is the differential tests and the identical replays below. Proof plan (from the analysis):

1. Write a Lean model of the native loop.
2. Prove Apply (W f) (template f) for an opaque f. This is what keying assumes. It is a symbolic run of spineWhnf; checkRun W fuel took 0.6 s when measured.
3. Extend Check.lean's explore with call/return verdicts, because the recursive calls on a and c are not in tail position. Add typed splits for malformed lists, Options and Snats.
4. Compose those macro-steps with strong induction on fuel, plus a lemma for List.concat (inside _push). Each branch takes 0.6–3.4 s of kernel time (measured).
5. Plug the result into runtime_sound.

What changes

EagerGraphNilMmap32Jets now answers arboretum's Quoted._whnf (src/quoted/spine.lamb) natively. This is the fuel-counted head reducer under Certify.Size.

• Tree: implementation/lean/Cpp/trees/spineWhnf.dag is Quoted._whnf:4 at arboretum e3df589. Its md5 is the same in forest's pinned arboretum. embed.mjs embeds it into jets.hpp and Jets/Trees.lean; both are purely additive.
• Key: each call is apply(_whnf fuel, t).
  • On every clear(), the evaluator reduces _whnf △ and _whnf (△△) by the rules and diffs them into a template with 6 fuel holes. It throws if the fuel shows up anywhere other than as-is.
  • In the S-rule branch, after recall(), a single compare u' == x gates a template match, and the match recovers the fuel.
• Native code: eager-graph-nil-mmap-32-jets.hpp (jets::SpineWhnf), kept apart from the evaluator.
  • It follows spine.lamb's loop, with the calls on a and c as frames on an explicit stack. Nesting depth is at most the fuel.
  • Any shape spine.lamb never builds returns 0, and the rules take over: a list ending in a stem, a non-spine, or a fork for fuel.
• Memo and stats: the answer goes into the memo the same way skip_line's does, through a shared remember().
  • RUNNER_STATS counts it in jets=.
  • With RUNNER_JETS=0 nothing is keyed.
  • The jet's entry point stays out of line in apply(); inlined, it costs 2.3% more instructions.

Measured effect

Same machine, back to back. Base is the runner at main b873b56.

	main	this PR	Δ
arboretum replay, steps	2,126.2M	842.7M	−60.4%
arboretum replay, runner time	159.9 s	74.1 s	−54%
forest replay, steps	2,971.2M	1,529.7M	−48.5%
forest replay, runner time	224.3 s	111.8 s	−50%
arboretum ./build.sh, empty caches	65.8 s (71.2)	44.3 s (46.3)	−21.5 s (−24.9)
forest ./build/full.sh	167.4 s (158.7)	154.3 s (137.4)	−13.1 s (−21.3)
compiling compiler.lamb (jet never fires), instructions	794.4M	822.9M	+3.6%
same, wall time (mean of 5, alternating)	0.437 s	0.422 s	noise

• Replay: one runner loads the build's whole canonical bundle, with every expect test included, then dumps it. The jet answers 243,761 calls in arboretum and 278,370 in forest (jets= less skip_line's 25). In arboretum the gate admits 410,982 calls: every one the template matched was answered, and the other 167,221 (other trees sharing x) fail the match. Collections drop from 7 to 2 (arboretum) and from 10 to 4 (forest).
• Reproduced in review, runners rebuilt from both heads (byte-identical to the ones above): steps exactly as in the table; runner time 156.5 → 64.9 s (arboretum) and 214.1 → 112.6 s (forest); dumps identical.
• Builds: the tree-calculus submodule was checked out at b873b56 for the base and at this commit for the jet. Numbers in parentheses are an earlier pair. Both builds already run their tests on 4 workers, so the wall-time savings are smaller than the replay's.
• Idle cost (cachegrind, compiling compiler.lamb):
  • The S-branch gate is 1.4%: this PR without the gate takes identical steps and 811.9M instructions. It admits 630 calls there, all rejected by the template match.
  • Keying is 507 steps and 2.1M instructions per clear(), two of them here (0.5%).
  • The remaining 1.7% is arena layout: keying's nodes shift every later index, so the memo collides differently. Without the gate, the build takes 0.4% fewer steps than main but 2.2% more instructions.

Validation

• implementation/cpp/dag-machine/test.sh passes under LC_ALL=C and LC_ALL=C.UTF-8: 33 PASS each, runner 21/21.
• test-jets.cpp tests for the new jet:
  • Differential against the rules (the evaluator without jets): 2,722 calls, 1,161 of them on odd shapes and 1,027 that ran out of fuel.
    • Each spine runs at every fuel from 0 to one past where it runs out (up to 46 rules).
    • The spines include I-chains, Ω = δδ and 400 pseudo-random ones.
    • The jet must answer every call on a spine spine.lamb builds.
    • Five hand-made mutations of the native loop each fail it.
  • A fork for fuel is left to the rules.
  • The memo answers again what the jet answered.
  • The jet survives collection and clear(), including a collection in the middle of keying.
  • With jets off, it runs step for step like the evaluator without jets.
• Review's own differential (not committed): 168,300 calls on random quoted terms over △ and variables, corrupted spines, fork and random-tree fuels, fuel up to 100,000, collections under a 4,096-node budget. 0 mismatches, and every well-formed call the memo did not answer was answered by the jet. Five further mutations of the loop each fail test-jets.cpp.
• lake build --wfail passes. Only Trees.lean grows; no theorem changed.
• Replays with RUNNER_JETS=0: rbase and this runner take identical steps (2,124,623,037) and produce the same dump.
• arboretum build: git status --porcelain --ignore-submodules is clean. The submodules/lambada demo env-dags diff is already on main, and is identical in the base and jet builds.
• forest build: git diff --exit-code --ignore-submodules is clean.

Caveats

• Not proven; see the note at the top.
• Keyed on the exact tree: a change to spine.lamb, to the helpers it is built from (Pair, List, Snat, Option, List.concat, fix), or to the compiler silently turns the jet off. Results stay correct, but builds go back to the old speed. A canary in arboretum's CI (jets > 0 on one Certify test) would catch this; it is not part of this PR.
• A malformed spine is re-walked: when the jet returns 0, the rules redo the call and ask the jet again of each recursive call, so native work grows quadratically with the rules taken. I^4000 K over an argument list ending in a stem takes 8.4 s with the jet against 1.4 s by the rules, ×4 per doubling. spine.lamb never builds one (_whnf is private to it), and the arboretum replay never meets one (every template match was answered).
• Effect needs pin bumps: downstream builds only speed up once arboretum bumps its tree-calculus pin, and forest bumps its arboretum pin.

Merge order

• Independent of other open PRs.
• If a spine.lamb rewrite lands first (the analysis's closure/CPS idea), regenerate spineWhnf.dag before merging. The regeneration command is in implementation/lean/Cpp/README.md.

🤖 Generated with Claude Code

https://claude.ai/code/session_018ffv5AybPTpV56D5vuayQr