diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index c74894d57..345f3d798 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
@@ -572,6 +576,52 @@ 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.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
+#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?_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
+#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
+#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
+#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?_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
+#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
+#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
@@ -585,10 +635,17 @@ 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
 -- #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
@@ -3839,4 +3896,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 (2717 public, 946 private, 0 sorry'd)
+-- Total: 3720 theorems/lemmas (2770 public, 950 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/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index 494282a46..2add4cfb0 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -26,6 +26,571 @@ 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 -/
+
+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
+
+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)
+    (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]
+
+/-- `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]
+
+/-- 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)
+
+/-- 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 ↔
+      (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]
+
+/-- 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
+
+/-- 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) :
+    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
+
+/-- 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)
+
+/-- 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))
+    (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₂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 :
+    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]
+
+/-- 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)
+    (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]
+
+/-- `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]
+
+/-- 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)
+
+/-- 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 ↔
+      (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]
+
+/-- 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
+  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
+
+/-- 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) :
+    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
+
+/-- 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) _)
+
+/-- 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 :
+    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]
+
+/-- 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. -/
 theorem mulDivDown_nat_eq (a b c : Uint256) (hMul : (a : Nat) * (b : Nat) ≤ MAX_UINT256) :
     (mulDivDown a b c : Nat) =
@@ -251,6 +816,38 @@ 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 : Nat) ≠ 0)
+    (hNum : (a : Nat) * (b : Nat) + ((c : Nat) - 1) ≤ MAX_UINT256) :
+    mulDiv512Up? a b c = some (mulDivUp a b c) := by
+  have hCUint : c ≠ 0 := by
+    intro 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) hC hQuotFit]
+  congr
+  apply Verity.Core.Uint256.ext
+  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. -/
 theorem mulDivDown_le_mulDivUp (a b c : Uint256)
     (hC : c ≠ 0)
@@ -306,6 +903,76 @@ 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
+
+/-- 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)
@@ -981,6 +1648,28 @@ 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
+- `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
+- `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
+- `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
+
 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/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-site/content/edsl-api-reference.mdx b/docs-site/content/edsl-api-reference.mdx
index bac0b4265..2d7b66ceb 100644
--- a/docs-site/content/edsl-api-reference.mdx
+++ b/docs-site/content/edsl-api-reference.mdx
@@ -326,6 +326,31 @@ 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`, `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`)
+
 ## 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.
diff --git a/docs/ARITHMETIC_PROFILE.md b/docs/ARITHMETIC_PROFILE.md
index 189eb1347..bd2b4f911 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,46 @@ 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`, `_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`, 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.
+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. 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`,
+`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` |
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 2a590b866..6e9002423 100644
--- a/docs/ROADMAP.md
+++ b/docs/ROADMAP.md
@@ -89,6 +89,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`):