Add full-precision mulDiv512 stdlib helpers

[Th0rgal]

Summary

Partially addresses #1761.

Adds proof-facing full-precision multiply-divide helpers for modeling Solidity Math.mulDiv / FullMath.mulDiv semantics without requiring the intermediate product to fit in uint256:

• mulDiv512Down? a b c
• mulDiv512Up? a b c

Both helpers compute a * b in unbounded natural-number precision and return none only when the divisor is zero or the final floor/ceil quotient exceeds MAX_UINT256.

This intentionally does not add a compiled Yul builtin yet. The docs call out that first-class compiler lowering through a 512-bit division algorithm remains the next #1761 step.

Follow-up hardening adds explicit proof regressions for MAX_UINT256 * 2 / 2, covering the core #1761 failure mode where the intermediate product exceeds 256 bits but the final quotient fits.

Latest update adds isSome / isNone iff lemmas for both floor and ceil helpers, so downstream proofs can discharge fit and rejection conditions directly instead of unpacking Option results by hand.

Validation

• lake build Verity.Stdlib.Math Verity.Proofs.Stdlib.Math
• lake build Verity.Proofs.Stdlib.Math
• lake build
• python3 scripts/generate_print_axioms.py
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• make check

---

Note

Low Risk
Adds new Stdlib.Math helper functions plus accompanying proof/automation lemmas; it does not change existing compiled arithmetic behavior, so risk is mainly API surface/lemma soundness.

Overview
Adds new Stdlib.Math APIs mulDiv512Down? and mulDiv512Up? that compute a*b/c in unbounded Nat precision and return none only on division-by-zero or when the final floor/ceil quotient exceeds MAX_UINT256.

Extends Verity/Proofs/Stdlib/Math.lean with a large lemma suite (fit/reject iff characterizations, sandwich bounds, monotonicity/antitonicity, cancellation/zero cases, ceil-vs-floor relationships, and regression proofs for wide intermediate products) and adds automation-friendly mirrors in Verity/Proofs/Stdlib/Automation.lean.

Updates generated PrintAxioms.lean counts and refreshes docs (edsl-api-reference, arithmetic profile, interpreter matrix, roadmap) to document the new full-precision modeling helpers and clarify they are not yet a compiled 512-bit Yul primitive.

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

Additional proof coverage:

• mulDiv512Up?_isSome_iff / mulDiv512Up?_isNone_iff
• floor/ceil sandwich lemmas for successful results:
  • mulDiv512Down?_mul_le
  • mulDiv512Down?_lt_succ_mul
  • mulDiv512Up?_mul_ge
  • mulDiv512Up?_mul_le_add_pred

Additional proof API parity:

• mulDiv512Down?_comm / mulDiv512Up?_comm
• zero-numerator lemmas for floor and ceil helpers
• exact same-denominator cancellation lemmas for floor and ceil helpers

Validation after latest update:

• lake build Verity.Stdlib.Math Verity.Proofs.Stdlib.Math
• lake build
• python3 scripts/generate_print_axioms.py --check
• git diff --check

[Th0rgal]

Latest update (1a1e223b) adds Verity.Proofs.Stdlib.Automation fit/rejection iff lemmas for mulDiv512Down? and mulDiv512Up?, updates the arithmetic profile, and refreshes PrintAxioms.lean.

Local validation:

• lake build Verity.Proofs.Stdlib.Automation Verity.Stdlib.Math Verity.Proofs.Stdlib.Math
• lake build
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• make check

[Th0rgal]

Latest update adds full-precision ceil/floor exactness lemmas:

• mulDiv512Up?_eq_down_of_dvd
• mulDiv512Up?_some_succ_of_not_dvd

These mirror the existing 256-bit mulDivUp/mulDivDown divisibility proof shape for the new mulDiv512 helpers.

Validation after this update:

• lake build Verity.Proofs.Stdlib.Math
• lake build Verity.Stdlib.Math Verity.Proofs.Stdlib.Math Verity.Proofs.Stdlib.Automation
• lake build
• python3 scripts/generate_print_axioms.py
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• make check

[Th0rgal]

Docs/API-reference follow-up after reviewing the mulDiv512 surface:

• Added a dedicated docs-site API section for mulDiv512Down? / mulDiv512Up?.
• Listed the fit/rejection, result-characterization, sandwich, rounding/shape, and automation theorem groups so downstream users can discover the new proof API from the public reference.

Validation passed locally:

• git diff --check
• lake build Verity.Stdlib.Math Verity.Proofs.Stdlib.Math Verity.Proofs.Stdlib.Automation

[Th0rgal]

Full local validation after the docs-site API reference update also passed:

• make check

[Th0rgal]

Latest update (e8256882) adds full-precision ceil/floor rounding-gap lemmas for successful mulDiv512 results:

• mulDiv512Down?_le_up
• mulDiv512Up?_le_down_add_one
• mulDiv512Up?_eq_down_or_succ

This gives the new 512-bit proof helpers the same one-step ceil/floor shape already available for the existing 256-bit mulDiv helpers. Docs/API references and PrintAxioms.lean were updated.

Local validation passed:

• lake build Verity.Proofs.Stdlib.Math
• lake build
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• make check

[Th0rgal]

Latest update (6011197a) adds successful-result numerator monotonicity lemmas for the full-precision helpers:

• mulDiv512Down?_monotone_left
• mulDiv512Down?_monotone_right
• mulDiv512Up?_monotone_left
• mulDiv512Up?_monotone_right

This brings the new mulDiv512...? proof surface closer to the existing 256-bit mulDiv monotonicity API while preserving the Option success boundary. Docs/API references and PrintAxioms.lean were updated.

Local validation passed:

• lake build Verity.Proofs.Stdlib.Math
• lake build
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• make check

[Th0rgal]

Latest update (3a4f3fd6) adds successful-result divisor antitonicity lemmas for the full-precision helpers:

• mulDiv512Down?_antitone_divisor
• mulDiv512Up?_antitone_divisor

This fills the corresponding 512-bit proof API gap next to the existing numerator monotonicity lemmas and mirrors the divisor-antitone shape already available for the 256-bit mulDiv helpers. Docs/API references and PrintAxioms.lean were updated.

Local validation passed:

• lake build Verity.Proofs.Stdlib.Math
• lake build
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• make check

[Th0rgal]

Latest update (c97715a9) adds ceil/floor bridge lemmas for the full-precision helpers:

• mulDiv512Down?_isSome_of_up_isSome: if the rounded-up quotient fits, the floor quotient also fits.
• mulDiv512Up?_isNone_of_down_isNone: if the floor quotient is rejected, the rounded-up quotient is rejected too.

These avoid re-proving the shared quotient-fit boundary when downstream proofs move between mulDiv512Up? and mulDiv512Down?. Docs/API references and PrintAxioms.lean were updated.

Local validation passed:

• lake build Verity.Proofs.Stdlib.Math
• python3 scripts/generate_print_axioms.py
• lake build
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• make check

[Th0rgal]

Follow-up (474caa02) addresses Bugbot's API symmetry finding:

• Removed the redundant (c₁ : Nat) ≠ 0 argument from mulDiv512Down?_antitone_divisor.
• The floor antitonicity lemma now derives divisor nonzero from its successful mulDiv512Down? ... = some ... hypothesis, matching the ceil antitonicity lemma shape.

Validation after this fix passed locally:

• lake build Verity.Proofs.Stdlib.Math
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• make check

[Th0rgal]

Latest update (5c927b7c) adds full-precision positivity lemmas for successful mulDiv512 results:

• mulDiv512Down?_pos: floor result is positive once the exact product reaches at least one divisor-width.
• mulDiv512Up?_pos: ceil result is positive when both numerator factors are positive.

This closes the remaining API parity gap with the existing 256-bit mulDivDown_pos / mulDivUp_pos proof surface. Docs/API references and PrintAxioms.lean were updated.

Local validation passed:

• lake build Verity.Proofs.Stdlib.Math
• lake build
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• make check

[Th0rgal]

Latest update (0863e032) adds compatibility bridge lemmas between the new full-precision helpers and the existing 256-bit helper API:

• mulDiv512Down?_eq_mulDivDown_of_no_overflow
• mulDiv512Up?_eq_mulDivUp_of_no_overflow

These prove the new Option-returning 512-bit helpers agree with mulDivDown / mulDivUp under the older no-overflow preconditions, giving downstream proofs an incremental migration path. Docs/API references and PrintAxioms.lean were updated.

Local validation passed:

• lake build Verity.Proofs.Stdlib.Math
• lake build
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• make check

[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 0863e03. Configure here.}

[Th0rgal]

Latest update (46ac5614) adds concrete final-overflow regressions for the full-precision helpers:

• mulDiv512Down?_final_overflow_regression
• mulDiv512Up?_final_overflow_regression

These pin the opposite boundary from the existing wide-product fitting regressions: a 512-bit product may exceed 256 bits, but the helper still rejects when the final floor/ceil quotient is above MAX_UINT256 instead of wrapping.

Local validation passed:

• lake build Verity.Proofs.Stdlib.Math
• lake build
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• make check

[Th0rgal]

Follow-up (b8fa0ec1) addresses Bugbot's bridge theorem consistency finding:

• Changed mulDiv512Up?_eq_mulDivUp_of_no_overflow to take (c : Nat) ≠ 0, matching mulDiv512Down?_eq_mulDivDown_of_no_overflow and the rest of the new mulDiv512 proof API.
• Kept the existing mulDivUp_nat_eq call by deriving the needed Uint256-level nonzero proof internally.

Validation after this fix passed locally:

• lake build Verity.Proofs.Stdlib.Math
• lake build
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• make check

[Th0rgal]

Latest update (e35aeba4) adds one-divisor error-bound convenience lemmas for successful full-precision results:

• mulDiv512Down?_mul_lt_add
• mulDiv512Up?_mul_lt_add

These mirror the existing 256-bit mulDivDown_mul_lt_add / mulDivUp_mul_lt_add proof API shape while reusing the stronger mulDiv512 sandwich lemmas. Docs/API references and PrintAxioms.lean were updated.

Local validation passed:

• lake build Verity.Proofs.Stdlib.Math
• lake build
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• make check