Speed up the interpreted matcher: VarRef byte re-check and a fused child-mask walk

[MesTTo]

Two fast paths in coreferential_transition, the interpreted matcher, byte-identical by
construction and by oracle, together 32.5% on bench process_calculus.

Re-check repeated variables by byte comparison (WAM unify_value). The matcher re-checked a
VarRef, a repeated pattern variable, by pushing the data subterm bound at the first occurrence and
re-matching it structurally, which args-decomposes the data subterm on every re-check, the
dominant matcher cost. When the bound value is ground, the re-check is now an exact byte descent:
walk the bound bytes down the trie, and the moment the data branches on a variable child, fall
back to the recursive re-match for the whole subterm. The gate is proved in
kernel/resources/formal/verus/VarRefRecheck.rs (verus, 5 verified, 0 errors): on ground data the
byte comparison equals the structural match, byte equality is always sound, and a non-ground data
position can match without byte equality, which is why the fallback keys on the data, not just the
bound value. A differential oracle (varref_fast_recheck_matches_recursive_path) runs ten
coreference programs with the fast path on and off, the non-ground witness included, and asserts
identical result sets (the fast path drops duplicate re-matches, so match counts may differ; the
sets must not).

Fuse the three child-mask passes into one word-walk. The NewVar arm read each data node's
child mask three times (and(VARS), and(SIZES), and(ARITIES)) with an iterator drain and a
byte_item re-decode per child. The fused walk reads each mask word once, in the exact
VARS -> SIZES -> ARITIES visit order (VarRefs ascending, NewVar, symbol sizes ascending, arities
ascending), taking the size or arity from the bit index itself. A second oracle
(match_any_fused_equals_three_pass) runs the fused walk against the original three-pass, which
is retained behind a cfg(test) toggle, on data mixing every child tag class at one node, and
asserts an identical result list and order.

Measured, min of 3 interleaved against the pre-change binary on one machine:

• commit 1 alone: bench process_calculus 31,526,693 -> 26,369,520 us, 16.4% faster
• both: bench process_calculus 31,461,091 -> 21,248,837 us, 32.5% faster

Byte-identical along the way: every kernel/resources program at several step depths, Nil's bfc
chainer at proof size 19 (801 steps, a 2.9M-atom space), and a 4096-hub triangle produce identical
result spaces against the pre-change binary.

The two commits stack in one PR because both rewrite arms of coreferential_transition; separate
PRs would conflict. Independent of #124 and #126 (#126 touches only expr; if this lands with it,
the wins compose).

[Adam-Vandervorst]

Hi! Appreciate your work here. The MORK kernel is closed to constant-time speed-ups until the asymptotic runtime has no known deficiencies. This prevents us from locking out much more impactful changes. Thanks for your understanding.

[MesTTo]

Closing per the same guidance: the kernel is closed to constant-time speed-ups until the asymptotic runtime has no known deficiencies. The VarRef byte re-check / fused child-mask walk is a constant-factor matcher optimization, so parking it.