From 37b145cc890d04f607e4752215beed0e522eb6db Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 01:04:20 +0200
Subject: [PATCH 01/18] Add full-precision mulDiv512 stdlib helpers

---
 PrintAxioms.lean                   | 10 +++-
 Verity/Proofs/Stdlib/Math.lean     | 81 ++++++++++++++++++++++++++++++
 Verity/Stdlib/Math.lean            | 46 +++++++++++++++++
 docs/ARITHMETIC_PROFILE.md         | 14 +++++-
 docs/INTERPRETER_FEATURE_MATRIX.md |  1 +
 docs/ROADMAP.md                    |  3 ++
 6 files changed, 153 insertions(+), 2 deletions(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index 1a85e0d5f..123e42ec1 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -572,6 +572,14 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Verity/Proofs/Stdlib/Math.lean
 -- #print axioms Verity.Proofs.Stdlib.Math.modulus_eq_max_succ  -- private
 -- #print axioms Verity.Proofs.Stdlib.Math.lt_modulus_of_le_max  -- private
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_some
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_none_of_zero_divisor
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_none_of_overflow
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_eq_some_iff
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_some
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_none_of_zero_divisor
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_none_of_overflow
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_eq_some_iff
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_nat_eq
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_mul_le
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_pos
@@ -3799,4 +3807,4 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Compiler/Proofs/YulGeneration/ReferenceOracle/Semantics.lean
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_sender
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
--- Total: 3623 theorems/lemmas (2677 public, 946 private, 0 sorry'd)
+-- Total: 3631 theorems/lemmas (2685 public, 946 private, 0 sorry'd)
diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index 494282a46..15dc76b4b 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -26,6 +26,87 @@ private theorem lt_modulus_of_le_max {n : Nat} (h : n ≤ MAX_UINT256) :
     n < MAX_UINT256 + 1 := Nat.lt_succ_of_le h
     _ = Verity.Core.Uint256.modulus := by simp [modulus_eq_max_succ]
 
+/-! ## Full-precision mulDiv512 helpers -/
+
+/-- `mulDiv512Down?` returns the exact full-precision floor quotient when it fits. -/
+theorem mulDiv512Down?_some (a b c : Uint256)
+    (hC : (c : Nat) ≠ 0)
+    (hFit : ((a : Nat) * (b : Nat)) / (c : Nat) ≤ MAX_UINT256) :
+    mulDiv512Down? a b c =
+      some (Verity.Core.Uint256.ofNat (((a : Nat) * (b : Nat)) / (c : Nat))) := by
+  simp [Verity.Stdlib.Math.mulDiv512Down?, hC, Nat.not_lt.mpr hFit]
+
+/-- `mulDiv512Down?` rejects a zero divisor. -/
+theorem mulDiv512Down?_none_of_zero_divisor (a b c : Uint256)
+    (hC : (c : Nat) = 0) :
+    mulDiv512Down? a b c = none := by
+  simp [Verity.Stdlib.Math.mulDiv512Down?, hC]
+
+/-- `mulDiv512Down?` rejects a quotient that does not fit in `uint256`. -/
+theorem mulDiv512Down?_none_of_overflow (a b c : Uint256)
+    (hC : (c : Nat) ≠ 0)
+    (hOverflow : MAX_UINT256 < ((a : Nat) * (b : Nat)) / (c : Nat)) :
+    mulDiv512Down? a b c = none := by
+  simp [Verity.Stdlib.Math.mulDiv512Down?, hC, hOverflow]
+
+/-- The quotient returned by `mulDiv512Down?` is the full-precision natural quotient. -/
+theorem mulDiv512Down?_eq_some_iff (a b c out : Uint256) :
+    mulDiv512Down? a b c = some out ↔
+      (c : Nat) ≠ 0 ∧
+      ((a : Nat) * (b : Nat)) / (c : Nat) ≤ MAX_UINT256 ∧
+      Verity.Core.Uint256.ofNat (((a : Nat) * (b : Nat)) / (c : Nat)) = out := by
+  by_cases hC : (c : Nat) = 0
+  · simp [Verity.Stdlib.Math.mulDiv512Down?, hC]
+  · by_cases hOverflow : ((a : Nat) * (b : Nat)) / (c : Nat) > MAX_UINT256
+    · have hNotFit : ¬((a : Nat) * (b : Nat)) / (c : Nat) ≤ MAX_UINT256 := by
+        exact Nat.not_le_of_gt hOverflow
+      simp [Verity.Stdlib.Math.mulDiv512Down?, hC, hOverflow, hNotFit]
+    · have hFit : ((a : Nat) * (b : Nat)) / (c : Nat) ≤ MAX_UINT256 := Nat.le_of_not_gt hOverflow
+      simp [Verity.Stdlib.Math.mulDiv512Down?, hC, hOverflow, hFit]
+
+/-- `mulDiv512Up?` returns the exact full-precision ceil quotient when it fits. -/
+theorem mulDiv512Up?_some (a b c : Uint256)
+    (hC : (c : Nat) ≠ 0)
+    (hFit : (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) ≤ MAX_UINT256) :
+    mulDiv512Up? a b c =
+      some (Verity.Core.Uint256.ofNat ((((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat))) := by
+  simp [Verity.Stdlib.Math.mulDiv512Up?, hC, Nat.not_lt.mpr hFit]
+
+/-- `mulDiv512Up?` rejects a zero divisor. -/
+theorem mulDiv512Up?_none_of_zero_divisor (a b c : Uint256)
+    (hC : (c : Nat) = 0) :
+    mulDiv512Up? a b c = none := by
+  simp [Verity.Stdlib.Math.mulDiv512Up?, hC]
+
+/-- `mulDiv512Up?` rejects a rounded-up quotient that does not fit in `uint256`. -/
+theorem mulDiv512Up?_none_of_overflow (a b c : Uint256)
+    (hC : (c : Nat) ≠ 0)
+    (hOverflow : MAX_UINT256 <
+      (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat)) :
+    mulDiv512Up? a b c = none := by
+  simp [Verity.Stdlib.Math.mulDiv512Up?, hC, hOverflow]
+
+/-- The quotient returned by `mulDiv512Up?` is the full-precision rounded-up quotient. -/
+theorem mulDiv512Up?_eq_some_iff (a b c out : Uint256) :
+    mulDiv512Up? a b c = some out ↔
+      (c : Nat) ≠ 0 ∧
+      (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) ≤ MAX_UINT256 ∧
+      Verity.Core.Uint256.ofNat ((((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat)) = out := by
+  by_cases hC : (c : Nat) = 0
+  · simp [Verity.Stdlib.Math.mulDiv512Up?, hC]
+  · by_cases hOverflow :
+        (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) > MAX_UINT256
+    · have hNotFit :
+          ¬((((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) ≤ MAX_UINT256) := by
+        exact Nat.not_le_of_gt hOverflow
+      simp [Verity.Stdlib.Math.mulDiv512Up?, hC, hOverflow, hNotFit]
+    · have hFit :
+          (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) ≤ MAX_UINT256 :=
+        Nat.le_of_not_gt hOverflow
+      simp [Verity.Stdlib.Math.mulDiv512Up?, hC, hOverflow, hFit]
+
+/-! ## mulDiv / wad helpers -/
+
 /-- `mulDivDown` agrees with exact natural-number division when the numerator does not wrap. -/
 theorem mulDivDown_nat_eq (a b c : Uint256) (hMul : (a : Nat) * (b : Nat) ≤ MAX_UINT256) :
     (mulDivDown a b c : Nat) =
diff --git a/Verity/Stdlib/Math.lean b/Verity/Stdlib/Math.lean
index c686c8262..c99d2aa7f 100644
--- a/Verity/Stdlib/Math.lean
+++ b/Verity/Stdlib/Math.lean
@@ -60,6 +60,32 @@ def mulDivDown (a b c : Uint256) : Uint256 :=
 def mulDivUp (a b c : Uint256) : Uint256 :=
   ((a * b) + (c - 1)) / c
 
+/-- Full-precision floor multiply-divide.
+
+Unlike `mulDivDown`, this computes the product in unbounded natural-number
+precision and returns `none` only when the divisor is zero or the final quotient
+does not fit in `uint256`. This matches the proof shape needed for Solidity
+`Math.mulDiv(..., Rounding.Floor)` / `FullMath.mulDiv` modeling without adding
+an artificial no-overflow hypothesis on `a * b`. -/
+def mulDiv512Down? (a b c : Uint256) : Option Uint256 :=
+  if (c : Nat) = 0 then
+    none
+  else
+    let q := ((a : Nat) * (b : Nat)) / (c : Nat)
+    if q > MAX_UINT256 then none else some (Core.Uint256.ofNat q)
+
+/-- Full-precision ceil multiply-divide.
+
+The product is computed in unbounded natural-number precision. The helper
+returns `none` when the divisor is zero or the rounded-up quotient does not fit
+in `uint256`. -/
+def mulDiv512Up? (a b c : Uint256) : Option Uint256 :=
+  if (c : Nat) = 0 then
+    none
+  else
+    let q := (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat)
+    if q > MAX_UINT256 then none else some (Core.Uint256.ofNat q)
+
 /-- `ceilDiv(a, b)` = `ceil(a / b)`, matching Solidity's Math256.ceilDiv / OpenZeppelin.
     Uses the overflow-safe formula: `a == 0 ? 0 : (a - 1) / b + 1`.
     Note: When `b = 0` and `a > 0`, EVM `DIV` returns 0, so this yields 1.
@@ -115,6 +141,26 @@ theorem WAD_ne_zero : WAD ≠ 0 := by
 @[simp] theorem mulDivUp_def (a b c : Uint256) :
   mulDivUp a b c = ((a * b) + (c - 1)) / c := rfl
 
+@[simp] theorem mulDiv512Down?_def (a b c : Uint256) :
+  mulDiv512Down? a b c =
+    if (c : Nat) = 0 then
+      none
+    else
+      let q := ((a : Nat) * (b : Nat)) / (c : Nat)
+      if q > MAX_UINT256 then none else some (Core.Uint256.ofNat q) := by
+  unfold mulDiv512Down?
+  split <;> rfl
+
+@[simp] theorem mulDiv512Up?_def (a b c : Uint256) :
+  mulDiv512Up? a b c =
+    if (c : Nat) = 0 then
+      none
+    else
+      let q := (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat)
+      if q > MAX_UINT256 then none else some (Core.Uint256.ofNat q) := by
+  unfold mulDiv512Up?
+  split <;> rfl
+
 @[simp] theorem wMulDown_def (a b : Uint256) :
   wMulDown a b = mulDivDown a b WAD := rfl
 
diff --git a/docs/ARITHMETIC_PROFILE.md b/docs/ARITHMETIC_PROFILE.md
index 189eb1347..86b72a0cf 100644
--- a/docs/ARITHMETIC_PROFILE.md
+++ b/docs/ARITHMETIC_PROFILE.md
@@ -61,6 +61,11 @@ Beyond the 15 low-level builtins, the `ExprCompileCore` proven fragment includes
 
 These proofs are in `Compiler/Proofs/IRGeneration/FunctionBody.lean` and cover both IR compilation correctness and end-to-end evaluation semantics.
 
+The compiled `mulDivDown` / `mulDivUp` operators still use 256-bit EVM
+multiplication before division. They are suitable for fixed-point code whose
+product is known to fit in `uint256`, but they are not full-precision
+OpenZeppelin/Solmate `Math.mulDiv` replacements.
+
 ## Checked (Safe) Arithmetic
 
 For contracts that require overflow protection, the EDSL provides checked operations:
@@ -71,13 +76,20 @@ For contracts that require overflow protection, the EDSL provides checked operat
 | `safeSub a b` | `Option Uint256` | `none` if `b > a` |
 | `safeMul a b` | `Option Uint256` | `none` if `a * b > 2^256 - 1` |
 | `safeDiv a b` | `Option Uint256` | `none` if `b = 0` |
+| `mulDiv512Down? a b c` | `Option Uint256` | `none` if `c = 0` or `floor(a * b / c) > 2^256 - 1`; product is unbounded |
+| `mulDiv512Up? a b c` | `Option Uint256` | `none` if `c = 0` or `ceil(a * b / c) > 2^256 - 1`; product is unbounded |
 
-Checked operations are **EDSL-level constructs**. They are not compiler-enforced; the compiler always uses wrapping arithmetic. Contracts that need checked behavior must explicitly use `safeAdd`/`safeSub`/`safeMul` and handle the `Option` result (e.g., via `requireSomeUint` to revert on `none`).
+Checked operations are **EDSL-level constructs**. They are not compiler-enforced; the compiler always uses wrapping arithmetic. Contracts that need checked behavior must explicitly use `safeAdd`/`safeSub`/`safeMul` and handle the `Option` result (e.g., via `requireSomeUint` to revert on `none`). The `mulDiv512...?` helpers are proof/modeling helpers for full-precision Solidity `Math.mulDiv` semantics; compiled Yul lowering for a first-class 512-bit division primitive is still tracked by #1761.
 
 **Correctness proofs**: `Verity/Proofs/Stdlib/Math.lean` proves that checked operations return the correct result within bounds and `none` otherwise (e.g., `safeAdd_some`, `safeAdd_none`).
 
 `Stdlib.Math` also exposes fixed-point helpers `mulDivDown`, `mulDivUp`, `wMulDown`, and `wDivUp` (the `w` variants fix the divisor/multiplier to `WAD = 10^18`). All lemmas are in `Verity/Proofs/Stdlib/Math.lean` and are intentionally **preconditioned**: they assume the widened numerator stays within `MAX_UINT256`.
 
+For full-precision modeling, `mulDiv512Down?_some` and `mulDiv512Up?_some`
+state the exact natural-number quotient returned when the divisor is nonzero
+and the final quotient fits; the matching `_none_of_zero_divisor`,
+`_none_of_overflow`, and `_eq_some_iff` lemmas expose the failure boundary.
+
 | Lemma family | Generic helpers | Wad-specialized helpers |
 |--------------|----------------|------------------------|
 | Monotonicity (numerator) | `mulDivDown_monotone_left/right`, `mulDivUp_monotone_left/right` | `wMulDown_monotone_left/right`, `wDivUp_monotone_left` |
diff --git a/docs/INTERPRETER_FEATURE_MATRIX.md b/docs/INTERPRETER_FEATURE_MATRIX.md
index 96086f907..9617dee50 100644
--- a/docs/INTERPRETER_FEATURE_MATRIX.md
+++ b/docs/INTERPRETER_FEATURE_MATRIX.md
@@ -59,6 +59,7 @@ with the existing sync scripts and boundary checks.
 | Comparison | `eq/lt/gt/le/ge` | ok | ok | ok | ok | proved |
 | Logical | `logicalAnd/Or/Not` | ok | ok | -- | -- | proved |
 | Fixed-point math | `mulDivDown/Up, wMulDown/wDivUp, min/max` | ok | ok | -- | -- | proved |
+| Full-precision mulDiv modeling | `mulDiv512Down?/Up?` | -- | -- | -- | -- | EDSL/proof helper |
 | Internal call (expr) | `Expr.internalCall` | **0** | ok | -- | -- | proved |
 | Local variable | `Expr.localVar` | ok | ok | ok | -- | proved |
 | External call (linked) | `Expr.externalCall` | ok | ok | -- | -- | assumed |
diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md
index 9d827c6ea..e96e69cf9 100644
--- a/docs/ROADMAP.md
+++ b/docs/ROADMAP.md
@@ -88,6 +88,9 @@ Recent progress for low-level calls + returndata handling (`#622`):
 Recent progress for dynamic ABI-shaped parameters:
 - `verity_contract` now accepts dynamic array parameters whose element type is a static tuple of ABI words, e.g. `Array (Tuple [Uint256, Uint256, Int256])`, on tuple destructuring and tuple-return `arrayElement` paths. Those paths lower to checked word reads with the tuple element stride, which covers Solidity memory arrays of small fixed-size structs such as `CurveCut[]`; plain scalar `arrayElement` remains limited to single-word static element arrays.
 - `verity_contract` now accepts named `struct` declarations for function parameters as ABI tuple aliases. Executable contracts get Lean structures and field projection syntax, while the compilation model keeps the existing tuple ABI lowering. Nested static struct fields are supported for parameter field reads, covering the #1750 TermMax-style `config.feeConfig.borrowTakerFeeRatio` shape.
+
+Recent progress for arithmetic modeling:
+- `Stdlib.Math` now exposes `mulDiv512Down?` and `mulDiv512Up?` as proof-facing full-precision multiply-divide helpers. They compute `a * b` in unbounded natural-number precision and return `none` only when the divisor is zero or the final floor/ceil quotient does not fit in `uint256`, removing the artificial intermediate-product overflow hypothesis when modeling Solidity `Math.mulDiv` behavior. A compiled Yul primitive using the usual 512-bit division algorithm is still tracked by #1761.
 - ABI artifact emission now reflects explicit function mutability markers (`isView`, `isPure`) as `stateMutability: "view" | "pure"` in generated JSON.
 
 Recent progress for custom errors (`#586`):

From 1d2bbade43fad77e4e92e002a70176f69294c9af Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 01:09:17 +0200
Subject: [PATCH 02/18] Add mulDiv512 wide product regressions

---
 PrintAxioms.lean               |  5 +++-
 Verity/Proofs/Stdlib/Math.lean | 49 ++++++++++++++++++++++++++++++++++
 2 files changed, 53 insertions(+), 1 deletion(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index 123e42ec1..6114ae829 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -572,14 +572,17 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Verity/Proofs/Stdlib/Math.lean
 -- #print axioms Verity.Proofs.Stdlib.Math.modulus_eq_max_succ  -- private
 -- #print axioms Verity.Proofs.Stdlib.Math.lt_modulus_of_le_max  -- private
+-- #print axioms Verity.Proofs.Stdlib.Math.max_uint256_lt_modulus  -- private
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_some
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_none_of_zero_divisor
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_none_of_overflow
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_eq_some_iff
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_wide_product_regression
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_some
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_none_of_zero_divisor
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_none_of_overflow
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_eq_some_iff
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_wide_product_regression
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_nat_eq
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_mul_le
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_pos
@@ -3807,4 +3810,4 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Compiler/Proofs/YulGeneration/ReferenceOracle/Semantics.lean
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_sender
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
--- Total: 3631 theorems/lemmas (2685 public, 946 private, 0 sorry'd)
+-- Total: 3634 theorems/lemmas (2687 public, 947 private, 0 sorry'd)
diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index 15dc76b4b..6d38c7f88 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -26,6 +26,10 @@ private theorem lt_modulus_of_le_max {n : Nat} (h : n ≤ MAX_UINT256) :
     n < MAX_UINT256 + 1 := Nat.lt_succ_of_le h
     _ = Verity.Core.Uint256.modulus := by simp [modulus_eq_max_succ]
 
+private theorem max_uint256_lt_modulus :
+    MAX_UINT256 < Verity.Core.Uint256.modulus :=
+  lt_modulus_of_le_max (Nat.le_refl MAX_UINT256)
+
 /-! ## Full-precision mulDiv512 helpers -/
 
 /-- `mulDiv512Down?` returns the exact full-precision floor quotient when it fits. -/
@@ -64,6 +68,25 @@ theorem mulDiv512Down?_eq_some_iff (a b c out : Uint256) :
     · have hFit : ((a : Nat) * (b : Nat)) / (c : Nat) ≤ MAX_UINT256 := Nat.le_of_not_gt hOverflow
       simp [Verity.Stdlib.Math.mulDiv512Down?, hC, hOverflow, hFit]
 
+/-- Regression: full-precision floor `mulDiv512` permits a 256-bit-overflowing
+intermediate product when the final quotient fits. -/
+theorem mulDiv512Down?_wide_product_regression :
+    mulDiv512Down?
+        (Verity.Core.Uint256.ofNat MAX_UINT256)
+        (Verity.Core.Uint256.ofNat 2)
+        (Verity.Core.Uint256.ofNat 2) =
+      some (Verity.Core.Uint256.ofNat MAX_UINT256) := by
+  have hMaxMod :
+      MAX_UINT256 % Verity.Core.Uint256.modulus = MAX_UINT256 :=
+    Nat.mod_eq_of_lt max_uint256_lt_modulus
+  have hTwoMod : (2 : Nat) % Verity.Core.Uint256.modulus = 2 :=
+    Nat.mod_eq_of_lt (by
+      dsimp [Verity.Core.Uint256.modulus, Verity.Core.UINT256_MODULUS]
+      decide)
+  have hQuot : MAX_UINT256 * 2 / 2 = MAX_UINT256 := by
+    simp
+  simp [Verity.Stdlib.Math.mulDiv512Down?, hMaxMod, hTwoMod, hQuot]
+
 /-- `mulDiv512Up?` returns the exact full-precision ceil quotient when it fits. -/
 theorem mulDiv512Up?_some (a b c : Uint256)
     (hC : (c : Nat) ≠ 0)
@@ -105,6 +128,32 @@ theorem mulDiv512Up?_eq_some_iff (a b c out : Uint256) :
         Nat.le_of_not_gt hOverflow
       simp [Verity.Stdlib.Math.mulDiv512Up?, hC, hOverflow, hFit]
 
+/-- Regression: full-precision ceil `mulDiv512` permits a 256-bit-overflowing
+intermediate product when the rounded quotient fits. -/
+theorem mulDiv512Up?_wide_product_regression :
+    mulDiv512Up?
+        (Verity.Core.Uint256.ofNat MAX_UINT256)
+        (Verity.Core.Uint256.ofNat 2)
+        (Verity.Core.Uint256.ofNat 2) =
+      some (Verity.Core.Uint256.ofNat MAX_UINT256) := by
+  have hMaxMod :
+      MAX_UINT256 % Verity.Core.Uint256.modulus = MAX_UINT256 :=
+    Nat.mod_eq_of_lt max_uint256_lt_modulus
+  have hTwoMod : (2 : Nat) % Verity.Core.Uint256.modulus = 2 :=
+    Nat.mod_eq_of_lt (by
+      dsimp [Verity.Core.Uint256.modulus, Verity.Core.UINT256_MODULUS]
+      decide)
+  have hQuot : (MAX_UINT256 * 2 + (2 - 1)) / 2 = MAX_UINT256 := by
+    rw [show (2 : Nat) - 1 = 1 by omega]
+    calc
+      (MAX_UINT256 * 2 + 1) / 2 = (1 + 2 * MAX_UINT256) / 2 := by
+        rw [Nat.mul_comm MAX_UINT256 2, Nat.add_comm]
+      _ = 1 / 2 + MAX_UINT256 := Nat.add_mul_div_left 1 MAX_UINT256 (by decide : 0 < 2)
+      _ = MAX_UINT256 := by
+        rw [Nat.div_eq_of_lt (by decide : 1 < 2)]
+        rfl
+  simp [Verity.Stdlib.Math.mulDiv512Up?, hMaxMod, hTwoMod, hQuot]
+
 /-! ## mulDiv / wad helpers -/
 
 /-- `mulDivDown` agrees with exact natural-number division when the numerator does not wrap. -/

From 76bd39819521ee04bfd3c3b3b45b9e57557b8e7b Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 02:08:08 +0200
Subject: [PATCH 03/18] Add mulDiv512 fit predicates

---
 PrintAxioms.lean               |  6 +++-
 Verity/Proofs/Stdlib/Math.lean | 58 ++++++++++++++++++++++++++++++++++
 2 files changed, 63 insertions(+), 1 deletion(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index 6114ae829..53a4546d0 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -577,11 +577,15 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_none_of_zero_divisor
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_none_of_overflow
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_eq_some_iff
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_isSome_iff
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_isNone_iff
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_wide_product_regression
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_some
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_none_of_zero_divisor
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_none_of_overflow
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_eq_some_iff
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_isSome_iff
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_isNone_iff
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_wide_product_regression
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_nat_eq
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_mul_le
@@ -3810,4 +3814,4 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Compiler/Proofs/YulGeneration/ReferenceOracle/Semantics.lean
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_sender
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
--- Total: 3634 theorems/lemmas (2687 public, 947 private, 0 sorry'd)
+-- Total: 3638 theorems/lemmas (2691 public, 947 private, 0 sorry'd)
diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index 6d38c7f88..1e99f9e7b 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -68,6 +68,32 @@ theorem mulDiv512Down?_eq_some_iff (a b c out : Uint256) :
     · have hFit : ((a : Nat) * (b : Nat)) / (c : Nat) ≤ MAX_UINT256 := Nat.le_of_not_gt hOverflow
       simp [Verity.Stdlib.Math.mulDiv512Down?, hC, hOverflow, hFit]
 
+/-- `mulDiv512Down?` succeeds exactly when the divisor is nonzero and the
+full-precision floor quotient fits in `uint256`. -/
+theorem mulDiv512Down?_isSome_iff (a b c : Uint256) :
+    (mulDiv512Down? a b c).isSome ↔
+      (c : Nat) ≠ 0 ∧
+      ((a : Nat) * (b : Nat)) / (c : Nat) ≤ MAX_UINT256 := by
+  by_cases hC : (c : Nat) = 0
+  · simp [Verity.Stdlib.Math.mulDiv512Down?, hC]
+  · by_cases hOverflow : ((a : Nat) * (b : Nat)) / (c : Nat) > MAX_UINT256
+    · have hNotFit : ¬((a : Nat) * (b : Nat)) / (c : Nat) ≤ MAX_UINT256 := by
+        exact Nat.not_le_of_gt hOverflow
+      simp [Verity.Stdlib.Math.mulDiv512Down?, hC, hOverflow, hNotFit]
+    · have hFit : ((a : Nat) * (b : Nat)) / (c : Nat) ≤ MAX_UINT256 := Nat.le_of_not_gt hOverflow
+      simp [Verity.Stdlib.Math.mulDiv512Down?, hC, hOverflow, hFit]
+
+/-- `mulDiv512Down?` rejects exactly zero divisors or overflowing floor quotients. -/
+theorem mulDiv512Down?_isNone_iff (a b c : Uint256) :
+    (mulDiv512Down? a b c).isNone ↔
+      (c : Nat) = 0 ∨
+      MAX_UINT256 < ((a : Nat) * (b : Nat)) / (c : Nat) := by
+  by_cases hC : (c : Nat) = 0
+  · simp [Verity.Stdlib.Math.mulDiv512Down?, hC]
+  · by_cases hOverflow : ((a : Nat) * (b : Nat)) / (c : Nat) > MAX_UINT256
+    · simp [Verity.Stdlib.Math.mulDiv512Down?, hC, hOverflow]
+    · simp [Verity.Stdlib.Math.mulDiv512Down?, hC, hOverflow]
+
 /-- Regression: full-precision floor `mulDiv512` permits a 256-bit-overflowing
 intermediate product when the final quotient fits. -/
 theorem mulDiv512Down?_wide_product_regression :
@@ -128,6 +154,38 @@ theorem mulDiv512Up?_eq_some_iff (a b c out : Uint256) :
         Nat.le_of_not_gt hOverflow
       simp [Verity.Stdlib.Math.mulDiv512Up?, hC, hOverflow, hFit]
 
+/-- `mulDiv512Up?` succeeds exactly when the divisor is nonzero and the
+full-precision rounded-up quotient fits in `uint256`. -/
+theorem mulDiv512Up?_isSome_iff (a b c : Uint256) :
+    (mulDiv512Up? a b c).isSome ↔
+      (c : Nat) ≠ 0 ∧
+      (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) ≤ MAX_UINT256 := by
+  by_cases hC : (c : Nat) = 0
+  · simp [Verity.Stdlib.Math.mulDiv512Up?, hC]
+  · by_cases hOverflow :
+        (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) > MAX_UINT256
+    · have hNotFit :
+          ¬((((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) ≤ MAX_UINT256) := by
+        exact Nat.not_le_of_gt hOverflow
+      simp [Verity.Stdlib.Math.mulDiv512Up?, hC, hOverflow, hNotFit]
+    · have hFit :
+          (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) ≤ MAX_UINT256 :=
+        Nat.le_of_not_gt hOverflow
+      simp [Verity.Stdlib.Math.mulDiv512Up?, hC, hOverflow, hFit]
+
+/-- `mulDiv512Up?` rejects exactly zero divisors or overflowing rounded-up quotients. -/
+theorem mulDiv512Up?_isNone_iff (a b c : Uint256) :
+    (mulDiv512Up? a b c).isNone ↔
+      (c : Nat) = 0 ∨
+      MAX_UINT256 <
+        (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) := by
+  by_cases hC : (c : Nat) = 0
+  · simp [Verity.Stdlib.Math.mulDiv512Up?, hC]
+  · by_cases hOverflow :
+        (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) > MAX_UINT256
+    · simp [Verity.Stdlib.Math.mulDiv512Up?, hC, hOverflow]
+    · simp [Verity.Stdlib.Math.mulDiv512Up?, hC, hOverflow]
+
 /-- Regression: full-precision ceil `mulDiv512` permits a 256-bit-overflowing
 intermediate product when the rounded quotient fits. -/
 theorem mulDiv512Up?_wide_product_regression :

From c56c57514e99bee692336753758a7937c78dbaec Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 02:14:27 +0200
Subject: [PATCH 04/18] Add mulDiv512 sandwich lemmas

---
 PrintAxioms.lean               |  8 +++++-
 Verity/Proofs/Stdlib/Math.lean | 51 ++++++++++++++++++++++++++++++++++
 docs/ARITHMETIC_PROFILE.md     |  6 +++-
 3 files changed, 63 insertions(+), 2 deletions(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index 53a4546d0..d09f506e6 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -573,11 +573,15 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- #print axioms Verity.Proofs.Stdlib.Math.modulus_eq_max_succ  -- private
 -- #print axioms Verity.Proofs.Stdlib.Math.lt_modulus_of_le_max  -- private
 -- #print axioms Verity.Proofs.Stdlib.Math.max_uint256_lt_modulus  -- private
+-- #print axioms Verity.Proofs.Stdlib.Math.ceil_mul_div_ge  -- private
+-- #print axioms Verity.Proofs.Stdlib.Math.ceil_mul_div_le_add_pred  -- private
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_some
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_none_of_zero_divisor
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_none_of_overflow
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_eq_some_iff
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_isSome_iff
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_mul_le
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_lt_succ_mul
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_isNone_iff
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_wide_product_regression
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_some
@@ -585,6 +589,8 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_none_of_overflow
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_eq_some_iff
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_isSome_iff
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_mul_ge
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_mul_le_add_pred
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_isNone_iff
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_wide_product_regression
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_nat_eq
@@ -3814,4 +3820,4 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Compiler/Proofs/YulGeneration/ReferenceOracle/Semantics.lean
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_sender
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
--- Total: 3638 theorems/lemmas (2691 public, 947 private, 0 sorry'd)
+-- Total: 3644 theorems/lemmas (2695 public, 949 private, 0 sorry'd)
diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index 1e99f9e7b..e06fb3875 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -32,6 +32,18 @@ private theorem max_uint256_lt_modulus :
 
 /-! ## Full-precision mulDiv512 helpers -/
 
+private theorem ceil_mul_div_ge (n d : Nat) (hd : 0 < d) :
+    n ≤ ((n + (d - 1)) / d) * d := by
+  have hdiv : (n + (d - 1)) / d ≤ (n + (d - 1)) / d := Nat.le_refl _
+  have hle := (Nat.div_le_iff_le_mul_add_pred (b := d) (a := n + (d - 1))
+    (c := (n + (d - 1)) / d) hd).mp hdiv
+  have h : n ≤ d * ((n + (d - 1)) / d) := Nat.le_of_add_le_add_right hle
+  simpa [Nat.mul_comm] using h
+
+private theorem ceil_mul_div_le_add_pred (n d : Nat) :
+    ((n + (d - 1)) / d) * d ≤ n + (d - 1) := by
+  simpa [Nat.mul_comm] using Nat.mul_div_le (n + (d - 1)) d
+
 /-- `mulDiv512Down?` returns the exact full-precision floor quotient when it fits. -/
 theorem mulDiv512Down?_some (a b c : Uint256)
     (hC : (c : Nat) ≠ 0)
@@ -83,6 +95,26 @@ theorem mulDiv512Down?_isSome_iff (a b c : Uint256) :
     · have hFit : ((a : Nat) * (b : Nat)) / (c : Nat) ≤ MAX_UINT256 := Nat.le_of_not_gt hOverflow
       simp [Verity.Stdlib.Math.mulDiv512Down?, hC, hOverflow, hFit]
 
+/-- A successful full-precision floor result is below the exact product. -/
+theorem mulDiv512Down?_mul_le (a b c out : Uint256)
+    (h : mulDiv512Down? a b c = some out) :
+    (out : Nat) * (c : Nat) ≤ (a : Nat) * (b : Nat) := by
+  rcases (mulDiv512Down?_eq_some_iff a b c out).mp h with ⟨_hC, hFit, hOut⟩
+  rw [← hOut]
+  simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit)]
+  exact Nat.div_mul_le_self ((a : Nat) * (b : Nat)) (c : Nat)
+
+/-- A successful full-precision floor result is the greatest quotient below
+the exact product. -/
+theorem mulDiv512Down?_lt_succ_mul (a b c out : Uint256)
+    (h : mulDiv512Down? a b c = some out) :
+    (a : Nat) * (b : Nat) < ((out : Nat) + 1) * (c : Nat) := by
+  rcases (mulDiv512Down?_eq_some_iff a b c out).mp h with ⟨hC, hFit, hOut⟩
+  rw [← hOut]
+  simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit)]
+  simpa [Nat.mul_comm] using
+    Nat.lt_mul_div_succ ((b : Nat) * (a : Nat)) (Nat.pos_of_ne_zero hC)
+
 /-- `mulDiv512Down?` rejects exactly zero divisors or overflowing floor quotients. -/
 theorem mulDiv512Down?_isNone_iff (a b c : Uint256) :
     (mulDiv512Down? a b c).isNone ↔
@@ -173,6 +205,25 @@ theorem mulDiv512Up?_isSome_iff (a b c : Uint256) :
         Nat.le_of_not_gt hOverflow
       simp [Verity.Stdlib.Math.mulDiv512Up?, hC, hOverflow, hFit]
 
+/-- A successful full-precision ceil result is above the exact product. -/
+theorem mulDiv512Up?_mul_ge (a b c out : Uint256)
+    (h : mulDiv512Up? a b c = some out) :
+    (a : Nat) * (b : Nat) ≤ (out : Nat) * (c : Nat) := by
+  rcases (mulDiv512Up?_eq_some_iff a b c out).mp h with ⟨hC, hFit, hOut⟩
+  rw [← hOut]
+  simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit)]
+  exact ceil_mul_div_ge ((a : Nat) * (b : Nat)) (c : Nat) (Nat.pos_of_ne_zero hC)
+
+/-- A successful full-precision ceil result exceeds the exact product by less
+than one divisor. -/
+theorem mulDiv512Up?_mul_le_add_pred (a b c out : Uint256)
+    (h : mulDiv512Up? a b c = some out) :
+    (out : Nat) * (c : Nat) ≤ (a : Nat) * (b : Nat) + ((c : Nat) - 1) := by
+  rcases (mulDiv512Up?_eq_some_iff a b c out).mp h with ⟨_hC, hFit, hOut⟩
+  rw [← hOut]
+  simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit)]
+  exact ceil_mul_div_le_add_pred ((a : Nat) * (b : Nat)) (c : Nat)
+
 /-- `mulDiv512Up?` rejects exactly zero divisors or overflowing rounded-up quotients. -/
 theorem mulDiv512Up?_isNone_iff (a b c : Uint256) :
     (mulDiv512Up? a b c).isNone ↔
diff --git a/docs/ARITHMETIC_PROFILE.md b/docs/ARITHMETIC_PROFILE.md
index 86b72a0cf..f4d0ce558 100644
--- a/docs/ARITHMETIC_PROFILE.md
+++ b/docs/ARITHMETIC_PROFILE.md
@@ -88,7 +88,11 @@ Checked operations are **EDSL-level constructs**. They are not compiler-enforced
 For full-precision modeling, `mulDiv512Down?_some` and `mulDiv512Up?_some`
 state the exact natural-number quotient returned when the divisor is nonzero
 and the final quotient fits; the matching `_none_of_zero_divisor`,
-`_none_of_overflow`, and `_eq_some_iff` lemmas expose the failure boundary.
+`_none_of_overflow`, `_eq_some_iff`, `_isSome_iff`, and `_isNone_iff` lemmas
+expose the failure boundary. Successful full-precision results also have
+direct sandwich lemmas: `mulDiv512Down?_mul_le`,
+`mulDiv512Down?_lt_succ_mul`, `mulDiv512Up?_mul_ge`, and
+`mulDiv512Up?_mul_le_add_pred`.
 
 | Lemma family | Generic helpers | Wad-specialized helpers |
 |--------------|----------------|------------------------|

From abd64a56e47bd7a8618fc573f5104547cdfe7858 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 02:20:27 +0200
Subject: [PATCH 05/18] Add mulDiv512 convenience lemmas

---
 PrintAxioms.lean               | 12 ++++-
 Verity/Proofs/Stdlib/Math.lean | 93 ++++++++++++++++++++++++++++++++++
 docs/ARITHMETIC_PROFILE.md     |  4 +-
 3 files changed, 107 insertions(+), 2 deletions(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index d09f506e6..ea07f6473 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -583,6 +583,11 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_mul_le
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_lt_succ_mul
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_isNone_iff
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_comm
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_zero_left
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_zero_right
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_cancel_right
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_cancel_left
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_wide_product_regression
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_some
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_none_of_zero_divisor
@@ -592,6 +597,11 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_mul_ge
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_mul_le_add_pred
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_isNone_iff
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_comm
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_zero_left
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_zero_right
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_cancel_right
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_cancel_left
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_wide_product_regression
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_nat_eq
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_mul_le
@@ -3820,4 +3830,4 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Compiler/Proofs/YulGeneration/ReferenceOracle/Semantics.lean
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_sender
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
--- Total: 3644 theorems/lemmas (2695 public, 949 private, 0 sorry'd)
+-- Total: 3654 theorems/lemmas (2705 public, 949 private, 0 sorry'd)
diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index e06fb3875..1ce28244c 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -126,6 +126,45 @@ theorem mulDiv512Down?_isNone_iff (a b c : Uint256) :
     · simp [Verity.Stdlib.Math.mulDiv512Down?, hC, hOverflow]
     · simp [Verity.Stdlib.Math.mulDiv512Down?, hC, hOverflow]
 
+/-- Full-precision floor multiplication is commutative in its numerator operands. -/
+theorem mulDiv512Down?_comm (a b c : Uint256) :
+    mulDiv512Down? a b c = mulDiv512Down? b a c := by
+  simp [Verity.Stdlib.Math.mulDiv512Down?, Nat.mul_comm]
+
+/-- A zero left numerator collapses full-precision floor multiplication to zero. -/
+theorem mulDiv512Down?_zero_left (b c : Uint256)
+    (hC : (c : Nat) ≠ 0) :
+    mulDiv512Down? 0 b c = some 0 := by
+  simp [Verity.Stdlib.Math.mulDiv512Down?, hC]
+
+/-- A zero right numerator collapses full-precision floor multiplication to zero. -/
+theorem mulDiv512Down?_zero_right (a c : Uint256)
+    (hC : (c : Nat) ≠ 0) :
+    mulDiv512Down? a 0 c = some 0 := by
+  simpa [mulDiv512Down?_comm] using mulDiv512Down?_zero_left a c hC
+
+/-- Exact full-precision floor cancellation by the right numerator operand. -/
+theorem mulDiv512Down?_cancel_right (a c : Uint256)
+    (hC : (c : Nat) ≠ 0) :
+    mulDiv512Down? a c c = some a := by
+  have hCPos : 0 < (c : Nat) := Nat.pos_of_ne_zero hC
+  have hQuot : (a : Nat) * (c : Nat) / (c : Nat) = (a : Nat) := by
+    simpa [Nat.mul_comm] using Nat.mul_div_right (a : Nat) hCPos
+  have hFit : (a : Nat) ≤ MAX_UINT256 := Verity.Core.Uint256.val_le_max a
+  rw [mulDiv512Down?_some (a := a) (b := c) (c := c) hC]
+  · congr
+    apply Verity.Core.Uint256.ext
+    rw [hQuot]
+    exact Nat.mod_eq_of_lt a.isLt
+  · simpa [hQuot] using hFit
+
+/-- Exact full-precision floor cancellation by the left numerator operand. -/
+theorem mulDiv512Down?_cancel_left (a c : Uint256)
+    (hC : (c : Nat) ≠ 0) :
+    mulDiv512Down? c a c = some a := by
+  rw [mulDiv512Down?_comm c a c]
+  exact mulDiv512Down?_cancel_right a c hC
+
 /-- Regression: full-precision floor `mulDiv512` permits a 256-bit-overflowing
 intermediate product when the final quotient fits. -/
 theorem mulDiv512Down?_wide_product_regression :
@@ -237,6 +276,60 @@ theorem mulDiv512Up?_isNone_iff (a b c : Uint256) :
     · simp [Verity.Stdlib.Math.mulDiv512Up?, hC, hOverflow]
     · simp [Verity.Stdlib.Math.mulDiv512Up?, hC, hOverflow]
 
+/-- Full-precision ceil multiplication is commutative in its numerator operands. -/
+theorem mulDiv512Up?_comm (a b c : Uint256) :
+    mulDiv512Up? a b c = mulDiv512Up? b a c := by
+  simp [Verity.Stdlib.Math.mulDiv512Up?, Nat.mul_comm]
+
+/-- A zero left numerator collapses full-precision ceil multiplication to zero. -/
+theorem mulDiv512Up?_zero_left (b c : Uint256)
+    (hC : (c : Nat) ≠ 0) :
+    mulDiv512Up? 0 b c = some 0 := by
+  have hCeilZero : (((0 : Uint256) : Nat) * (b : Nat) + ((c : Nat) - 1)) / (c : Nat) = 0 := by
+    simpa using Nat.div_eq_of_lt (Nat.pred_lt hC)
+  rw [mulDiv512Up?_some (a := 0) (b := b) (c := c) hC]
+  · congr
+  · rw [hCeilZero]
+    exact Nat.zero_le _
+
+/-- A zero right numerator collapses full-precision ceil multiplication to zero. -/
+theorem mulDiv512Up?_zero_right (a c : Uint256)
+    (hC : (c : Nat) ≠ 0) :
+    mulDiv512Up? a 0 c = some 0 := by
+  simpa [mulDiv512Up?_comm] using mulDiv512Up?_zero_left a c hC
+
+/-- Exact full-precision ceil cancellation by the right numerator operand. -/
+theorem mulDiv512Up?_cancel_right (a c : Uint256)
+    (hC : (c : Nat) ≠ 0) :
+    mulDiv512Up? a c c = some a := by
+  have hCPos : 0 < (c : Nat) := Nat.pos_of_ne_zero hC
+  have hQuot :
+      (((a : Nat) * (c : Nat)) + ((c : Nat) - 1)) / (c : Nat) = (a : Nat) := by
+    calc
+      (((a : Nat) * (c : Nat)) + ((c : Nat) - 1)) / (c : Nat)
+          = (((c : Nat) - 1) + (c : Nat) * (a : Nat)) / (c : Nat) := by
+              rw [Nat.mul_comm, Nat.add_comm]
+      _ = ((c : Nat) - 1) / (c : Nat) + (a : Nat) :=
+              Nat.add_mul_div_left ((c : Nat) - 1) (a : Nat) hCPos
+      _ = (a : Nat) := by
+              have hPredDiv : ((c : Nat) - 1) / (c : Nat) = 0 :=
+                Nat.div_eq_of_lt (Nat.pred_lt hC)
+              omega
+  have hFit : (a : Nat) ≤ MAX_UINT256 := Verity.Core.Uint256.val_le_max a
+  rw [mulDiv512Up?_some (a := a) (b := c) (c := c) hC]
+  · congr
+    apply Verity.Core.Uint256.ext
+    rw [hQuot]
+    exact Nat.mod_eq_of_lt a.isLt
+  · simpa [hQuot] using hFit
+
+/-- Exact full-precision ceil cancellation by the left numerator operand. -/
+theorem mulDiv512Up?_cancel_left (a c : Uint256)
+    (hC : (c : Nat) ≠ 0) :
+    mulDiv512Up? c a c = some a := by
+  rw [mulDiv512Up?_comm c a c]
+  exact mulDiv512Up?_cancel_right a c hC
+
 /-- Regression: full-precision ceil `mulDiv512` permits a 256-bit-overflowing
 intermediate product when the rounded quotient fits. -/
 theorem mulDiv512Up?_wide_product_regression :
diff --git a/docs/ARITHMETIC_PROFILE.md b/docs/ARITHMETIC_PROFILE.md
index f4d0ce558..68fd17aab 100644
--- a/docs/ARITHMETIC_PROFILE.md
+++ b/docs/ARITHMETIC_PROFILE.md
@@ -92,7 +92,9 @@ and the final quotient fits; the matching `_none_of_zero_divisor`,
 expose the failure boundary. Successful full-precision results also have
 direct sandwich lemmas: `mulDiv512Down?_mul_le`,
 `mulDiv512Down?_lt_succ_mul`, `mulDiv512Up?_mul_ge`, and
-`mulDiv512Up?_mul_le_add_pred`.
+`mulDiv512Up?_mul_le_add_pred`. They also mirror the existing `mulDiv`
+convenience surface with numerator commutativity, zero-numerator, and exact
+same-denominator cancellation lemmas.
 
 | Lemma family | Generic helpers | Wad-specialized helpers |
 |--------------|----------------|------------------------|

From 1a1e223b629dddd87a99c3e94c26c4c9b58e7e2b Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 02:30:56 +0200
Subject: [PATCH 06/18] Add mulDiv512 automation lemmas

---
 PrintAxioms.lean                     |  6 +-
 Verity/Proofs/Stdlib/Automation.lean | 95 ++++++++++++++++++++++++++++
 docs/ARITHMETIC_PROFILE.md           |  6 ++
 3 files changed, 106 insertions(+), 1 deletion(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index ea07f6473..e060744b3 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -463,6 +463,10 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Automation.safeAdd_some_val
 #print axioms Verity.Proofs.Stdlib.Automation.safeMul_some_iff_le
 #print axioms Verity.Proofs.Stdlib.Automation.safeMul_none_iff_gt
+#print axioms Verity.Proofs.Stdlib.Automation.mulDiv512Down?_some_iff
+#print axioms Verity.Proofs.Stdlib.Automation.mulDiv512Down?_none_iff
+#print axioms Verity.Proofs.Stdlib.Automation.mulDiv512Up?_some_iff
+#print axioms Verity.Proofs.Stdlib.Automation.mulDiv512Up?_none_iff
 #print axioms Verity.Proofs.Stdlib.Automation.add_one_preserves_order_iff_no_overflow
 #print axioms Verity.Proofs.Stdlib.Automation.wf_of_state_eq
 #print axioms Verity.Proofs.Stdlib.Automation.wf_preservation_of_frame
@@ -3830,4 +3834,4 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Compiler/Proofs/YulGeneration/ReferenceOracle/Semantics.lean
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_sender
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
--- Total: 3654 theorems/lemmas (2705 public, 949 private, 0 sorry'd)
+-- Total: 3658 theorems/lemmas (2709 public, 949 private, 0 sorry'd)
diff --git a/Verity/Proofs/Stdlib/Automation.lean b/Verity/Proofs/Stdlib/Automation.lean
index 9688906c4..c51027e38 100644
--- a/Verity/Proofs/Stdlib/Automation.lean
+++ b/Verity/Proofs/Stdlib/Automation.lean
@@ -717,6 +717,101 @@ theorem safeMul_none_iff_gt (a b : Verity.Core.Uint256) :
     · intro h_gt
       exact absurd h_gt h
 
+-- Full-precision floor mulDiv succeeds iff the divisor is nonzero and the quotient fits.
+theorem mulDiv512Down?_some_iff (a b c : Verity.Core.Uint256) :
+    (Verity.Stdlib.Math.mulDiv512Down? a b c).isSome ↔
+    (c : Nat) ≠ 0 ∧
+      ((a : Nat) * (b : Nat)) / (c : Nat) ≤ Verity.Stdlib.Math.MAX_UINT256 := by
+  unfold Verity.Stdlib.Math.mulDiv512Down?
+  by_cases hC : (c : Nat) = 0
+  · simp [hC]
+  · by_cases hOverflow : ((a : Nat) * (b : Nat)) / (c : Nat) > Verity.Stdlib.Math.MAX_UINT256
+    · constructor
+      · intro h_some
+        simp [hC, hOverflow] at h_some
+      · intro h_fit
+        omega
+    · constructor
+      · intro _
+        exact ⟨hC, Nat.le_of_not_gt hOverflow⟩
+      · intro _
+        simp [hC, hOverflow]
+
+-- Full-precision floor mulDiv rejects iff the divisor is zero or the quotient overflows.
+theorem mulDiv512Down?_none_iff (a b c : Verity.Core.Uint256) :
+    (Verity.Stdlib.Math.mulDiv512Down? a b c).isNone ↔
+    (c : Nat) = 0 ∨
+      Verity.Stdlib.Math.MAX_UINT256 <
+        ((a : Nat) * (b : Nat)) / (c : Nat) := by
+  unfold Verity.Stdlib.Math.mulDiv512Down?
+  by_cases hC : (c : Nat) = 0
+  · simp [hC]
+  · by_cases hOverflow : ((a : Nat) * (b : Nat)) / (c : Nat) > Verity.Stdlib.Math.MAX_UINT256
+    · simp [hC, hOverflow]
+    · constructor
+      · intro h_none
+        simp [hC, hOverflow] at h_none
+      · intro h_reject
+        rcases h_reject with h_zero | h_gt
+        · exact False.elim (hC h_zero)
+        · exact False.elim (hOverflow h_gt)
+
+-- Full-precision ceil mulDiv succeeds iff the divisor is nonzero and the rounded quotient fits.
+theorem mulDiv512Up?_some_iff (a b c : Verity.Core.Uint256) :
+    (Verity.Stdlib.Math.mulDiv512Up? a b c).isSome ↔
+    (c : Nat) ≠ 0 ∧
+      (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) ≤
+        Verity.Stdlib.Math.MAX_UINT256 := by
+  unfold Verity.Stdlib.Math.mulDiv512Up?
+  by_cases hC : (c : Nat) = 0
+  · simp [hC]
+  · by_cases hOverflow :
+      (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) >
+        Verity.Stdlib.Math.MAX_UINT256
+    · constructor
+      · intro h_some
+        simp [hC, hOverflow] at h_some
+      · intro h_fit
+        omega
+    · constructor
+      · intro _
+        exact ⟨hC, Nat.le_of_not_gt hOverflow⟩
+      · intro _
+        simp [hC, hOverflow]
+
+-- Full-precision ceil mulDiv rejects iff the divisor is zero or the rounded quotient overflows.
+theorem mulDiv512Up?_none_iff (a b c : Verity.Core.Uint256) :
+    (Verity.Stdlib.Math.mulDiv512Up? a b c).isNone ↔
+    (c : Nat) = 0 ∨
+      Verity.Stdlib.Math.MAX_UINT256 <
+        (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) := by
+  unfold Verity.Stdlib.Math.mulDiv512Up?
+  by_cases hC : (c : Nat) = 0
+  · simp [hC]
+  · by_cases hOverflow :
+      (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) >
+        Verity.Stdlib.Math.MAX_UINT256
+    · simp [hC, hOverflow]
+    · constructor
+      · intro h_none
+        simp [hC, hOverflow] at h_none
+      · intro h_reject
+        rcases h_reject with h_zero | h_gt
+        · exact False.elim (hC h_zero)
+        · exact False.elim (hOverflow h_gt)
+
+example (a b c : Verity.Core.Uint256)
+    (hC : (c : Nat) ≠ 0)
+    (hFit : ((a : Nat) * (b : Nat)) / (c : Nat) ≤ Verity.Stdlib.Math.MAX_UINT256) :
+    (Verity.Stdlib.Math.mulDiv512Down? a b c).isSome := by
+  exact (mulDiv512Down?_some_iff a b c).mpr ⟨hC, hFit⟩
+
+example (a b c : Verity.Core.Uint256)
+    (hOverflow : Verity.Stdlib.Math.MAX_UINT256 <
+      (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat)) :
+    (Verity.Stdlib.Math.mulDiv512Up? a b c).isNone := by
+  exact (mulDiv512Up?_none_iff a b c).mpr (Or.inr hOverflow)
+
 /-!
 ## Modular Arithmetic Wraparound Lemmas
 
diff --git a/docs/ARITHMETIC_PROFILE.md b/docs/ARITHMETIC_PROFILE.md
index 68fd17aab..7f8affd6a 100644
--- a/docs/ARITHMETIC_PROFILE.md
+++ b/docs/ARITHMETIC_PROFILE.md
@@ -96,6 +96,12 @@ direct sandwich lemmas: `mulDiv512Down?_mul_le`,
 convenience surface with numerator commutativity, zero-numerator, and exact
 same-denominator cancellation lemmas.
 
+`Verity.Proofs.Stdlib.Automation` mirrors the full-precision fit/rejection iff
+lemmas under automation-friendly names (`mulDiv512Down?_some_iff`,
+`mulDiv512Down?_none_iff`, `mulDiv512Up?_some_iff`,
+`mulDiv512Up?_none_iff`), so downstream proofs can rewrite common quotient-fit
+side conditions without importing the full arithmetic proof module directly.
+
 | Lemma family | Generic helpers | Wad-specialized helpers |
 |--------------|----------------|------------------------|
 | Monotonicity (numerator) | `mulDivDown_monotone_left/right`, `mulDivUp_monotone_left/right` | `wMulDown_monotone_left/right`, `wDivUp_monotone_left` |

From f3827217a028ba12514949f5b34c2b861581fdde Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 02:36:16 +0200
Subject: [PATCH 07/18] Add mulDiv512 rounding exactness lemmas

---
 PrintAxioms.lean               |  4 +++-
 Verity/Proofs/Stdlib/Math.lean | 31 +++++++++++++++++++++++++++++++
 docs/ARITHMETIC_PROFILE.md     |  5 ++++-
 3 files changed, 38 insertions(+), 2 deletions(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index e060744b3..e150f0735 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -624,6 +624,8 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- #print axioms Verity.Proofs.Stdlib.Math.nat_ceil_div_le_div_add_one  -- private
 -- #print axioms Verity.Proofs.Stdlib.Math.nat_ceil_div_eq_div_of_dvd  -- private
 -- #print axioms Verity.Proofs.Stdlib.Math.nat_ceil_div_eq_div_add_one_of_not_dvd  -- private
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_eq_down_of_dvd
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_some_succ_of_not_dvd
 #print axioms Verity.Proofs.Stdlib.Math.mulDivUp_le_mulDivDown_add_one
 #print axioms Verity.Proofs.Stdlib.Math.mulDivUp_eq_mulDivDown_or_succ
 #print axioms Verity.Proofs.Stdlib.Math.mulDivUp_eq_mulDivDown_of_dvd
@@ -3834,4 +3836,4 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Compiler/Proofs/YulGeneration/ReferenceOracle/Semantics.lean
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_sender
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
--- Total: 3658 theorems/lemmas (2709 public, 949 private, 0 sorry'd)
+-- Total: 3660 theorems/lemmas (2711 public, 949 private, 0 sorry'd)
diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index 1ce28244c..008fe2447 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -638,6 +638,37 @@ private theorem nat_ceil_div_eq_div_add_one_of_not_dvd (n c : Nat) (hC : c ≠ 0
   simp
   simpa [Nat.mod_eq_of_lt hSubLt] using hCarry
 
+/-- Exact divisibility removes the full-precision ceil/floor gap. -/
+theorem mulDiv512Up?_eq_down_of_dvd (a b c : Uint256)
+    (hC : (c : Nat) ≠ 0)
+    (hFit : (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) ≤ MAX_UINT256)
+    (hDvd : (c : Nat) ∣ (a : Nat) * (b : Nat)) :
+    mulDiv512Up? a b c = mulDiv512Down? a b c := by
+  have hCeil :
+      (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) =
+        ((a : Nat) * (b : Nat)) / (c : Nat) :=
+    nat_ceil_div_eq_div_of_dvd ((a : Nat) * (b : Nat)) (c : Nat) hC hDvd
+  rw [mulDiv512Up?_some (a := a) (b := b) (c := c) hC hFit]
+  rw [mulDiv512Down?_some (a := a) (b := b) (c := c) hC]
+  · congr
+  · simpa [← hCeil] using hFit
+
+/-- If the full-precision numerator is not divisible by the divisor, ceil
+division is the successor of floor division. -/
+theorem mulDiv512Up?_some_succ_of_not_dvd (a b c : Uint256)
+    (hC : (c : Nat) ≠ 0)
+    (hFit : (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) ≤ MAX_UINT256)
+    (hNotDvd : ¬ (c : Nat) ∣ (a : Nat) * (b : Nat)) :
+    mulDiv512Up? a b c =
+      some (Verity.Core.Uint256.ofNat (((a : Nat) * (b : Nat)) / (c : Nat) + 1)) := by
+  have hCeil :
+      (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) =
+        ((a : Nat) * (b : Nat)) / (c : Nat) + 1 :=
+    nat_ceil_div_eq_div_add_one_of_not_dvd
+      ((a : Nat) * (b : Nat)) (c : Nat) hC hNotDvd
+  rw [mulDiv512Up?_some (a := a) (b := b) (c := c) hC hFit]
+  congr
+
 /-- The ceil helper exceeds the floor helper by at most one quotient step when both are exact. -/
 theorem mulDivUp_le_mulDivDown_add_one (a b c : Uint256)
     (hC : c ≠ 0)
diff --git a/docs/ARITHMETIC_PROFILE.md b/docs/ARITHMETIC_PROFILE.md
index 7f8affd6a..7d4ca1127 100644
--- a/docs/ARITHMETIC_PROFILE.md
+++ b/docs/ARITHMETIC_PROFILE.md
@@ -94,7 +94,10 @@ direct sandwich lemmas: `mulDiv512Down?_mul_le`,
 `mulDiv512Down?_lt_succ_mul`, `mulDiv512Up?_mul_ge`, and
 `mulDiv512Up?_mul_le_add_pred`. They also mirror the existing `mulDiv`
 convenience surface with numerator commutativity, zero-numerator, and exact
-same-denominator cancellation lemmas.
+same-denominator cancellation lemmas. Full-precision ceil/floor exactness is
+covered by `mulDiv512Up?_eq_down_of_dvd` and
+`mulDiv512Up?_some_succ_of_not_dvd`, matching the older 256-bit `mulDiv`
+divisibility proof shape.
 
 `Verity.Proofs.Stdlib.Automation` mirrors the full-precision fit/rejection iff
 lemmas under automation-friendly names (`mulDiv512Down?_some_iff`,

From 67980be376548e6ad867d3fc1e961d0972dd0085 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 05:15:25 +0200
Subject: [PATCH 08/18] Document mulDiv512 API helpers

---
 docs-site/content/edsl-api-reference.mdx | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/docs-site/content/edsl-api-reference.mdx b/docs-site/content/edsl-api-reference.mdx
index bac0b4265..a3406a1fb 100644
--- a/docs-site/content/edsl-api-reference.mdx
+++ b/docs-site/content/edsl-api-reference.mdx
@@ -326,6 +326,30 @@ def wDivUp (a b : Uint256) : Uint256
 - Exact cancellation and wad identity lemmas: `mulDivDown_cancel_right/left`, `mulDivUp_cancel_right/left`, `wMulDown_one_left/right`, `wDivUp_by_wad` (`Verity/Proofs/Stdlib/Math.lean`)
 - Wad-specialized helper lemmas: `wMulDown_nat_eq`, `wDivUp_nat_eq`, `wDivUp_antitone_right` (`Verity/Proofs/Stdlib/Math.lean`)
 
+### Full-precision `mulDiv512`
+
+Proof/modeling helpers for Solidity `Math.mulDiv` / `FullMath.mulDiv`
+semantics live in `Stdlib.Math`:
+
+```lean
+def mulDiv512Down? (a b c : Uint256) : Option Uint256
+
+def mulDiv512Up? (a b c : Uint256) : Option Uint256
+```
+
+These compute `a * b` in unbounded natural-number precision and return `none`
+only when the divisor is zero or the final floor/ceil quotient does not fit in
+`uint256`. They are EDSL proof helpers; first-class compiler lowering for a
+512-bit division primitive remains tracked separately.
+
+**Proof lemmas**
+
+- Fit/rejection lemmas: `mulDiv512Down?_some`, `mulDiv512Down?_none_of_zero_divisor`, `mulDiv512Down?_none_of_overflow`, `mulDiv512Down?_isSome_iff`, `mulDiv512Down?_isNone_iff`, `mulDiv512Up?_some`, `mulDiv512Up?_none_of_zero_divisor`, `mulDiv512Up?_none_of_overflow`, `mulDiv512Up?_isSome_iff`, `mulDiv512Up?_isNone_iff` (`Verity/Proofs/Stdlib/Math.lean`)
+- Result-characterization lemmas: `mulDiv512Down?_eq_some_iff`, `mulDiv512Up?_eq_some_iff` (`Verity/Proofs/Stdlib/Math.lean`)
+- Sandwich lemmas: `mulDiv512Down?_mul_le`, `mulDiv512Down?_lt_succ_mul`, `mulDiv512Up?_mul_ge`, `mulDiv512Up?_mul_le_add_pred` (`Verity/Proofs/Stdlib/Math.lean`)
+- Rounding and shape lemmas: `mulDiv512Down?_comm`, `mulDiv512Up?_comm`, `mulDiv512Up?_eq_down_of_dvd`, `mulDiv512Up?_some_succ_of_not_dvd`, `mulDiv512Down?_zero_left/right`, `mulDiv512Up?_zero_left/right`, `mulDiv512Down?_cancel_right/left`, `mulDiv512Up?_cancel_right/left` (`Verity/Proofs/Stdlib/Math.lean`)
+- Automation mirrors: `mulDiv512Down?_some_iff`, `mulDiv512Down?_none_iff`, `mulDiv512Up?_some_iff`, `mulDiv512Up?_none_iff` (`Verity/Proofs/Stdlib/Automation.lean`)
+
 ## Same-Contract Helper Calls
 
 Inside `verity_contract`, call reusable same-contract helpers with ordinary function-call syntax. Do not write `internalCall` or `internalCallAssign` in source contracts; those names are compilation-model IR constructors used after macro lowering.

From e8256882a1c6da5f3b0abd54990204f01d97872b Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 05:23:32 +0200
Subject: [PATCH 09/18] Add mulDiv512 rounding gap lemmas

---
 PrintAxioms.lean                         |  5 ++-
 Verity/Proofs/Stdlib/Math.lean           | 55 ++++++++++++++++++++++++
 docs-site/content/edsl-api-reference.mdx |  2 +-
 docs/ARITHMETIC_PROFILE.md               |  4 +-
 4 files changed, 63 insertions(+), 3 deletions(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index e150f0735..39c4dce87 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -626,6 +626,9 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- #print axioms Verity.Proofs.Stdlib.Math.nat_ceil_div_eq_div_add_one_of_not_dvd  -- private
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_eq_down_of_dvd
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_some_succ_of_not_dvd
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_le_up
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_le_down_add_one
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_eq_down_or_succ
 #print axioms Verity.Proofs.Stdlib.Math.mulDivUp_le_mulDivDown_add_one
 #print axioms Verity.Proofs.Stdlib.Math.mulDivUp_eq_mulDivDown_or_succ
 #print axioms Verity.Proofs.Stdlib.Math.mulDivUp_eq_mulDivDown_of_dvd
@@ -3836,4 +3839,4 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Compiler/Proofs/YulGeneration/ReferenceOracle/Semantics.lean
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_sender
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
--- Total: 3660 theorems/lemmas (2711 public, 949 private, 0 sorry'd)
+-- Total: 3663 theorems/lemmas (2714 public, 949 private, 0 sorry'd)
diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index 008fe2447..0486b0524 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -669,6 +669,45 @@ theorem mulDiv512Up?_some_succ_of_not_dvd (a b c : Uint256)
   rw [mulDiv512Up?_some (a := a) (b := b) (c := c) hC hFit]
   congr
 
+/-- A successful full-precision ceil result never rounds below the matching
+floor result. -/
+theorem mulDiv512Down?_le_up (a b c down up : Uint256)
+    (hDown : mulDiv512Down? a b c = some down)
+    (hUp : mulDiv512Up? a b c = some up) :
+    (down : Nat) ≤ (up : Nat) := by
+  rcases (mulDiv512Down?_eq_some_iff a b c down).mp hDown with ⟨_hCDown, hDownFit, hDownOut⟩
+  rcases (mulDiv512Up?_eq_some_iff a b c up).mp hUp with ⟨_hCUp, hUpFit, hUpOut⟩
+  rw [← hDownOut, ← hUpOut]
+  simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hDownFit),
+    Nat.mod_eq_of_lt (lt_modulus_of_le_max hUpFit)]
+  apply Nat.div_le_div_right
+  exact Nat.le_add_right _ _
+
+/-- A successful full-precision ceil result is at most one quotient step above
+the matching floor result. -/
+theorem mulDiv512Up?_le_down_add_one (a b c down up : Uint256)
+    (hDown : mulDiv512Down? a b c = some down)
+    (hUp : mulDiv512Up? a b c = some up) :
+    (up : Nat) ≤ (down : Nat) + 1 := by
+  rcases (mulDiv512Down?_eq_some_iff a b c down).mp hDown with ⟨hC, hDownFit, hDownOut⟩
+  rcases (mulDiv512Up?_eq_some_iff a b c up).mp hUp with ⟨_hCUp, hUpFit, hUpOut⟩
+  rw [← hDownOut, ← hUpOut]
+  simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hDownFit),
+    Nat.mod_eq_of_lt (lt_modulus_of_le_max hUpFit)]
+  exact nat_ceil_div_le_div_add_one ((a : Nat) * (b : Nat)) (c : Nat) hC
+
+/-- Successful full-precision ceil and floor results either match exactly or
+differ by one quotient step. -/
+theorem mulDiv512Up?_eq_down_or_succ (a b c down up : Uint256)
+    (hDown : mulDiv512Down? a b c = some down)
+    (hUp : mulDiv512Up? a b c = some up) :
+    (up : Nat) = (down : Nat) ∨ (up : Nat) = (down : Nat) + 1 := by
+  have hLower : (down : Nat) ≤ (up : Nat) :=
+    mulDiv512Down?_le_up a b c down up hDown hUp
+  have hUpper : (up : Nat) ≤ (down : Nat) + 1 :=
+    mulDiv512Up?_le_down_add_one a b c down up hDown hUp
+  omega
+
 /-- The ceil helper exceeds the floor helper by at most one quotient step when both are exact. -/
 theorem mulDivUp_le_mulDivDown_add_one (a b c : Uint256)
     (hC : c ≠ 0)
@@ -1344,6 +1383,22 @@ safeDiv:
 
 /-! ## Fixed-point Helper Summary
 
+Full-precision mulDiv512 helpers:
+- `mulDiv512Down?_some` / `mulDiv512Up?_some` — return exact natural quotients when they fit
+- `mulDiv512Down?_none_of_zero_divisor` / `mulDiv512Up?_none_of_zero_divisor` — reject zero divisors
+- `mulDiv512Down?_none_of_overflow` / `mulDiv512Up?_none_of_overflow` — reject overflowing quotients
+- `mulDiv512Down?_eq_some_iff` / `mulDiv512Up?_eq_some_iff` — characterize successful results
+- `mulDiv512Down?_isSome_iff` / `mulDiv512Up?_isSome_iff` — characterize fit conditions
+- `mulDiv512Down?_isNone_iff` / `mulDiv512Up?_isNone_iff` — characterize rejection conditions
+- `mulDiv512Down?_mul_le` / `mulDiv512Down?_lt_succ_mul` — floor sandwich bounds
+- `mulDiv512Up?_mul_ge` / `mulDiv512Up?_mul_le_add_pred` — ceil sandwich bounds
+- `mulDiv512Down?_comm` / `mulDiv512Up?_comm` — numerator multiplication order does not matter
+- `mulDiv512Down?_zero_left/right` / `mulDiv512Up?_zero_left/right` — zero numerators collapse helpers
+- `mulDiv512Down?_cancel_right/left` / `mulDiv512Up?_cancel_right/left` — exact same-denominator cancellation
+- `mulDiv512Down?_wide_product_regression` / `mulDiv512Up?_wide_product_regression` — products may exceed 256 bits when quotients fit
+- `mulDiv512Up?_eq_down_of_dvd` / `mulDiv512Up?_some_succ_of_not_dvd` — ceil/floor divisibility shape
+- `mulDiv512Down?_le_up` / `mulDiv512Up?_le_down_add_one` / `mulDiv512Up?_eq_down_or_succ` — ceil/floor one-step rounding boundary
+
 26. mulDivDown_nat_eq — exact floor division when the numerator fits
 27. mulDivDown_mul_le — floor result never overshoots the numerator
 28. mulDivDown_pos — floor division is positive once the numerator reaches one divisor-width
diff --git a/docs-site/content/edsl-api-reference.mdx b/docs-site/content/edsl-api-reference.mdx
index a3406a1fb..8c7b8ca48 100644
--- a/docs-site/content/edsl-api-reference.mdx
+++ b/docs-site/content/edsl-api-reference.mdx
@@ -347,7 +347,7 @@ only when the divisor is zero or the final floor/ceil quotient does not fit in
 - Fit/rejection lemmas: `mulDiv512Down?_some`, `mulDiv512Down?_none_of_zero_divisor`, `mulDiv512Down?_none_of_overflow`, `mulDiv512Down?_isSome_iff`, `mulDiv512Down?_isNone_iff`, `mulDiv512Up?_some`, `mulDiv512Up?_none_of_zero_divisor`, `mulDiv512Up?_none_of_overflow`, `mulDiv512Up?_isSome_iff`, `mulDiv512Up?_isNone_iff` (`Verity/Proofs/Stdlib/Math.lean`)
 - Result-characterization lemmas: `mulDiv512Down?_eq_some_iff`, `mulDiv512Up?_eq_some_iff` (`Verity/Proofs/Stdlib/Math.lean`)
 - Sandwich lemmas: `mulDiv512Down?_mul_le`, `mulDiv512Down?_lt_succ_mul`, `mulDiv512Up?_mul_ge`, `mulDiv512Up?_mul_le_add_pred` (`Verity/Proofs/Stdlib/Math.lean`)
-- Rounding and shape lemmas: `mulDiv512Down?_comm`, `mulDiv512Up?_comm`, `mulDiv512Up?_eq_down_of_dvd`, `mulDiv512Up?_some_succ_of_not_dvd`, `mulDiv512Down?_zero_left/right`, `mulDiv512Up?_zero_left/right`, `mulDiv512Down?_cancel_right/left`, `mulDiv512Up?_cancel_right/left` (`Verity/Proofs/Stdlib/Math.lean`)
+- Rounding and shape lemmas: `mulDiv512Down?_comm`, `mulDiv512Up?_comm`, `mulDiv512Down?_le_up`, `mulDiv512Up?_le_down_add_one`, `mulDiv512Up?_eq_down_or_succ`, `mulDiv512Up?_eq_down_of_dvd`, `mulDiv512Up?_some_succ_of_not_dvd`, `mulDiv512Down?_zero_left/right`, `mulDiv512Up?_zero_left/right`, `mulDiv512Down?_cancel_right/left`, `mulDiv512Up?_cancel_right/left` (`Verity/Proofs/Stdlib/Math.lean`)
 - Automation mirrors: `mulDiv512Down?_some_iff`, `mulDiv512Down?_none_iff`, `mulDiv512Up?_some_iff`, `mulDiv512Up?_none_iff` (`Verity/Proofs/Stdlib/Automation.lean`)
 
 ## Same-Contract Helper Calls
diff --git a/docs/ARITHMETIC_PROFILE.md b/docs/ARITHMETIC_PROFILE.md
index 7d4ca1127..6cacf5a3c 100644
--- a/docs/ARITHMETIC_PROFILE.md
+++ b/docs/ARITHMETIC_PROFILE.md
@@ -97,7 +97,9 @@ convenience surface with numerator commutativity, zero-numerator, and exact
 same-denominator cancellation lemmas. Full-precision ceil/floor exactness is
 covered by `mulDiv512Up?_eq_down_of_dvd` and
 `mulDiv512Up?_some_succ_of_not_dvd`, matching the older 256-bit `mulDiv`
-divisibility proof shape.
+divisibility proof shape. Successful ceil/floor result pairs also expose the
+same one-step rounding boundary through `mulDiv512Down?_le_up`,
+`mulDiv512Up?_le_down_add_one`, and `mulDiv512Up?_eq_down_or_succ`.
 
 `Verity.Proofs.Stdlib.Automation` mirrors the full-precision fit/rejection iff
 lemmas under automation-friendly names (`mulDiv512Down?_some_iff`,

From 6011197a0da8b1038d70d53bdfea2f4b3b6f7b66 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 05:28:03 +0200
Subject: [PATCH 10/18] Add mulDiv512 monotonicity lemmas

---
 PrintAxioms.lean                         |  6 ++-
 Verity/Proofs/Stdlib/Math.lean           | 57 ++++++++++++++++++++++++
 docs-site/content/edsl-api-reference.mdx |  2 +-
 docs/ARITHMETIC_PROFILE.md               |  5 ++-
 4 files changed, 66 insertions(+), 4 deletions(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index 39c4dce87..72f91d498 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -592,6 +592,8 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_zero_right
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_cancel_right
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_cancel_left
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_monotone_left
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_monotone_right
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_wide_product_regression
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_some
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_none_of_zero_divisor
@@ -606,6 +608,8 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_zero_right
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_cancel_right
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_cancel_left
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_monotone_left
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_monotone_right
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_wide_product_regression
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_nat_eq
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_mul_le
@@ -3839,4 +3843,4 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Compiler/Proofs/YulGeneration/ReferenceOracle/Semantics.lean
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_sender
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
--- Total: 3663 theorems/lemmas (2714 public, 949 private, 0 sorry'd)
+-- Total: 3667 theorems/lemmas (2718 public, 949 private, 0 sorry'd)
diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index 0486b0524..b48c53512 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -165,6 +165,34 @@ theorem mulDiv512Down?_cancel_left (a c : Uint256)
   rw [mulDiv512Down?_comm c a c]
   exact mulDiv512Down?_cancel_right a c hC
 
+/-- Full-precision floor multiplication is monotone in its left numerator
+operand for successful results. -/
+theorem mulDiv512Down?_monotone_left (a₁ a₂ b c out₁ out₂ : Uint256)
+    (hA : (a₁ : Nat) ≤ (a₂ : Nat))
+    (h₁ : mulDiv512Down? a₁ b c = some out₁)
+    (h₂ : mulDiv512Down? a₂ b c = some out₂) :
+    (out₁ : Nat) ≤ (out₂ : Nat) := by
+  rcases (mulDiv512Down?_eq_some_iff a₁ b c out₁).mp h₁ with ⟨_hC₁, hFit₁, hOut₁⟩
+  rcases (mulDiv512Down?_eq_some_iff a₂ b c out₂).mp h₂ with ⟨_hC₂, hFit₂, hOut₂⟩
+  rw [← hOut₁, ← hOut₂]
+  simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit₁),
+    Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit₂)]
+  exact Nat.div_le_div_right (Nat.mul_le_mul_right _ hA)
+
+/-- Full-precision floor multiplication is monotone in its right numerator
+operand for successful results. -/
+theorem mulDiv512Down?_monotone_right (a b₁ b₂ c out₁ out₂ : Uint256)
+    (hB : (b₁ : Nat) ≤ (b₂ : Nat))
+    (h₁ : mulDiv512Down? a b₁ c = some out₁)
+    (h₂ : mulDiv512Down? a b₂ c = some out₂) :
+    (out₁ : Nat) ≤ (out₂ : Nat) := by
+  rcases (mulDiv512Down?_eq_some_iff a b₁ c out₁).mp h₁ with ⟨_hC₁, hFit₁, hOut₁⟩
+  rcases (mulDiv512Down?_eq_some_iff a b₂ c out₂).mp h₂ with ⟨_hC₂, hFit₂, hOut₂⟩
+  rw [← hOut₁, ← hOut₂]
+  simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit₁),
+    Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit₂)]
+  exact Nat.div_le_div_right (Nat.mul_le_mul_left _ hB)
+
 /-- Regression: full-precision floor `mulDiv512` permits a 256-bit-overflowing
 intermediate product when the final quotient fits. -/
 theorem mulDiv512Down?_wide_product_regression :
@@ -330,6 +358,34 @@ theorem mulDiv512Up?_cancel_left (a c : Uint256)
   rw [mulDiv512Up?_comm c a c]
   exact mulDiv512Up?_cancel_right a c hC
 
+/-- Full-precision ceil multiplication is monotone in its left numerator
+operand for successful results. -/
+theorem mulDiv512Up?_monotone_left (a₁ a₂ b c out₁ out₂ : Uint256)
+    (hA : (a₁ : Nat) ≤ (a₂ : Nat))
+    (h₁ : mulDiv512Up? a₁ b c = some out₁)
+    (h₂ : mulDiv512Up? a₂ b c = some out₂) :
+    (out₁ : Nat) ≤ (out₂ : Nat) := by
+  rcases (mulDiv512Up?_eq_some_iff a₁ b c out₁).mp h₁ with ⟨_hC₁, hFit₁, hOut₁⟩
+  rcases (mulDiv512Up?_eq_some_iff a₂ b c out₂).mp h₂ with ⟨_hC₂, hFit₂, hOut₂⟩
+  rw [← hOut₁, ← hOut₂]
+  simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit₁),
+    Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit₂)]
+  exact Nat.div_le_div_right (Nat.add_le_add_right (Nat.mul_le_mul_right _ hA) _)
+
+/-- Full-precision ceil multiplication is monotone in its right numerator
+operand for successful results. -/
+theorem mulDiv512Up?_monotone_right (a b₁ b₂ c out₁ out₂ : Uint256)
+    (hB : (b₁ : Nat) ≤ (b₂ : Nat))
+    (h₁ : mulDiv512Up? a b₁ c = some out₁)
+    (h₂ : mulDiv512Up? a b₂ c = some out₂) :
+    (out₁ : Nat) ≤ (out₂ : Nat) := by
+  rcases (mulDiv512Up?_eq_some_iff a b₁ c out₁).mp h₁ with ⟨_hC₁, hFit₁, hOut₁⟩
+  rcases (mulDiv512Up?_eq_some_iff a b₂ c out₂).mp h₂ with ⟨_hC₂, hFit₂, hOut₂⟩
+  rw [← hOut₁, ← hOut₂]
+  simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit₁),
+    Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit₂)]
+  exact Nat.div_le_div_right (Nat.add_le_add_right (Nat.mul_le_mul_left _ hB) _)
+
 /-- Regression: full-precision ceil `mulDiv512` permits a 256-bit-overflowing
 intermediate product when the rounded quotient fits. -/
 theorem mulDiv512Up?_wide_product_regression :
@@ -1393,6 +1449,7 @@ Full-precision mulDiv512 helpers:
 - `mulDiv512Down?_mul_le` / `mulDiv512Down?_lt_succ_mul` — floor sandwich bounds
 - `mulDiv512Up?_mul_ge` / `mulDiv512Up?_mul_le_add_pred` — ceil sandwich bounds
 - `mulDiv512Down?_comm` / `mulDiv512Up?_comm` — numerator multiplication order does not matter
+- `mulDiv512Down?_monotone_left/right` / `mulDiv512Up?_monotone_left/right` — numerator monotonicity
 - `mulDiv512Down?_zero_left/right` / `mulDiv512Up?_zero_left/right` — zero numerators collapse helpers
 - `mulDiv512Down?_cancel_right/left` / `mulDiv512Up?_cancel_right/left` — exact same-denominator cancellation
 - `mulDiv512Down?_wide_product_regression` / `mulDiv512Up?_wide_product_regression` — products may exceed 256 bits when quotients fit
diff --git a/docs-site/content/edsl-api-reference.mdx b/docs-site/content/edsl-api-reference.mdx
index 8c7b8ca48..47c05c8e2 100644
--- a/docs-site/content/edsl-api-reference.mdx
+++ b/docs-site/content/edsl-api-reference.mdx
@@ -347,7 +347,7 @@ only when the divisor is zero or the final floor/ceil quotient does not fit in
 - Fit/rejection lemmas: `mulDiv512Down?_some`, `mulDiv512Down?_none_of_zero_divisor`, `mulDiv512Down?_none_of_overflow`, `mulDiv512Down?_isSome_iff`, `mulDiv512Down?_isNone_iff`, `mulDiv512Up?_some`, `mulDiv512Up?_none_of_zero_divisor`, `mulDiv512Up?_none_of_overflow`, `mulDiv512Up?_isSome_iff`, `mulDiv512Up?_isNone_iff` (`Verity/Proofs/Stdlib/Math.lean`)
 - Result-characterization lemmas: `mulDiv512Down?_eq_some_iff`, `mulDiv512Up?_eq_some_iff` (`Verity/Proofs/Stdlib/Math.lean`)
 - Sandwich lemmas: `mulDiv512Down?_mul_le`, `mulDiv512Down?_lt_succ_mul`, `mulDiv512Up?_mul_ge`, `mulDiv512Up?_mul_le_add_pred` (`Verity/Proofs/Stdlib/Math.lean`)
-- Rounding and shape lemmas: `mulDiv512Down?_comm`, `mulDiv512Up?_comm`, `mulDiv512Down?_le_up`, `mulDiv512Up?_le_down_add_one`, `mulDiv512Up?_eq_down_or_succ`, `mulDiv512Up?_eq_down_of_dvd`, `mulDiv512Up?_some_succ_of_not_dvd`, `mulDiv512Down?_zero_left/right`, `mulDiv512Up?_zero_left/right`, `mulDiv512Down?_cancel_right/left`, `mulDiv512Up?_cancel_right/left` (`Verity/Proofs/Stdlib/Math.lean`)
+- Rounding and shape lemmas: `mulDiv512Down?_comm`, `mulDiv512Up?_comm`, `mulDiv512Down?_monotone_left/right`, `mulDiv512Up?_monotone_left/right`, `mulDiv512Down?_le_up`, `mulDiv512Up?_le_down_add_one`, `mulDiv512Up?_eq_down_or_succ`, `mulDiv512Up?_eq_down_of_dvd`, `mulDiv512Up?_some_succ_of_not_dvd`, `mulDiv512Down?_zero_left/right`, `mulDiv512Up?_zero_left/right`, `mulDiv512Down?_cancel_right/left`, `mulDiv512Up?_cancel_right/left` (`Verity/Proofs/Stdlib/Math.lean`)
 - Automation mirrors: `mulDiv512Down?_some_iff`, `mulDiv512Down?_none_iff`, `mulDiv512Up?_some_iff`, `mulDiv512Up?_none_iff` (`Verity/Proofs/Stdlib/Automation.lean`)
 
 ## Same-Contract Helper Calls
diff --git a/docs/ARITHMETIC_PROFILE.md b/docs/ARITHMETIC_PROFILE.md
index 6cacf5a3c..52ff6670f 100644
--- a/docs/ARITHMETIC_PROFILE.md
+++ b/docs/ARITHMETIC_PROFILE.md
@@ -93,8 +93,9 @@ expose the failure boundary. Successful full-precision results also have
 direct sandwich lemmas: `mulDiv512Down?_mul_le`,
 `mulDiv512Down?_lt_succ_mul`, `mulDiv512Up?_mul_ge`, and
 `mulDiv512Up?_mul_le_add_pred`. They also mirror the existing `mulDiv`
-convenience surface with numerator commutativity, zero-numerator, and exact
-same-denominator cancellation lemmas. Full-precision ceil/floor exactness is
+convenience surface with numerator commutativity, successful-result numerator
+monotonicity, zero-numerator, and exact same-denominator cancellation lemmas.
+Full-precision ceil/floor exactness is
 covered by `mulDiv512Up?_eq_down_of_dvd` and
 `mulDiv512Up?_some_succ_of_not_dvd`, matching the older 256-bit `mulDiv`
 divisibility proof shape. Successful ceil/floor result pairs also expose the

From 3a4f3fd6322185c028105d0ee4bacbae190734fc Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 05:36:51 +0200
Subject: [PATCH 11/18] Add mulDiv512 divisor antitone lemmas

---
 PrintAxioms.lean                         |  5 +-
 Verity/Proofs/Stdlib/Math.lean           | 61 ++++++++++++++++++++++++
 docs-site/content/edsl-api-reference.mdx |  2 +-
 docs/ARITHMETIC_PROFILE.md               |  3 +-
 4 files changed, 68 insertions(+), 3 deletions(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index 72f91d498..85a57c8de 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -579,6 +579,7 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- #print axioms Verity.Proofs.Stdlib.Math.max_uint256_lt_modulus  -- private
 -- #print axioms Verity.Proofs.Stdlib.Math.ceil_mul_div_ge  -- private
 -- #print axioms Verity.Proofs.Stdlib.Math.ceil_mul_div_le_add_pred  -- private
+-- #print axioms Verity.Proofs.Stdlib.Math.nat_ceil_div_antitone_divisor  -- private
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_some
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_none_of_zero_divisor
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_none_of_overflow
@@ -594,6 +595,7 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_cancel_left
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_monotone_left
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_monotone_right
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_antitone_divisor
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_wide_product_regression
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_some
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_none_of_zero_divisor
@@ -610,6 +612,7 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_cancel_left
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_monotone_left
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_monotone_right
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_antitone_divisor
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_wide_product_regression
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_nat_eq
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_mul_le
@@ -3843,4 +3846,4 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Compiler/Proofs/YulGeneration/ReferenceOracle/Semantics.lean
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_sender
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
--- Total: 3667 theorems/lemmas (2718 public, 949 private, 0 sorry'd)
+-- Total: 3670 theorems/lemmas (2720 public, 950 private, 0 sorry'd)
diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index b48c53512..c1593b4c6 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -44,6 +44,37 @@ private theorem ceil_mul_div_le_add_pred (n d : Nat) :
     ((n + (d - 1)) / d) * d ≤ n + (d - 1) := by
   simpa [Nat.mul_comm] using Nat.mul_div_le (n + (d - 1)) d
 
+private theorem nat_ceil_div_antitone_divisor (n c₁ c₂ : Nat)
+    (hC : c₁ ≤ c₂)
+    (hC₁ : c₁ ≠ 0)
+    (hC₂ : c₂ ≠ 0) :
+    (n + (c₂ - 1)) / c₂ ≤ (n + (c₁ - 1)) / c₁ := by
+  have hC₂Pos : 0 < c₂ := Nat.pos_of_ne_zero hC₂
+  have hUpper :
+      ((n + (c₂ - 1)) / c₂) * c₂ < n + c₂ := by
+    calc
+      ((n + (c₂ - 1)) / c₂) * c₂ ≤ n + (c₂ - 1) :=
+        ceil_mul_div_le_add_pred n c₂
+      _ < n + c₂ := Nat.add_lt_add_left (Nat.sub_lt hC₂Pos (by decide)) _
+  have hLower :
+      n ≤ ((n + (c₁ - 1)) / c₁) * c₂ := by
+    exact Nat.le_trans
+      (ceil_mul_div_ge n c₁ (Nat.pos_of_ne_zero hC₁))
+      (Nat.mul_le_mul_left _ hC)
+  have hLt :
+      ((n + (c₂ - 1)) / c₂) * c₂ <
+        (((n + (c₁ - 1)) / c₁) + 1) * c₂ := by
+    calc
+      ((n + (c₂ - 1)) / c₂) * c₂ < n + c₂ := hUpper
+      _ ≤ ((n + (c₁ - 1)) / c₁) * c₂ + c₂ := Nat.add_le_add_right hLower _
+      _ = (((n + (c₁ - 1)) / c₁) + 1) * c₂ := by
+            simp [Nat.right_distrib]
+  have hLt' :
+      c₂ * ((n + (c₂ - 1)) / c₂) <
+        c₂ * (((n + (c₁ - 1)) / c₁) + 1) := by
+    simpa [Nat.mul_comm] using hLt
+  exact Nat.lt_succ_iff.mp (Nat.lt_of_mul_lt_mul_left hLt')
+
 /-- `mulDiv512Down?` returns the exact full-precision floor quotient when it fits. -/
 theorem mulDiv512Down?_some (a b c : Uint256)
     (hC : (c : Nat) ≠ 0)
@@ -193,6 +224,21 @@ theorem mulDiv512Down?_monotone_right (a b₁ b₂ c out₁ out₂ : Uint256)
     Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit₂)]
   exact Nat.div_le_div_right (Nat.mul_le_mul_left _ hB)
 
+/-- Full-precision floor multiplication is antitone in the divisor for
+successful results. -/
+theorem mulDiv512Down?_antitone_divisor (a b c₁ c₂ out₁ out₂ : Uint256)
+    (hC : (c₁ : Nat) ≤ (c₂ : Nat))
+    (hC₁ : (c₁ : Nat) ≠ 0)
+    (h₁ : mulDiv512Down? a b c₁ = some out₁)
+    (h₂ : mulDiv512Down? a b c₂ = some out₂) :
+    (out₂ : Nat) ≤ (out₁ : Nat) := by
+  rcases (mulDiv512Down?_eq_some_iff a b c₁ out₁).mp h₁ with ⟨_hC₁Some, hFit₁, hOut₁⟩
+  rcases (mulDiv512Down?_eq_some_iff a b c₂ out₂).mp h₂ with ⟨_hC₂Some, hFit₂, hOut₂⟩
+  rw [← hOut₁, ← hOut₂]
+  simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit₁),
+    Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit₂)]
+  exact Nat.div_le_div_left hC (Nat.pos_of_ne_zero hC₁)
+
 /-- Regression: full-precision floor `mulDiv512` permits a 256-bit-overflowing
 intermediate product when the final quotient fits. -/
 theorem mulDiv512Down?_wide_product_regression :
@@ -386,6 +432,20 @@ theorem mulDiv512Up?_monotone_right (a b₁ b₂ c out₁ out₂ : Uint256)
     Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit₂)]
   exact Nat.div_le_div_right (Nat.add_le_add_right (Nat.mul_le_mul_left _ hB) _)
 
+/-- Full-precision ceil multiplication is antitone in the divisor for
+successful results. -/
+theorem mulDiv512Up?_antitone_divisor (a b c₁ c₂ out₁ out₂ : Uint256)
+    (hC : (c₁ : Nat) ≤ (c₂ : Nat))
+    (h₁ : mulDiv512Up? a b c₁ = some out₁)
+    (h₂ : mulDiv512Up? a b c₂ = some out₂) :
+    (out₂ : Nat) ≤ (out₁ : Nat) := by
+  rcases (mulDiv512Up?_eq_some_iff a b c₁ out₁).mp h₁ with ⟨hC₁, hFit₁, hOut₁⟩
+  rcases (mulDiv512Up?_eq_some_iff a b c₂ out₂).mp h₂ with ⟨hC₂, hFit₂, hOut₂⟩
+  rw [← hOut₁, ← hOut₂]
+  simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit₁),
+    Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit₂)]
+  exact nat_ceil_div_antitone_divisor ((a : Nat) * (b : Nat)) (c₁ : Nat) (c₂ : Nat) hC hC₁ hC₂
+
 /-- Regression: full-precision ceil `mulDiv512` permits a 256-bit-overflowing
 intermediate product when the rounded quotient fits. -/
 theorem mulDiv512Up?_wide_product_regression :
@@ -1450,6 +1510,7 @@ Full-precision mulDiv512 helpers:
 - `mulDiv512Up?_mul_ge` / `mulDiv512Up?_mul_le_add_pred` — ceil sandwich bounds
 - `mulDiv512Down?_comm` / `mulDiv512Up?_comm` — numerator multiplication order does not matter
 - `mulDiv512Down?_monotone_left/right` / `mulDiv512Up?_monotone_left/right` — numerator monotonicity
+- `mulDiv512Down?_antitone_divisor` / `mulDiv512Up?_antitone_divisor` — divisor antitonicity
 - `mulDiv512Down?_zero_left/right` / `mulDiv512Up?_zero_left/right` — zero numerators collapse helpers
 - `mulDiv512Down?_cancel_right/left` / `mulDiv512Up?_cancel_right/left` — exact same-denominator cancellation
 - `mulDiv512Down?_wide_product_regression` / `mulDiv512Up?_wide_product_regression` — products may exceed 256 bits when quotients fit
diff --git a/docs-site/content/edsl-api-reference.mdx b/docs-site/content/edsl-api-reference.mdx
index 47c05c8e2..f6c3af74a 100644
--- a/docs-site/content/edsl-api-reference.mdx
+++ b/docs-site/content/edsl-api-reference.mdx
@@ -347,7 +347,7 @@ only when the divisor is zero or the final floor/ceil quotient does not fit in
 - Fit/rejection lemmas: `mulDiv512Down?_some`, `mulDiv512Down?_none_of_zero_divisor`, `mulDiv512Down?_none_of_overflow`, `mulDiv512Down?_isSome_iff`, `mulDiv512Down?_isNone_iff`, `mulDiv512Up?_some`, `mulDiv512Up?_none_of_zero_divisor`, `mulDiv512Up?_none_of_overflow`, `mulDiv512Up?_isSome_iff`, `mulDiv512Up?_isNone_iff` (`Verity/Proofs/Stdlib/Math.lean`)
 - Result-characterization lemmas: `mulDiv512Down?_eq_some_iff`, `mulDiv512Up?_eq_some_iff` (`Verity/Proofs/Stdlib/Math.lean`)
 - Sandwich lemmas: `mulDiv512Down?_mul_le`, `mulDiv512Down?_lt_succ_mul`, `mulDiv512Up?_mul_ge`, `mulDiv512Up?_mul_le_add_pred` (`Verity/Proofs/Stdlib/Math.lean`)
-- Rounding and shape lemmas: `mulDiv512Down?_comm`, `mulDiv512Up?_comm`, `mulDiv512Down?_monotone_left/right`, `mulDiv512Up?_monotone_left/right`, `mulDiv512Down?_le_up`, `mulDiv512Up?_le_down_add_one`, `mulDiv512Up?_eq_down_or_succ`, `mulDiv512Up?_eq_down_of_dvd`, `mulDiv512Up?_some_succ_of_not_dvd`, `mulDiv512Down?_zero_left/right`, `mulDiv512Up?_zero_left/right`, `mulDiv512Down?_cancel_right/left`, `mulDiv512Up?_cancel_right/left` (`Verity/Proofs/Stdlib/Math.lean`)
+- Rounding and shape lemmas: `mulDiv512Down?_comm`, `mulDiv512Up?_comm`, `mulDiv512Down?_monotone_left/right`, `mulDiv512Up?_monotone_left/right`, `mulDiv512Down?_antitone_divisor`, `mulDiv512Up?_antitone_divisor`, `mulDiv512Down?_le_up`, `mulDiv512Up?_le_down_add_one`, `mulDiv512Up?_eq_down_or_succ`, `mulDiv512Up?_eq_down_of_dvd`, `mulDiv512Up?_some_succ_of_not_dvd`, `mulDiv512Down?_zero_left/right`, `mulDiv512Up?_zero_left/right`, `mulDiv512Down?_cancel_right/left`, `mulDiv512Up?_cancel_right/left` (`Verity/Proofs/Stdlib/Math.lean`)
 - Automation mirrors: `mulDiv512Down?_some_iff`, `mulDiv512Down?_none_iff`, `mulDiv512Up?_some_iff`, `mulDiv512Up?_none_iff` (`Verity/Proofs/Stdlib/Automation.lean`)
 
 ## Same-Contract Helper Calls
diff --git a/docs/ARITHMETIC_PROFILE.md b/docs/ARITHMETIC_PROFILE.md
index 52ff6670f..a21b59ee4 100644
--- a/docs/ARITHMETIC_PROFILE.md
+++ b/docs/ARITHMETIC_PROFILE.md
@@ -94,7 +94,8 @@ direct sandwich lemmas: `mulDiv512Down?_mul_le`,
 `mulDiv512Down?_lt_succ_mul`, `mulDiv512Up?_mul_ge`, and
 `mulDiv512Up?_mul_le_add_pred`. They also mirror the existing `mulDiv`
 convenience surface with numerator commutativity, successful-result numerator
-monotonicity, zero-numerator, and exact same-denominator cancellation lemmas.
+monotonicity, divisor antitonicity, zero-numerator, and exact
+same-denominator cancellation lemmas.
 Full-precision ceil/floor exactness is
 covered by `mulDiv512Up?_eq_down_of_dvd` and
 `mulDiv512Up?_some_succ_of_not_dvd`, matching the older 256-bit `mulDiv`

From c97715a949ecbea76cfe20c17b11afd8f8c0639c Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 05:42:57 +0200
Subject: [PATCH 12/18] Add mulDiv512 rounding bridge lemmas

---
 PrintAxioms.lean                         |  4 +++-
 Verity/Proofs/Stdlib/Math.lean           | 27 ++++++++++++++++++++++++
 docs-site/content/edsl-api-reference.mdx |  2 +-
 docs/ARITHMETIC_PROFILE.md               |  9 +++++---
 4 files changed, 37 insertions(+), 5 deletions(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index 85a57c8de..953d824c5 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -605,6 +605,8 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_mul_ge
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_mul_le_add_pred
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_isNone_iff
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_isSome_of_up_isSome
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_isNone_of_down_isNone
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_comm
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_zero_left
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_zero_right
@@ -3846,4 +3848,4 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Compiler/Proofs/YulGeneration/ReferenceOracle/Semantics.lean
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_sender
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
--- Total: 3670 theorems/lemmas (2720 public, 950 private, 0 sorry'd)
+-- Total: 3672 theorems/lemmas (2722 public, 950 private, 0 sorry'd)
diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index c1593b4c6..021afd348 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -350,6 +350,32 @@ theorem mulDiv512Up?_isNone_iff (a b c : Uint256) :
     · simp [Verity.Stdlib.Math.mulDiv512Up?, hC, hOverflow]
     · simp [Verity.Stdlib.Math.mulDiv512Up?, hC, hOverflow]
 
+/-- If the rounded-up full-precision quotient fits, the matching floor
+quotient also fits. -/
+theorem mulDiv512Down?_isSome_of_up_isSome (a b c : Uint256)
+    (h : (mulDiv512Up? a b c).isSome) :
+    (mulDiv512Down? a b c).isSome := by
+  rw [mulDiv512Up?_isSome_iff] at h
+  rw [mulDiv512Down?_isSome_iff]
+  rcases h with ⟨hC, hFit⟩
+  refine ⟨hC, ?_⟩
+  exact Nat.le_trans
+    (Nat.div_le_div_right (Nat.le_add_right ((a : Nat) * (b : Nat)) ((c : Nat) - 1)))
+    hFit
+
+/-- If the full-precision floor quotient is rejected, the matching rounded-up
+quotient is rejected too. -/
+theorem mulDiv512Up?_isNone_of_down_isNone (a b c : Uint256)
+    (h : (mulDiv512Down? a b c).isNone) :
+    (mulDiv512Up? a b c).isNone := by
+  rw [mulDiv512Down?_isNone_iff] at h
+  rw [mulDiv512Up?_isNone_iff]
+  rcases h with hZero | hOverflow
+  · exact Or.inl hZero
+  · exact Or.inr (Nat.lt_of_lt_of_le hOverflow
+      (Nat.div_le_div_right
+        (Nat.le_add_right ((a : Nat) * (b : Nat)) ((c : Nat) - 1))))
+
 /-- Full-precision ceil multiplication is commutative in its numerator operands. -/
 theorem mulDiv512Up?_comm (a b c : Uint256) :
     mulDiv512Up? a b c = mulDiv512Up? b a c := by
@@ -1511,6 +1537,7 @@ Full-precision mulDiv512 helpers:
 - `mulDiv512Down?_comm` / `mulDiv512Up?_comm` — numerator multiplication order does not matter
 - `mulDiv512Down?_monotone_left/right` / `mulDiv512Up?_monotone_left/right` — numerator monotonicity
 - `mulDiv512Down?_antitone_divisor` / `mulDiv512Up?_antitone_divisor` — divisor antitonicity
+- `mulDiv512Down?_isSome_of_up_isSome` / `mulDiv512Up?_isNone_of_down_isNone` — ceil/floor success and rejection bridge
 - `mulDiv512Down?_zero_left/right` / `mulDiv512Up?_zero_left/right` — zero numerators collapse helpers
 - `mulDiv512Down?_cancel_right/left` / `mulDiv512Up?_cancel_right/left` — exact same-denominator cancellation
 - `mulDiv512Down?_wide_product_regression` / `mulDiv512Up?_wide_product_regression` — products may exceed 256 bits when quotients fit
diff --git a/docs-site/content/edsl-api-reference.mdx b/docs-site/content/edsl-api-reference.mdx
index f6c3af74a..06122c437 100644
--- a/docs-site/content/edsl-api-reference.mdx
+++ b/docs-site/content/edsl-api-reference.mdx
@@ -347,7 +347,7 @@ only when the divisor is zero or the final floor/ceil quotient does not fit in
 - Fit/rejection lemmas: `mulDiv512Down?_some`, `mulDiv512Down?_none_of_zero_divisor`, `mulDiv512Down?_none_of_overflow`, `mulDiv512Down?_isSome_iff`, `mulDiv512Down?_isNone_iff`, `mulDiv512Up?_some`, `mulDiv512Up?_none_of_zero_divisor`, `mulDiv512Up?_none_of_overflow`, `mulDiv512Up?_isSome_iff`, `mulDiv512Up?_isNone_iff` (`Verity/Proofs/Stdlib/Math.lean`)
 - Result-characterization lemmas: `mulDiv512Down?_eq_some_iff`, `mulDiv512Up?_eq_some_iff` (`Verity/Proofs/Stdlib/Math.lean`)
 - Sandwich lemmas: `mulDiv512Down?_mul_le`, `mulDiv512Down?_lt_succ_mul`, `mulDiv512Up?_mul_ge`, `mulDiv512Up?_mul_le_add_pred` (`Verity/Proofs/Stdlib/Math.lean`)
-- Rounding and shape lemmas: `mulDiv512Down?_comm`, `mulDiv512Up?_comm`, `mulDiv512Down?_monotone_left/right`, `mulDiv512Up?_monotone_left/right`, `mulDiv512Down?_antitone_divisor`, `mulDiv512Up?_antitone_divisor`, `mulDiv512Down?_le_up`, `mulDiv512Up?_le_down_add_one`, `mulDiv512Up?_eq_down_or_succ`, `mulDiv512Up?_eq_down_of_dvd`, `mulDiv512Up?_some_succ_of_not_dvd`, `mulDiv512Down?_zero_left/right`, `mulDiv512Up?_zero_left/right`, `mulDiv512Down?_cancel_right/left`, `mulDiv512Up?_cancel_right/left` (`Verity/Proofs/Stdlib/Math.lean`)
+- Rounding and shape lemmas: `mulDiv512Down?_comm`, `mulDiv512Up?_comm`, `mulDiv512Down?_monotone_left/right`, `mulDiv512Up?_monotone_left/right`, `mulDiv512Down?_antitone_divisor`, `mulDiv512Up?_antitone_divisor`, `mulDiv512Down?_isSome_of_up_isSome`, `mulDiv512Up?_isNone_of_down_isNone`, `mulDiv512Down?_le_up`, `mulDiv512Up?_le_down_add_one`, `mulDiv512Up?_eq_down_or_succ`, `mulDiv512Up?_eq_down_of_dvd`, `mulDiv512Up?_some_succ_of_not_dvd`, `mulDiv512Down?_zero_left/right`, `mulDiv512Up?_zero_left/right`, `mulDiv512Down?_cancel_right/left`, `mulDiv512Up?_cancel_right/left` (`Verity/Proofs/Stdlib/Math.lean`)
 - Automation mirrors: `mulDiv512Down?_some_iff`, `mulDiv512Down?_none_iff`, `mulDiv512Up?_some_iff`, `mulDiv512Up?_none_iff` (`Verity/Proofs/Stdlib/Automation.lean`)
 
 ## Same-Contract Helper Calls
diff --git a/docs/ARITHMETIC_PROFILE.md b/docs/ARITHMETIC_PROFILE.md
index a21b59ee4..3b52a6da7 100644
--- a/docs/ARITHMETIC_PROFILE.md
+++ b/docs/ARITHMETIC_PROFILE.md
@@ -99,9 +99,12 @@ same-denominator cancellation lemmas.
 Full-precision ceil/floor exactness is
 covered by `mulDiv512Up?_eq_down_of_dvd` and
 `mulDiv512Up?_some_succ_of_not_dvd`, matching the older 256-bit `mulDiv`
-divisibility proof shape. Successful ceil/floor result pairs also expose the
-same one-step rounding boundary through `mulDiv512Down?_le_up`,
-`mulDiv512Up?_le_down_add_one`, and `mulDiv512Up?_eq_down_or_succ`.
+divisibility proof shape. The success/rejection bridge lemmas
+`mulDiv512Down?_isSome_of_up_isSome` and
+`mulDiv512Up?_isNone_of_down_isNone` connect the two rounding modes. Successful
+ceil/floor result pairs also expose the same one-step rounding boundary through
+`mulDiv512Down?_le_up`, `mulDiv512Up?_le_down_add_one`, and
+`mulDiv512Up?_eq_down_or_succ`.
 
 `Verity.Proofs.Stdlib.Automation` mirrors the full-precision fit/rejection iff
 lemmas under automation-friendly names (`mulDiv512Down?_some_iff`,

From 474caa027769083a41fa196d8b2efb1d3cf3a4b5 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 05:45:45 +0200
Subject: [PATCH 13/18] Remove redundant mulDiv512 divisor hypothesis

---
 Verity/Proofs/Stdlib/Math.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index 021afd348..aea4d4c94 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -228,11 +228,10 @@ theorem mulDiv512Down?_monotone_right (a b₁ b₂ c out₁ out₂ : Uint256)
 successful results. -/
 theorem mulDiv512Down?_antitone_divisor (a b c₁ c₂ out₁ out₂ : Uint256)
     (hC : (c₁ : Nat) ≤ (c₂ : Nat))
-    (hC₁ : (c₁ : Nat) ≠ 0)
     (h₁ : mulDiv512Down? a b c₁ = some out₁)
     (h₂ : mulDiv512Down? a b c₂ = some out₂) :
     (out₂ : Nat) ≤ (out₁ : Nat) := by
-  rcases (mulDiv512Down?_eq_some_iff a b c₁ out₁).mp h₁ with ⟨_hC₁Some, hFit₁, hOut₁⟩
+  rcases (mulDiv512Down?_eq_some_iff a b c₁ out₁).mp h₁ with ⟨hC₁, hFit₁, hOut₁⟩
   rcases (mulDiv512Down?_eq_some_iff a b c₂ out₂).mp h₂ with ⟨_hC₂Some, hFit₂, hOut₂⟩
   rw [← hOut₁, ← hOut₂]
   simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit₁),

From 5c927b7cdb64bdf1c1fa0c7acd4a68ed696c14a4 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 05:50:18 +0200
Subject: [PATCH 14/18] Add mulDiv512 positivity lemmas

---
 PrintAxioms.lean                         |  4 +++-
 Verity/Proofs/Stdlib/Math.lean           | 30 ++++++++++++++++++++++++
 docs-site/content/edsl-api-reference.mdx |  2 +-
 docs/ARITHMETIC_PROFILE.md               |  2 +-
 4 files changed, 35 insertions(+), 3 deletions(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index 953d824c5..2d8edb086 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -591,6 +591,7 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_comm
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_zero_left
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_zero_right
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_pos
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_cancel_right
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_cancel_left
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_monotone_left
@@ -610,6 +611,7 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_comm
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_zero_left
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_zero_right
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_pos
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_cancel_right
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_cancel_left
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_monotone_left
@@ -3848,4 +3850,4 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Compiler/Proofs/YulGeneration/ReferenceOracle/Semantics.lean
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_sender
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
--- Total: 3672 theorems/lemmas (2722 public, 950 private, 0 sorry'd)
+-- Total: 3674 theorems/lemmas (2724 public, 950 private, 0 sorry'd)
diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index aea4d4c94..eb119d658 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -174,6 +174,18 @@ theorem mulDiv512Down?_zero_right (a c : Uint256)
     mulDiv512Down? a 0 c = some 0 := by
   simpa [mulDiv512Down?_comm] using mulDiv512Down?_zero_left a c hC
 
+/-- A successful full-precision floor result is positive once the exact product
+reaches at least one divisor-width. -/
+theorem mulDiv512Down?_pos (a b c out : Uint256)
+    (hLower : (c : Nat) ≤ (a : Nat) * (b : Nat))
+    (h : mulDiv512Down? a b c = some out) :
+    0 < (out : Nat) := by
+  rcases (mulDiv512Down?_eq_some_iff a b c out).mp h with ⟨hC, hFit, hOut⟩
+  have hCPos : 0 < (c : Nat) := Nat.pos_of_ne_zero hC
+  rw [← hOut]
+  simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit)]
+  simpa [Nat.div_pos_iff, hCPos] using hLower
+
 /-- Exact full-precision floor cancellation by the right numerator operand. -/
 theorem mulDiv512Down?_cancel_right (a c : Uint256)
     (hC : (c : Nat) ≠ 0) :
@@ -397,6 +409,23 @@ theorem mulDiv512Up?_zero_right (a c : Uint256)
     mulDiv512Up? a 0 c = some 0 := by
   simpa [mulDiv512Up?_comm] using mulDiv512Up?_zero_left a c hC
 
+/-- A successful full-precision ceil result is positive whenever both numerator
+factors are positive. -/
+theorem mulDiv512Up?_pos (a b c out : Uint256)
+    (hA : 0 < (a : Nat))
+    (hB : 0 < (b : Nat))
+    (h : mulDiv512Up? a b c = some out) :
+    0 < (out : Nat) := by
+  rcases (mulDiv512Up?_eq_some_iff a b c out).mp h with ⟨hC, hFit, hOut⟩
+  have hCPos : 0 < (c : Nat) := Nat.pos_of_ne_zero hC
+  have hProdPos : 0 < (a : Nat) * (b : Nat) := Nat.mul_pos hA hB
+  have hDivisorLe :
+      (c : Nat) ≤ (a : Nat) * (b : Nat) + ((c : Nat) - 1) := by
+    omega
+  rw [← hOut]
+  simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit)]
+  simpa [Nat.div_pos_iff, hCPos] using hDivisorLe
+
 /-- Exact full-precision ceil cancellation by the right numerator operand. -/
 theorem mulDiv512Up?_cancel_right (a c : Uint256)
     (hC : (c : Nat) ≠ 0) :
@@ -1537,6 +1566,7 @@ Full-precision mulDiv512 helpers:
 - `mulDiv512Down?_monotone_left/right` / `mulDiv512Up?_monotone_left/right` — numerator monotonicity
 - `mulDiv512Down?_antitone_divisor` / `mulDiv512Up?_antitone_divisor` — divisor antitonicity
 - `mulDiv512Down?_isSome_of_up_isSome` / `mulDiv512Up?_isNone_of_down_isNone` — ceil/floor success and rejection bridge
+- `mulDiv512Down?_pos` / `mulDiv512Up?_pos` — positive full-precision results under nonzero-output conditions
 - `mulDiv512Down?_zero_left/right` / `mulDiv512Up?_zero_left/right` — zero numerators collapse helpers
 - `mulDiv512Down?_cancel_right/left` / `mulDiv512Up?_cancel_right/left` — exact same-denominator cancellation
 - `mulDiv512Down?_wide_product_regression` / `mulDiv512Up?_wide_product_regression` — products may exceed 256 bits when quotients fit
diff --git a/docs-site/content/edsl-api-reference.mdx b/docs-site/content/edsl-api-reference.mdx
index 06122c437..d86d13dcd 100644
--- a/docs-site/content/edsl-api-reference.mdx
+++ b/docs-site/content/edsl-api-reference.mdx
@@ -347,7 +347,7 @@ only when the divisor is zero or the final floor/ceil quotient does not fit in
 - Fit/rejection lemmas: `mulDiv512Down?_some`, `mulDiv512Down?_none_of_zero_divisor`, `mulDiv512Down?_none_of_overflow`, `mulDiv512Down?_isSome_iff`, `mulDiv512Down?_isNone_iff`, `mulDiv512Up?_some`, `mulDiv512Up?_none_of_zero_divisor`, `mulDiv512Up?_none_of_overflow`, `mulDiv512Up?_isSome_iff`, `mulDiv512Up?_isNone_iff` (`Verity/Proofs/Stdlib/Math.lean`)
 - Result-characterization lemmas: `mulDiv512Down?_eq_some_iff`, `mulDiv512Up?_eq_some_iff` (`Verity/Proofs/Stdlib/Math.lean`)
 - Sandwich lemmas: `mulDiv512Down?_mul_le`, `mulDiv512Down?_lt_succ_mul`, `mulDiv512Up?_mul_ge`, `mulDiv512Up?_mul_le_add_pred` (`Verity/Proofs/Stdlib/Math.lean`)
-- Rounding and shape lemmas: `mulDiv512Down?_comm`, `mulDiv512Up?_comm`, `mulDiv512Down?_monotone_left/right`, `mulDiv512Up?_monotone_left/right`, `mulDiv512Down?_antitone_divisor`, `mulDiv512Up?_antitone_divisor`, `mulDiv512Down?_isSome_of_up_isSome`, `mulDiv512Up?_isNone_of_down_isNone`, `mulDiv512Down?_le_up`, `mulDiv512Up?_le_down_add_one`, `mulDiv512Up?_eq_down_or_succ`, `mulDiv512Up?_eq_down_of_dvd`, `mulDiv512Up?_some_succ_of_not_dvd`, `mulDiv512Down?_zero_left/right`, `mulDiv512Up?_zero_left/right`, `mulDiv512Down?_cancel_right/left`, `mulDiv512Up?_cancel_right/left` (`Verity/Proofs/Stdlib/Math.lean`)
+- Rounding and shape lemmas: `mulDiv512Down?_comm`, `mulDiv512Up?_comm`, `mulDiv512Down?_monotone_left/right`, `mulDiv512Up?_monotone_left/right`, `mulDiv512Down?_antitone_divisor`, `mulDiv512Up?_antitone_divisor`, `mulDiv512Down?_isSome_of_up_isSome`, `mulDiv512Up?_isNone_of_down_isNone`, `mulDiv512Down?_le_up`, `mulDiv512Up?_le_down_add_one`, `mulDiv512Up?_eq_down_or_succ`, `mulDiv512Up?_eq_down_of_dvd`, `mulDiv512Up?_some_succ_of_not_dvd`, `mulDiv512Down?_pos`, `mulDiv512Up?_pos`, `mulDiv512Down?_zero_left/right`, `mulDiv512Up?_zero_left/right`, `mulDiv512Down?_cancel_right/left`, `mulDiv512Up?_cancel_right/left` (`Verity/Proofs/Stdlib/Math.lean`)
 - Automation mirrors: `mulDiv512Down?_some_iff`, `mulDiv512Down?_none_iff`, `mulDiv512Up?_some_iff`, `mulDiv512Up?_none_iff` (`Verity/Proofs/Stdlib/Automation.lean`)
 
 ## Same-Contract Helper Calls
diff --git a/docs/ARITHMETIC_PROFILE.md b/docs/ARITHMETIC_PROFILE.md
index 3b52a6da7..340a24966 100644
--- a/docs/ARITHMETIC_PROFILE.md
+++ b/docs/ARITHMETIC_PROFILE.md
@@ -94,7 +94,7 @@ direct sandwich lemmas: `mulDiv512Down?_mul_le`,
 `mulDiv512Down?_lt_succ_mul`, `mulDiv512Up?_mul_ge`, and
 `mulDiv512Up?_mul_le_add_pred`. They also mirror the existing `mulDiv`
 convenience surface with numerator commutativity, successful-result numerator
-monotonicity, divisor antitonicity, zero-numerator, and exact
+monotonicity, divisor antitonicity, positivity, zero-numerator, and exact
 same-denominator cancellation lemmas.
 Full-precision ceil/floor exactness is
 covered by `mulDiv512Up?_eq_down_of_dvd` and

From 0863e0327c324899b93361330909c833151696f4 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 05:54:55 +0200
Subject: [PATCH 15/18] Bridge mulDiv512 to existing mulDiv helpers

---
 PrintAxioms.lean                         |  4 ++-
 Verity/Proofs/Stdlib/Math.lean           | 33 ++++++++++++++++++++++++
 docs-site/content/edsl-api-reference.mdx |  1 +
 docs/ARITHMETIC_PROFILE.md               |  5 +++-
 4 files changed, 41 insertions(+), 2 deletions(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index 2d8edb086..8a03257d8 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -631,6 +631,8 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_mul_lt_add
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_antitone_divisor
 #print axioms Verity.Proofs.Stdlib.Math.mulDivUp_nat_eq
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_eq_mulDivDown_of_no_overflow
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_eq_mulDivUp_of_no_overflow
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_le_mulDivUp
 -- #print axioms Verity.Proofs.Stdlib.Math.nat_ceil_div_le_div_add_one  -- private
 -- #print axioms Verity.Proofs.Stdlib.Math.nat_ceil_div_eq_div_of_dvd  -- private
@@ -3850,4 +3852,4 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Compiler/Proofs/YulGeneration/ReferenceOracle/Semantics.lean
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_sender
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
--- Total: 3674 theorems/lemmas (2724 public, 950 private, 0 sorry'd)
+-- Total: 3676 theorems/lemmas (2726 public, 950 private, 0 sorry'd)
diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index eb119d658..154d89700 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -753,6 +753,39 @@ theorem mulDivUp_nat_eq (a b c : Uint256)
             simp [hNumerator]
     _ = (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) := Nat.mod_eq_of_lt hDivLt
 
+/-- `mulDiv512Down?` agrees with the existing `mulDivDown` helper when the
+intermediate product fits in `uint256`. -/
+theorem mulDiv512Down?_eq_mulDivDown_of_no_overflow (a b c : Uint256)
+    (hC : (c : Nat) ≠ 0)
+    (hMul : (a : Nat) * (b : Nat) ≤ MAX_UINT256) :
+    mulDiv512Down? a b c = some (mulDivDown a b c) := by
+  have hQuotFit : ((a : Nat) * (b : Nat)) / (c : Nat) ≤ MAX_UINT256 :=
+    Nat.le_trans (Nat.div_le_self _ _) hMul
+  rw [mulDiv512Down?_some (a := a) (b := b) (c := c) hC hQuotFit]
+  congr
+  apply Verity.Core.Uint256.ext
+  rw [mulDivDown_nat_eq a b c hMul]
+  simp [hC, Nat.mod_eq_of_lt (lt_modulus_of_le_max hQuotFit)]
+
+/-- `mulDiv512Up?` agrees with the existing `mulDivUp` helper when the
+rounded numerator expression fits in `uint256`. -/
+theorem mulDiv512Up?_eq_mulDivUp_of_no_overflow (a b c : Uint256)
+    (hC : c ≠ 0)
+    (hNum : (a : Nat) * (b : Nat) + ((c : Nat) - 1) ≤ MAX_UINT256) :
+    mulDiv512Up? a b c = some (mulDivUp a b c) := by
+  have hCVal : (c : Nat) ≠ 0 := by
+    intro h
+    apply hC
+    exact Verity.Core.Uint256.ext (by simpa using h)
+  have hQuotFit :
+      (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) ≤ MAX_UINT256 :=
+    Nat.le_trans (Nat.div_le_self _ _) hNum
+  rw [mulDiv512Up?_some (a := a) (b := b) (c := c) hCVal hQuotFit]
+  congr
+  apply Verity.Core.Uint256.ext
+  rw [mulDivUp_nat_eq a b c hC hNum]
+  simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hQuotFit)]
+
 /-- The ceil helper never rounds below the floor helper when both are exact. -/
 theorem mulDivDown_le_mulDivUp (a b c : Uint256)
     (hC : c ≠ 0)
diff --git a/docs-site/content/edsl-api-reference.mdx b/docs-site/content/edsl-api-reference.mdx
index d86d13dcd..71197d6ba 100644
--- a/docs-site/content/edsl-api-reference.mdx
+++ b/docs-site/content/edsl-api-reference.mdx
@@ -347,6 +347,7 @@ only when the divisor is zero or the final floor/ceil quotient does not fit in
 - Fit/rejection lemmas: `mulDiv512Down?_some`, `mulDiv512Down?_none_of_zero_divisor`, `mulDiv512Down?_none_of_overflow`, `mulDiv512Down?_isSome_iff`, `mulDiv512Down?_isNone_iff`, `mulDiv512Up?_some`, `mulDiv512Up?_none_of_zero_divisor`, `mulDiv512Up?_none_of_overflow`, `mulDiv512Up?_isSome_iff`, `mulDiv512Up?_isNone_iff` (`Verity/Proofs/Stdlib/Math.lean`)
 - Result-characterization lemmas: `mulDiv512Down?_eq_some_iff`, `mulDiv512Up?_eq_some_iff` (`Verity/Proofs/Stdlib/Math.lean`)
 - Sandwich lemmas: `mulDiv512Down?_mul_le`, `mulDiv512Down?_lt_succ_mul`, `mulDiv512Up?_mul_ge`, `mulDiv512Up?_mul_le_add_pred` (`Verity/Proofs/Stdlib/Math.lean`)
+- Compatibility lemmas: `mulDiv512Down?_eq_mulDivDown_of_no_overflow`, `mulDiv512Up?_eq_mulDivUp_of_no_overflow` (`Verity/Proofs/Stdlib/Math.lean`)
 - Rounding and shape lemmas: `mulDiv512Down?_comm`, `mulDiv512Up?_comm`, `mulDiv512Down?_monotone_left/right`, `mulDiv512Up?_monotone_left/right`, `mulDiv512Down?_antitone_divisor`, `mulDiv512Up?_antitone_divisor`, `mulDiv512Down?_isSome_of_up_isSome`, `mulDiv512Up?_isNone_of_down_isNone`, `mulDiv512Down?_le_up`, `mulDiv512Up?_le_down_add_one`, `mulDiv512Up?_eq_down_or_succ`, `mulDiv512Up?_eq_down_of_dvd`, `mulDiv512Up?_some_succ_of_not_dvd`, `mulDiv512Down?_pos`, `mulDiv512Up?_pos`, `mulDiv512Down?_zero_left/right`, `mulDiv512Up?_zero_left/right`, `mulDiv512Down?_cancel_right/left`, `mulDiv512Up?_cancel_right/left` (`Verity/Proofs/Stdlib/Math.lean`)
 - Automation mirrors: `mulDiv512Down?_some_iff`, `mulDiv512Down?_none_iff`, `mulDiv512Up?_some_iff`, `mulDiv512Up?_none_iff` (`Verity/Proofs/Stdlib/Automation.lean`)
 
diff --git a/docs/ARITHMETIC_PROFILE.md b/docs/ARITHMETIC_PROFILE.md
index 340a24966..9ffeb0158 100644
--- a/docs/ARITHMETIC_PROFILE.md
+++ b/docs/ARITHMETIC_PROFILE.md
@@ -95,7 +95,10 @@ direct sandwich lemmas: `mulDiv512Down?_mul_le`,
 `mulDiv512Up?_mul_le_add_pred`. They also mirror the existing `mulDiv`
 convenience surface with numerator commutativity, successful-result numerator
 monotonicity, divisor antitonicity, positivity, zero-numerator, and exact
-same-denominator cancellation lemmas.
+same-denominator cancellation lemmas. Compatibility bridge lemmas
+`mulDiv512Down?_eq_mulDivDown_of_no_overflow` and
+`mulDiv512Up?_eq_mulDivUp_of_no_overflow` connect the full-precision helpers to
+the existing 256-bit helpers under the older no-overflow preconditions.
 Full-precision ceil/floor exactness is
 covered by `mulDiv512Up?_eq_down_of_dvd` and
 `mulDiv512Up?_some_succ_of_not_dvd`, matching the older 256-bit `mulDiv`

From 46ac561437389903f9195ee5ebb24f7ec9d5ee05 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 06:04:27 +0200
Subject: [PATCH 16/18] Add mulDiv512 final overflow regressions

---
 PrintAxioms.lean               |  4 ++-
 Verity/Proofs/Stdlib/Math.lean | 47 ++++++++++++++++++++++++++++++++++
 2 files changed, 50 insertions(+), 1 deletion(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index 8a03257d8..c535ee607 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -598,6 +598,7 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_monotone_right
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_antitone_divisor
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_wide_product_regression
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_final_overflow_regression
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_some
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_none_of_zero_divisor
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_none_of_overflow
@@ -618,6 +619,7 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_monotone_right
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_antitone_divisor
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_wide_product_regression
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_final_overflow_regression
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_nat_eq
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_mul_le
 #print axioms Verity.Proofs.Stdlib.Math.mulDivDown_pos
@@ -3852,4 +3854,4 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Compiler/Proofs/YulGeneration/ReferenceOracle/Semantics.lean
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_sender
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
--- Total: 3676 theorems/lemmas (2726 public, 950 private, 0 sorry'd)
+-- Total: 3678 theorems/lemmas (2728 public, 950 private, 0 sorry'd)
diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index 154d89700..5c68306b2 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -269,6 +269,30 @@ theorem mulDiv512Down?_wide_product_regression :
     simp
   simp [Verity.Stdlib.Math.mulDiv512Down?, hMaxMod, hTwoMod, hQuot]
 
+/-- Regression: full-precision floor `mulDiv512` rejects when the 512-bit
+product is valid but the final quotient does not fit in `uint256`. -/
+theorem mulDiv512Down?_final_overflow_regression :
+    mulDiv512Down?
+        (Verity.Core.Uint256.ofNat MAX_UINT256)
+        (Verity.Core.Uint256.ofNat 2)
+        (Verity.Core.Uint256.ofNat 1) =
+      none := by
+  have hMaxMod :
+      MAX_UINT256 % Verity.Core.Uint256.modulus = MAX_UINT256 :=
+    Nat.mod_eq_of_lt max_uint256_lt_modulus
+  have hTwoMod : (2 : Nat) % Verity.Core.Uint256.modulus = 2 :=
+    Nat.mod_eq_of_lt (by
+      dsimp [Verity.Core.Uint256.modulus, Verity.Core.UINT256_MODULUS]
+      decide)
+  have hQuot : MAX_UINT256 * 2 / 1 = MAX_UINT256 * 2 := by
+    simp
+  have hOverflow : MAX_UINT256 < MAX_UINT256 * 2 := by
+    have hMaxPos : 0 < MAX_UINT256 := by
+      dsimp [MAX_UINT256, Verity.Core.MAX_UINT256]
+      decide
+    simpa [Nat.mul_two] using Nat.lt_add_of_pos_right (n := MAX_UINT256) hMaxPos
+  simp [Verity.Stdlib.Math.mulDiv512Down?, hMaxMod, hTwoMod, hQuot, hOverflow]
+
 /-- `mulDiv512Up?` returns the exact full-precision ceil quotient when it fits. -/
 theorem mulDiv512Up?_some (a b c : Uint256)
     (hC : (c : Nat) ≠ 0)
@@ -526,6 +550,28 @@ theorem mulDiv512Up?_wide_product_regression :
         rfl
   simp [Verity.Stdlib.Math.mulDiv512Up?, hMaxMod, hTwoMod, hQuot]
 
+/-- Regression: full-precision ceil `mulDiv512` rejects when the rounded
+512-bit quotient does not fit in `uint256`. -/
+theorem mulDiv512Up?_final_overflow_regression :
+    mulDiv512Up?
+        (Verity.Core.Uint256.ofNat MAX_UINT256)
+        (Verity.Core.Uint256.ofNat 2)
+        (Verity.Core.Uint256.ofNat 1) =
+      none := by
+  have hMaxMod :
+      MAX_UINT256 % Verity.Core.Uint256.modulus = MAX_UINT256 :=
+    Nat.mod_eq_of_lt max_uint256_lt_modulus
+  have hTwoMod : (2 : Nat) % Verity.Core.Uint256.modulus = 2 :=
+    Nat.mod_eq_of_lt (by
+      dsimp [Verity.Core.Uint256.modulus, Verity.Core.UINT256_MODULUS]
+      decide)
+  have hOverflow : MAX_UINT256 < MAX_UINT256 * 2 := by
+    have hMaxPos : 0 < MAX_UINT256 := by
+      dsimp [MAX_UINT256, Verity.Core.MAX_UINT256]
+      decide
+    simpa [Nat.mul_two] using Nat.lt_add_of_pos_right (n := MAX_UINT256) hMaxPos
+  simp [Verity.Stdlib.Math.mulDiv512Up?, hMaxMod, hTwoMod, hOverflow]
+
 /-! ## mulDiv / wad helpers -/
 
 /-- `mulDivDown` agrees with exact natural-number division when the numerator does not wrap. -/
@@ -1603,6 +1649,7 @@ Full-precision mulDiv512 helpers:
 - `mulDiv512Down?_zero_left/right` / `mulDiv512Up?_zero_left/right` — zero numerators collapse helpers
 - `mulDiv512Down?_cancel_right/left` / `mulDiv512Up?_cancel_right/left` — exact same-denominator cancellation
 - `mulDiv512Down?_wide_product_regression` / `mulDiv512Up?_wide_product_regression` — products may exceed 256 bits when quotients fit
+- `mulDiv512Down?_final_overflow_regression` / `mulDiv512Up?_final_overflow_regression` — final quotients above `MAX_UINT256` are rejected
 - `mulDiv512Up?_eq_down_of_dvd` / `mulDiv512Up?_some_succ_of_not_dvd` — ceil/floor divisibility shape
 - `mulDiv512Down?_le_up` / `mulDiv512Up?_le_down_add_one` / `mulDiv512Up?_eq_down_or_succ` — ceil/floor one-step rounding boundary
 

From b8fa0ec1f15c9eb971a422cf75257c1ed36270d4 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 06:06:55 +0200
Subject: [PATCH 17/18] Align mulDiv512 bridge divisor hypothesis

---
 Verity/Proofs/Stdlib/Math.lean | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index 5c68306b2..9b3a58b9f 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -816,20 +816,19 @@ theorem mulDiv512Down?_eq_mulDivDown_of_no_overflow (a b c : Uint256)
 /-- `mulDiv512Up?` agrees with the existing `mulDivUp` helper when the
 rounded numerator expression fits in `uint256`. -/
 theorem mulDiv512Up?_eq_mulDivUp_of_no_overflow (a b c : Uint256)
-    (hC : c ≠ 0)
+    (hC : (c : Nat) ≠ 0)
     (hNum : (a : Nat) * (b : Nat) + ((c : Nat) - 1) ≤ MAX_UINT256) :
     mulDiv512Up? a b c = some (mulDivUp a b c) := by
-  have hCVal : (c : Nat) ≠ 0 := by
+  have hCUint : c ≠ 0 := by
     intro h
-    apply hC
-    exact Verity.Core.Uint256.ext (by simpa using h)
+    exact hC (by simpa using congrArg (fun x : Uint256 => (x : Nat)) h)
   have hQuotFit :
       (((a : Nat) * (b : Nat)) + ((c : Nat) - 1)) / (c : Nat) ≤ MAX_UINT256 :=
     Nat.le_trans (Nat.div_le_self _ _) hNum
-  rw [mulDiv512Up?_some (a := a) (b := b) (c := c) hCVal hQuotFit]
+  rw [mulDiv512Up?_some (a := a) (b := b) (c := c) hC hQuotFit]
   congr
   apply Verity.Core.Uint256.ext
-  rw [mulDivUp_nat_eq a b c hC hNum]
+  rw [mulDivUp_nat_eq a b c hCUint hNum]
   simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hQuotFit)]
 
 /-- The ceil helper never rounds below the floor helper when both are exact. -/

From e35aeba4153573e983fe2c460427247e4b369ef5 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Sat, 2 May 2026 06:12:18 +0200
Subject: [PATCH 18/18] Add mulDiv512 one-divisor bounds

---
 PrintAxioms.lean                         |  4 +++-
 Verity/Proofs/Stdlib/Math.lean           | 18 ++++++++++++++++++
 docs-site/content/edsl-api-reference.mdx |  2 +-
 docs/ARITHMETIC_PROFILE.md               |  9 +++++----
 4 files changed, 27 insertions(+), 6 deletions(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index c535ee607..5781c7059 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -587,6 +587,7 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_isSome_iff
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_mul_le
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_lt_succ_mul
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_mul_lt_add
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_isNone_iff
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_comm
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_zero_left
@@ -606,6 +607,7 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_isSome_iff
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_mul_ge
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_mul_le_add_pred
+#print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_mul_lt_add
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_isNone_iff
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Down?_isSome_of_up_isSome
 #print axioms Verity.Proofs.Stdlib.Math.mulDiv512Up?_isNone_of_down_isNone
@@ -3854,4 +3856,4 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Compiler/Proofs/YulGeneration/ReferenceOracle/Semantics.lean
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_sender
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
--- Total: 3678 theorems/lemmas (2728 public, 950 private, 0 sorry'd)
+-- Total: 3680 theorems/lemmas (2730 public, 950 private, 0 sorry'd)
diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index 9b3a58b9f..2add4cfb0 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -146,6 +146,13 @@ theorem mulDiv512Down?_lt_succ_mul (a b c out : Uint256)
   simpa [Nat.mul_comm] using
     Nat.lt_mul_div_succ ((b : Nat) * (a : Nat)) (Nat.pos_of_ne_zero hC)
 
+/-- A successful full-precision floor result undershoots the exact product by
+less than one divisor-width. -/
+theorem mulDiv512Down?_mul_lt_add (a b c out : Uint256)
+    (h : mulDiv512Down? a b c = some out) :
+    (a : Nat) * (b : Nat) < (out : Nat) * (c : Nat) + (c : Nat) := by
+  simpa [Nat.right_distrib] using mulDiv512Down?_lt_succ_mul a b c out h
+
 /-- `mulDiv512Down?` rejects exactly zero divisors or overflowing floor quotients. -/
 theorem mulDiv512Down?_isNone_iff (a b c : Uint256) :
     (mulDiv512Down? a b c).isNone ↔
@@ -372,6 +379,16 @@ theorem mulDiv512Up?_mul_le_add_pred (a b c out : Uint256)
   simp [Nat.mod_eq_of_lt (lt_modulus_of_le_max hFit)]
   exact ceil_mul_div_le_add_pred ((a : Nat) * (b : Nat)) (c : Nat)
 
+/-- A successful full-precision ceil result overshoots the exact product by
+less than one divisor-width. -/
+theorem mulDiv512Up?_mul_lt_add (a b c out : Uint256)
+    (h : mulDiv512Up? a b c = some out) :
+    (out : Nat) * (c : Nat) < (a : Nat) * (b : Nat) + (c : Nat) := by
+  rcases (mulDiv512Up?_eq_some_iff a b c out).mp h with ⟨hC, _hFit, _hOut⟩
+  exact Nat.lt_of_le_of_lt
+    (mulDiv512Up?_mul_le_add_pred a b c out h)
+    (Nat.add_lt_add_left (Nat.sub_lt (Nat.pos_of_ne_zero hC) (by decide)) _)
+
 /-- `mulDiv512Up?` rejects exactly zero divisors or overflowing rounded-up quotients. -/
 theorem mulDiv512Up?_isNone_iff (a b c : Uint256) :
     (mulDiv512Up? a b c).isNone ↔
@@ -1639,6 +1656,7 @@ Full-precision mulDiv512 helpers:
 - `mulDiv512Down?_isSome_iff` / `mulDiv512Up?_isSome_iff` — characterize fit conditions
 - `mulDiv512Down?_isNone_iff` / `mulDiv512Up?_isNone_iff` — characterize rejection conditions
 - `mulDiv512Down?_mul_le` / `mulDiv512Down?_lt_succ_mul` — floor sandwich bounds
+- `mulDiv512Down?_mul_lt_add` / `mulDiv512Up?_mul_lt_add` — one-divisor error bounds
 - `mulDiv512Up?_mul_ge` / `mulDiv512Up?_mul_le_add_pred` — ceil sandwich bounds
 - `mulDiv512Down?_comm` / `mulDiv512Up?_comm` — numerator multiplication order does not matter
 - `mulDiv512Down?_monotone_left/right` / `mulDiv512Up?_monotone_left/right` — numerator monotonicity
diff --git a/docs-site/content/edsl-api-reference.mdx b/docs-site/content/edsl-api-reference.mdx
index 71197d6ba..2d7b66ceb 100644
--- a/docs-site/content/edsl-api-reference.mdx
+++ b/docs-site/content/edsl-api-reference.mdx
@@ -346,7 +346,7 @@ only when the divisor is zero or the final floor/ceil quotient does not fit in
 
 - Fit/rejection lemmas: `mulDiv512Down?_some`, `mulDiv512Down?_none_of_zero_divisor`, `mulDiv512Down?_none_of_overflow`, `mulDiv512Down?_isSome_iff`, `mulDiv512Down?_isNone_iff`, `mulDiv512Up?_some`, `mulDiv512Up?_none_of_zero_divisor`, `mulDiv512Up?_none_of_overflow`, `mulDiv512Up?_isSome_iff`, `mulDiv512Up?_isNone_iff` (`Verity/Proofs/Stdlib/Math.lean`)
 - Result-characterization lemmas: `mulDiv512Down?_eq_some_iff`, `mulDiv512Up?_eq_some_iff` (`Verity/Proofs/Stdlib/Math.lean`)
-- Sandwich lemmas: `mulDiv512Down?_mul_le`, `mulDiv512Down?_lt_succ_mul`, `mulDiv512Up?_mul_ge`, `mulDiv512Up?_mul_le_add_pred` (`Verity/Proofs/Stdlib/Math.lean`)
+- Sandwich lemmas: `mulDiv512Down?_mul_le`, `mulDiv512Down?_lt_succ_mul`, `mulDiv512Down?_mul_lt_add`, `mulDiv512Up?_mul_ge`, `mulDiv512Up?_mul_le_add_pred`, `mulDiv512Up?_mul_lt_add` (`Verity/Proofs/Stdlib/Math.lean`)
 - Compatibility lemmas: `mulDiv512Down?_eq_mulDivDown_of_no_overflow`, `mulDiv512Up?_eq_mulDivUp_of_no_overflow` (`Verity/Proofs/Stdlib/Math.lean`)
 - Rounding and shape lemmas: `mulDiv512Down?_comm`, `mulDiv512Up?_comm`, `mulDiv512Down?_monotone_left/right`, `mulDiv512Up?_monotone_left/right`, `mulDiv512Down?_antitone_divisor`, `mulDiv512Up?_antitone_divisor`, `mulDiv512Down?_isSome_of_up_isSome`, `mulDiv512Up?_isNone_of_down_isNone`, `mulDiv512Down?_le_up`, `mulDiv512Up?_le_down_add_one`, `mulDiv512Up?_eq_down_or_succ`, `mulDiv512Up?_eq_down_of_dvd`, `mulDiv512Up?_some_succ_of_not_dvd`, `mulDiv512Down?_pos`, `mulDiv512Up?_pos`, `mulDiv512Down?_zero_left/right`, `mulDiv512Up?_zero_left/right`, `mulDiv512Down?_cancel_right/left`, `mulDiv512Up?_cancel_right/left` (`Verity/Proofs/Stdlib/Math.lean`)
 - Automation mirrors: `mulDiv512Down?_some_iff`, `mulDiv512Down?_none_iff`, `mulDiv512Up?_some_iff`, `mulDiv512Up?_none_iff` (`Verity/Proofs/Stdlib/Automation.lean`)
diff --git a/docs/ARITHMETIC_PROFILE.md b/docs/ARITHMETIC_PROFILE.md
index 9ffeb0158..bd2b4f911 100644
--- a/docs/ARITHMETIC_PROFILE.md
+++ b/docs/ARITHMETIC_PROFILE.md
@@ -92,10 +92,11 @@ and the final quotient fits; the matching `_none_of_zero_divisor`,
 expose the failure boundary. Successful full-precision results also have
 direct sandwich lemmas: `mulDiv512Down?_mul_le`,
 `mulDiv512Down?_lt_succ_mul`, `mulDiv512Up?_mul_ge`, and
-`mulDiv512Up?_mul_le_add_pred`. They also mirror the existing `mulDiv`
-convenience surface with numerator commutativity, successful-result numerator
-monotonicity, divisor antitonicity, positivity, zero-numerator, and exact
-same-denominator cancellation lemmas. Compatibility bridge lemmas
+`mulDiv512Up?_mul_le_add_pred`, plus one-divisor error-bound lemmas
+`mulDiv512Down?_mul_lt_add` and `mulDiv512Up?_mul_lt_add`. They also mirror the
+existing `mulDiv` convenience surface with numerator commutativity,
+successful-result numerator monotonicity, divisor antitonicity, positivity,
+zero-numerator, and exact same-denominator cancellation lemmas. Compatibility bridge lemmas
 `mulDiv512Down?_eq_mulDivDown_of_no_overflow` and
 `mulDiv512Up?_eq_mulDivUp_of_no_overflow` connect the full-precision helpers to
 the existing 256-bit helpers under the older no-overflow preconditions.