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

[olydis]

Draft: this jet has no proof. runtimeJets_sound covers skip_line's jet only. The only evidence that this jet answers what its tree does is the differential tests and the identical replays below. Proof plan: the same machinery #63 needs (a Lean model of the loop, plus call/return verdicts and typed splits in Check.lean's explore). The induction is different: it runs on (fuel, size q) lexicographically, because _normalize recurses on f and x without spending fuel.

What changes

EagerGraphNilMmap32Jets now answers arboretum's Quoted._normalize (src/quoted/eval.lamb) natively, together with the _apply_nf and _classify it calls. This is the budgeted applicative-order normalizer behind Certify.Size's _eagerly.

• Tree: trees/quotedNormalize.dag is Quoted._normalize:6 at arboretum e3df589. Forest's pinned arboretum (c8bcaf5) has the same md5. embed.mjs regenerates jets.hpp and Jets/Trees.lean. Trees.lean renumbers its shared definitions because the new file sorts before skipLine.
• Key: _normalize fuel has the shape △(△x)y. y is a 464-node tree that is the same for every fuel; the fuel sits at 3 places inside x.
  • In the S-rule branch, after recall(), one compare y == Y gates a template match, and the match recovers the fuel.
  • The template comes from the new jets::Partial. On every clear() it reduces f △ and f (△△) by the rules and diffs the two results. It throws if the fuel appears anywhere other than as-is.
• Native loop (jets::QuotedNormalize, in the new eager-graph-nil-mmap-32-jets.hpp):
  • It applies eval.lamb's rules over quoted terms on explicit task and value stacks, so nesting costs heap, not C stack.
  • Fuel threads through in Option.bind order, and the first none is the answer.
  • If the fuel turns out not to be a Snat at a point where a rule needs a unit, the jet returns 0 and the rules take over.
  • Within a call, it remembers the normal form of every subterm that spent no fuel. A DAG-shared term is therefore walked as a DAG, as the rules' memo would walk it.
• Memo and stats: the answer goes into the memo through remember(), which skip_line now uses too. RUNNER_STATS counts it in jets=. With RUNNER_JETS=0, nothing is keyed.

Measured effect

All runs on the same machine, back to back. Step counts are deterministic for a given configuration; wall-time differences are within run-to-run noise.

Replay: one runner loads the build's whole canonical bundle, with every expect test, then dumps it. Dumps are byte-identical in every run. Steps saved (negative means fewer steps):

collection budget (RUNNER_RSS_THRESHOLD_MB)	448	512 (default)	576	none (4096)
arboretum, main → this	−14.8M	−10.5M	−104.2M	−67.5M (−4.2%)
forest, main → this	−19.7M	−25.0M	−26.1M	−64.6M (−2.9%)
arboretum, #63 → #63 + this	−60.0M	−127.1M	−56.9M	−49.5M (−6.5%)
forest, #63 → #63 + this	−65.2M	−0.9M	+120.3M	−52.3M (−4.1%)

• Bases at 512 MB / with no collections: main is arboretum 2,126.2M / 1,595.7M and forest 2,970.5M / 2,212.4M. eager: answer Quoted._whnf natively, a jet not yet proven #63 is 842.7M / 756.8M and 1,529.8M / 1,283.2M.
• eager: answer Quoted._whnf natively, a jet not yet proven #63 + this at 384 and 640 MB: arboretum −81.4M and −57.6M; forest +8.3M and −72.1M.
• The analysis estimated 62M on top of eager: answer Quoted._whnf natively, a jet not yet proven #63. Without collections I measured 49.5M (arboretum) and 52.3M (forest).
• Review re-run: arboretum at 512 and 4096 MB and forest at 4096 MB reproduce to the step (−10.5M, −67.5M, −64.6M), with the same dumps; the jet fires about 1,000 times per replay.

Builds from empty caches (4 test threads, RUNNER_STATS=1, steps summed over every runner command):

	main	this	#63	#63 + this
arboretum ./build.sh, steps	2,375.8M / 2,343.5M	2,147.2M / 2,062.1M	986.2M / 1,069.9M / 995.5M	998.3M / 996.6M / 986.7M
arboretum, wall	60.7 / 68.2 s	60.5 / 62.0 s	38.9 / 42.1 / 39.2 s	43.4 / 40.1 / 41.7 s
arboretum, review re-run, steps	2,249.4M / 2,262.2M	2,191.9M / 2,123.8M
arboretum, review re-run, wall	64.5 / 64.6 s	65.7 / 59.3 s
forest ./build/full.sh, steps	3,242.6M	3,018.3M	1,628.3M / 1,823.7M	1,783.8M / 1,769.7M
forest, wall	133.9 s	127.4 s	107.6 / 111.3 s	113.9 / 112.9 s

Build step counts vary between identical runs: two identical #63 builds differ by up to 195M steps. The review re-run (order base, this, this, base) saves 58M and 138M steps (mean 98M), against 229M and 281M in the first pairs. On top of #63, the build-level effect is within noise.

Idle cost, measured by compiling compiler.lamb, where the jet never fires (GCC 13, -O3):

• Instructions go from 794.4M to 823.4M (+3.6%).
• The S-branch compare accounts for +0.7%: a variant that never keys runs 800.0M.
• Keying costs 1.5M instructions per clear().
• The remaining ~2% is code generation, not the arena. Partial::key calls apply() on an evaluator that GCC cannot prove is the runner's global. GCC therefore emits a generic apply() beside the constprop clone the runner runs, and the clone shrinks from 0x124f to 0xf76 bytes because less gets inlined into it.
  • Shifting the arena by 500–3,000 nodes on main changes instructions by −0.15% to −0.34%.
  • Resetting the memo after keying changes nothing.
  • noinline or always_inline on the keying path does not remove the generic copy.
  • eager: answer Quoted._whnf natively, a jet not yet proven #63 keys the same way.
• Wall time: author 0.429 vs 0.454 s (mean of 5); review 354 ± 41 vs 363 ± 38 ms, medians 352.5 vs 348.5 ms (20 alternating runs). Both are within noise.

Validation

• implementation/cpp/dag-machine/test.sh passes under LC_ALL=C and LC_ALL=C.UTF-8: 35 PASS each, runner 21/21.
• New checks in test-jets.cpp:
  • Differential against the evaluator without jets: 600 terms (I-chains, Ω = δδ, and pseudo-random applications of △, variables, K, I, δ and △(△ w x)). Each term runs at every fuel from 0 to one past where it runs out, capped at 48. That is 5,346 calls, 4,538 of which run out of fuel, using up to 46 rules. The jet answers every call, and every answer equals the rules'. Every rule branch fires: rule 1 23k times, rule 2 31k, rule 3 on △ / △u / △uv 243 / 1.6k / 2.0k, stuck 1.6k.
  • Fuel that is not a Snat (a fork 0–7 units down): the jet either answers or leaves the call to the rules, and the result is equal either way.
  • A forged partial with two fuels in it is left to the rules.
  • A 40-deep DAG (2^40 subterms as a tree) is answered at once.
  • The memo answers the jet's call again.
  • 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 differentials, outside the suite, all equal to the rules:
  • 23,300 calls over 2,330 distinct terms that mix quoted random trees, variables of any shape, K, I, δ and compositions of them, at fuels 0, 1, 2, 3, 5, 8, 13, 50, 200 and 1000 (Certify.Size's budget).
  • 9,080 of those calls again under a 1,024-node collection budget (12 collections).
  • 3,000 calls with random trees as fuel; the jet answers 2,126 of them.
• Mutation check: 18 hand mutations each fail a check; 3 of them fail by hanging. They cover the loop (every rule's operands, task order, the stuck test, the fuel decline, the memo condition, the classification), the template match, and remember().
• lake build --wfail passes. Only Trees.lean changes; no theorem changed.
• arboretum ./build.sh from empty caches on this tree (author 2×, review 2×): git status --porcelain --ignore-submodules is clean, and the submodules/lambada diff is identical to main's run (md5 09cfb412).
• forest ./build/full.sh: git diff --exit-code --ignore-submodules is clean.

Caveats

• Unproven; see the note at the top.
• Small and noisy.
  • Arboretum saves steps in every configuration measured.
  • Forest saves steps when the jet stands alone. On top of eager: answer Quoted._whnf natively, a jet not yet proven #63 at realistic budgets it does not save reliably (+120M to −72M), because collections and the memo's heuristics rearrange more than the 50M this jet removes.
  • Wall time does not resolve in any build.
• Keyed on the exact tree: a change to eval.lamb, to its helpers (Option, Pair, Snat.match, fix, the quoting in reflect/quote.lamb), or to the compiler turns the jet off silently. Results stay correct; only the speedup is lost.
• Idle cost: +3.6% instructions where the jet never fires, mostly from code generation (see above). eager: answer Quoted._whnf natively, a jet not yet proven #63 reports the same figure.
• Pin bumps needed: downstream builds only change once arboretum and forest bump their pins.

Overlap and merge order

• Independent: branches from main, and builds and passes without eager: answer Quoted._whnf natively, a jet not yet proven #63.
• Intended order: after eager: answer Quoted._whnf natively, a jet not yet proven #63. The measurements above show where it helps most.
• Shared with eager: answer Quoted._whnf natively, a jet not yet proven #63, in identical text, so those hunks merge as-is:
  • remember() (eager: Nat.divmod__fastest as a jet #62 and eager: Nat.add and Nat.mul as jets #65 add the same helper as answered());
  • test-jets.cpp's tree(), snat(), kids() and copy();
  • the header of eager-graph-nil-mmap-32-jets.hpp. It says the file uses nothing but the evaluator's arena, stem() and fork(), but keying also calls apply() and roots(). Whichever PR lands second should correct it.
• Checked by cherry-picking onto eager: answer Quoted._whnf natively, a jet not yet proven #63: conflicts are limited to each jet's own lines (members, keying, mark, S-branch hook, test bodies, docs, generated files). With those resolved, the combined test-jets.cpp passes all 14 checks.
• Left for the second PR to land: jets::Partial is eager: answer Quoted._whnf natively, a jet not yet proven #63's SpineWhnf::key() / fuel_of(), lifted out and generalized to holes on either side. Whichever PR lands second should move SpineWhnf onto it, adding a left() twin of right(), so the template code exists once, then rerun embed.mjs.

🤖 Generated with Claude Code

https://claude.ai/code/session_018ffv5AybPTpV56D5vuayQr