Add Uint256 pow macro lowering

[Th0rgal]

Summary

Closes #1759.

Adds Uint256.pow / a ^ b support for decimal exponentiation without adding a new CompilationModel expression constructor:

• defines EVM-style modular Uint256.pow plus HPow/Pow instances
• lowers macro-level pow a b and a ^ b to a reserved compiler builtin
• compiles that reserved builtin directly to Yul/EVM exp(a, b)
• treats the reserved builtin as pure arithmetic, not as a linked external/trust boundary
• adds smoke and feature coverage plus arithmetic docs

Validation

• lake build Verity.Core.Uint256 Verity.EVM.Uint256 Compiler.CompilationModel.ExpressionCompile Verity.Macro.Translate Contracts.Smoke Compiler.CompilationModelFeatureTest
• lake build Compiler
• lake build
• python3 scripts/generate_print_axioms.py --check
• git diff --check

Note: lake build Compiler still reports the pre-existing unnecessary simpa warnings in Compiler/Proofs/IRGeneration/ContractFeatureTest.lean.

---

Note

Medium Risk
Adds new arithmetic operator lowering that changes how Expr.externalCall is compiled/validated and how purity/external-interaction checks classify a reserved name; mistakes could misclassify real externals or generate wrong Yul exp calls.

Overview
Adds EVM-style modular exponentiation to the EDSL (Uint256.pow and a ^ b) and lowers it through macros to a reserved external-call name builtinExpName.

Updates compilation and analysis so that Expr.externalCall builtinExpName [...] compiles directly to Yul exp(base, exponent) (with arity checks) and is treated as pure arithmetic (excluded from call-like/external-interaction/state read-write detection and from trust-surface linked-externals reporting).

Extends validation to reserve the builtin name against user externals shadowing, and adds smoke tests/contracts, generated Solidity property stubs, and docs/feature-matrix updates covering pow.

^{Reviewed by Cursor Bugbot for commit 3920322. Bugbot is set up for automated code reviews on this repo. Configure here.}

[github-actions]

\n### CI Failure Hints\n\nFailed jobs: `compiler-audits`, `compiler-regressions`, `foundry`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n```