Support safeMul require lowering

[Th0rgal]

Summary

Partially addresses #1752.

Stdlib.Math.safeMul and Stdlib.Math.safeDiv already exist and the executable path can use requireSomeUint (...), but verity_contract only accepted safeAdd and safeSub in its compiled requireSomeUint translator. This PR closes that inconsistency for checked multiplication and division:

• accepts safeMul and safeDiv in requireSomeUint bind type inference
• lowers requireSomeUint (safeMul a b) "..." to an explicit overflow guard before binding the product
• uses the standard EVM multiplication check b == 0 || (a * b) / b == a
• lowers requireSomeUint (safeDiv a b) "..." to an explicit b != 0 guard before binding the quotient
• adds smoke coverage, compilation-model regressions for safeAdd/safeSub/safeMul/safeDiv lowering shapes, invariant/round-trip coverage, and generated property artifact coverage
• documents that safeAdd / safeSub / safeMul / safeDiv are all supported through requireSomeUint

This does not change bare add / sub / mul / div; those remain wrapping/EVM arithmetic, so #1752 remains open for the broader Solidity-0.8 default-semantics question.

Validation

• lake build Contracts.Smoke Compiler.CompilationModelFeatureTest Contracts.MacroTranslateInvariantTest Contracts.MacroTranslateRoundTripFuzz
• python3 scripts/check_macro_health.py
• make check
• git diff --check

---

Note

Medium Risk
Extends verity_contract macro translation to new arithmetic forms, affecting generated require guards and thus compiled runtime behavior for contracts using checked mul/div. Risk is moderate due to potential edge cases in overflow/zero-check lowering, but changes are localized and covered by new smoke/invariant tests and docs updates.

Overview
Adds verity_contract support for binding requireSomeUint (safeMul ...) and requireSomeUint (safeDiv ...), extending the existing checked safeAdd/safeSub lowering.

The macro translator now typechecks these bind sources and lowers them to explicit compiled require guards: mul uses the standard b == 0 || (a*b)/b == a overflow check, and div requires b != 0 before computing the quotient.

Introduces a new SafeMulRequireSmoke contract plus compilation-model and macro invariant/round-trip coverage, adds a generated Solidity property-test stub artifact, and updates docs to document the expanded checked-arithmetic lowering behavior.

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

[Th0rgal]

Latest update (baf262eb) aligns the Solidity-to-Verity migration guide with the new requireSomeUint lowering surface:

• added checked * and / translation rows using safeMul and safeDiv
• updated the checked-vs-wrapping arithmetic pitfall to list all four supported safe helpers

Local validation passed:

• git diff --check
• npm ci (docs-site dependencies)
• npm run build from docs-site