[adeerkhan]

Resolves #1708, #1709, #1710

The problem

On main, the C lane still evaluates these through Base's recursive definitions:

• Nat.pow scales with the exponent (a multiply and runtime call per step, even for bases 0 and 1).
• U32.log2 keeps the Base bit search in numeric folds.
• Map.msb.u walks the bits of each U32 query.

The JS lane is unchanged (it runs Base's definitions); only the C lane gains native paths.

The fix (bend2/comp.ts)

Three C-only intrinsics added to OPERATIONS (JS runs Base's), plus their C implementations in NATIVE.C:

• u32_log2: { C: "(31 - CLZ((u32)$0 | 1))" } — log2(0) stays 0, no undefined CLZ.
• nat_pow: { C: "nat_pow(e, $0, $1)" } — checked repeated squaring, using nat_mul so the 48-bit immediate wall is checked (no u64 wrap); the unused final square is skipped.
• map_msb_u: { C: "map_msb_u($0, $1)" } — CLZ-based width, clamped by the original Nat fuel; zero input / zero fuel return 0; fuel is not narrowed to U32.

GUIDE.md updated to mention the native scalar paths. Three run-lane tests added with the exact expected outputs (boundary values, two overflow cases).

Verification

• --check-only on all three new tests: ALL PROOFS CHECK.
• C lane (gcc 16, -std=c11 -O1): native_numeric_boundaries prints all 23 expected lines; nat_power_overflow / nat_power_wide_overflow print bend: a Nat past the largest immediate 2^48-1 and exit 1.
• JS lane on small_num.bend (3 values) agrees with C: 2187 / 31 / 31.
• Full tests/**.bend --check-only sweep (1661 files), before vs after: byte-identical — 588 pre-existing failures both ways, 0 new, 0 changed.
• comp.ts token count: 64,561 → still under the 66,000 cap (headroom 1,439).
• JS behavior unchanged (Base's definitions run on JS), so existing JS-lane tests are unaffected.

Notes

• The intrinsics are C-only by design, matching the existing u32_pow pattern (intr_of skips an op with no JS). JS continues to use Base's recursive definitions.
• Test expected outputs and boundary cases follow the behavior proofs in the linked issues (zero, adjacent small powers, 2^31-1, 2^31, 2^32-1, fuel 0/1/31/32/99, and two overflow boundaries).
• This change is credited to the analysis in Native Nat.pow still scales with the exponent #1708/Native Map.msb.u walks the bits of each U32 query #1709/Native U32.log2 retains the Base bit search in numeric folds #1710 (oxura).

[Lorenzobattistela]

Closing as a duplicate of #1713, which carries the same comp.ts change and tests for #1708/#1709/#1710 (and drops the GUIDE.md edit, which we don't take in PRs). Review continues there.