Add mulDiv512Down / mulDiv512Up codegen with FullMath Yul helper (#1761)

[Th0rgal]

Summary

Closes the codegen gap on #1761: Verity's existing mulDivDown / mulDivUp lower to div(mul(a, b), c), which truncates the intermediate product to 256 bits. That does not faithfully model Solidity libraries such as OpenZeppelin Math.mulDiv / Solmate FullMath.mulDiv, where the intermediate product is handled at full precision and may exceed 2^256 as long as the final quotient fits.

The proof-side mulDiv512Down? / mulDiv512Up? Lean helpers already capture the correct spec (the issue's "proof-side shipped" reference); this PR adds the matching compiler-side surface and a FullMath-style Yul helper so contract authors can write mulDiv512Down a b c directly inside a verity_contract body.

Fixes #1761.

What lands

• Expr.mulDiv512Down / Expr.mulDiv512Up constructors.
• Yul helpers __verity_full_mul_div (down) and __verity_full_mul_div_up (up) implementing the OpenZeppelin / Solmate FullMath.mulDiv algorithm:
  • 512-bit product via the mulmod identity.
  • Short-circuit to div(prod0, denominator) when prod1 == 0.
  • 512-by-256 division via Hensel-lifted modular inverse after factoring out powers of two from the denominator.
  • _up variant adds 1 when mulmod(a, b, c) != 0.
  • Both revert on denominator == 0 and on quotient overflow.
• Lowering in ExpressionCompile.lean, helper-emission gating via a new contractUsesMulDiv512 detector in UsageAnalysis.lean, threaded through Dispatch.compileValidatedCore and ValidationCalls.reservedExternalNames / firstReservedExternalCollision.
• Case-handler updates in every existing Expr traversal that already handles mulDivDown / mulDivUp: LogicalPurity (incl. the duplication-safe mulDivUp analogue for mulDiv512Up), UsageAnalysis (4 walk sites + 3 detectors), Validation (incl. an explicit-leaves expansion of exprHasUntrackableWrites to escape the Lean 4 _mutual.eq_def heartbeat ceiling that new constructors keep tripping), ValidationCalls (2 sites), ValidationInterop, ValidationHelpers, ScopeValidation (separate arms — mulDiv512Up inherits the c-duplication purity guard from mulDivUp), TrustSurface (5 sites), ExpressionCompile.
• Macro routing: mulDiv512Down a b c / mulDiv512Up a b c type-check as Uint256 with word-like operands.
• Verity.Stdlib.Math.mulDiv512Down / mulDiv512Up — Uint256-valued Lean defs via the existing Option Uint256 proof helpers with a 0 fallback on none. The fallback is unreachable at runtime because the IR reverts on the same boundary; the def exists so the macro identifier resolves at the Lean level.

Smoke + invariant + property-test coverage

• Contracts.Smoke.MulDiv512Smoke exercises both operators with three-arg storage-bound functions.
• Registered in MacroTranslateInvariantTest (spec list, function signatures, selectors) and MacroTranslateRoundTripFuzz (spec list).
• Auto-generated Foundry property stub at artifacts/macro_property_tests/PropertyMulDiv512Smoke.t.sol.

Test plan

• lake build succeeds (all 105 targets).
• make check passes locally (macro health, IR/Yul identity diff, selector audit, property-test artifacts).
• Hensel-lifted inverse is correct: starts from a 4-bit seed (xor(2, mul(3, d))) and seven inverse := mul(inverse, sub(2, mul(d, inverse))) rounds raise precision through 8, 16, 32, 64, 128, 256 bits — matching OpenZeppelin's Math.mulDiv reference implementation.

Scope

No new axiom, no new trust assumption — the Yul helper is local arithmetic over mulmod / mul / div / sub / and / or / xor. AUDIT.md / AXIOMS.md / TRUST_ASSUMPTIONS.md unaffected. Faithfulness to the proof-side mulDiv512Down? / mulDiv512Up? spec is the standard yul-against-stdlib bridge that the existing mulDivDown / mulDivUp rely on.

Downstream

Concrete blocker referenced in the issue: Cork Phoenix unwindExerciseOther (contracts/libraries/MathHelper.sol / PoolLib.sol) — assetsInWithoutFee = normalizedReferenceAsset.mulDiv(swapRate, 1e18, Math.Rounding.Ceil) no longer needs the hNoOvf3 : normalizedReferenceAsset * swapRate.val < modulus workaround hypothesis. The verity-benchmark Cork case can be re-modeled with mulDiv512Up / mulDiv512Down directly against the upstream Solidity source.

🤖 Generated with Claude Code

---

Note

Medium Risk
Adds new arithmetic primitives and emits new Yul helper functions used in contract codegen, affecting core expression compilation and validation paths; mistakes could cause incorrect math or unexpected reverts.

Overview
Adds new Expr.mulDiv512Down / Expr.mulDiv512Up operations that compile to OpenZeppelin/Solmate-style 512-bit-precision multiply-divide via new Yul helpers __verity_full_mul_div and __verity_full_mul_div_up (with revert-on-/0 and quotient overflow behavior).

Threads support end-to-end: macro translation/typechecking, expression compilation, reserved-name collision checks, helper emission gating via contractUsesMulDiv512, and updates to purity/scope/validation/trust-surface traversals to understand the new Expr variants.

Adds a new smoke contract MulDiv512Smoke and registers it in invariant/fuzz test harnesses, plus an autogenerated Foundry property-test stub.

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

[github-actions]

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

[cursor]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit f1bbf70. Configure here.}