From 75b40ddaf5d2a0b007b5ca755d3033a70a059815 Mon Sep 17 00:00:00 2001
From: Josh Liebow-Feeser <hello@joshlf.com>
Date: Thu, 1 Oct 2026 22:49:50 -0400
Subject: [PATCH] Prove least padding and greatest aligned predecessors

Strengthen the initial arithmetic specs from bounds to exact behavior.
For power-of-two alignments, prove the least padding that reaches an
aligned length and the greatest aligned value no larger than the input.
Strengthen extrema with their input-selection and ordering properties.

Preserve broader raw arithmetic lemmas and derive mathematical-model
contracts and caller corollaries from them. Add total Rust assertion
harnesses comparing the bitwise implementation with independent division
and remainder calculations. Their visible alignment guard leaves every
machine length, including usize::MAX, in the supported domain.

gherrit-pr-id: Gcqu6kiltuj5regk4e2yhgquvd5vqi7ho
Agent-authored-by: AI agent acting on joshlf's behalf
---
 verification/aeneas/README.md                 |   2 +
 verification/aeneas/golden/Funs.lean          |  94 +++++++----
 .../aeneas/golden/FunsExternal_Template.lean  |   6 +-
 verification/aeneas/lean/Arithmetic.lean      | 139 ++++++++++++++++
 verification/aeneas/lean/Corollaries.lean     |  85 ++++++++++
 verification/aeneas/lean/Obligations.lean     |  44 +++--
 .../aeneas/lean/Proofs/ArithmeticChecks.lean  |  54 ++++++
 verification/aeneas/lean/Proofs/Util.lean     | 154 +++++++++++-------
 .../lean/RequiredModelContracts/Util.lean     |  64 ++++++--
 verification/aeneas/projections/Specs.lean    |  30 +++-
 .../aeneas/projections/TraitLaws.lean         |   1 +
 zerocopy/src/util/checks.rs                   |  61 +++++++
 zerocopy/src/util/mod.rs                      |  22 ++-
 13 files changed, 625 insertions(+), 131 deletions(-)
 create mode 100644 verification/aeneas/lean/Arithmetic.lean
 create mode 100644 verification/aeneas/lean/Corollaries.lean
 create mode 100644 verification/aeneas/lean/Proofs/ArithmeticChecks.lean
 create mode 100644 zerocopy/src/util/checks.rs

diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md
index 59c094fcce..f9880d62f0 100644
--- a/verification/aeneas/README.md
+++ b/verification/aeneas/README.md
@@ -262,6 +262,8 @@ whole-program unsafe-code certification.
 
 ## Scope and proofs
 
+Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs).
+
 Extraction starts from the function and nominal-type owners of every present
 `aeneas` fence in `zerocopy/src`, including their dependencies. The current
 function specifications cover the layout and arithmetic methods and their Rust
diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean
index c6237d79f3..c706647675 100644
--- a/verification/aeneas/golden/Funs.lean
+++ b/verification/aeneas/golden/Funs.lean
@@ -857,6 +857,63 @@ def util.bytewrite.be_word_prefix
   let s ← lift (Array.to_slice a)
   util.bytewrite.prefix s dst
 
+/-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
+    Source: 'src/util/mod.rs', lines 267:0-285:1 -/
+def util.round_down_to_next_multiple_of_alignment
+  (n : Std.Usize)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) :
+  Result Std.Usize
+  := do
+  let align1 ←
+    core.num.nonzero.NonZero.get
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
+  let b ← core.num.Usize.is_power_of_two align1
+  massert b
+  let i ← align1 - 1#usize
+  let mask ← lift (~~~ i)
+  ok (n &&& mask)
+
+/-- [zerocopy::util::padding_needed_for]:
+    Source: 'src/util/mod.rs', lines 175:0-235:1 -/
+def util.padding_needed_for
+  (len : Std.Usize)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) :
+  Result Std.Usize
+  := do
+  let i ←
+    core.num.nonzero.NonZero.get
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
+  let mask ← i - 1#usize
+  let i1 ← lift (core.num.Usize.wrapping_sub len 1#usize)
+  let i2 ← lift (~~~ i1)
+  ok (i2 &&& mask)
+
+/-- [zerocopy::util::checks::check_arithmetic]:
+    Source: 'src/util/checks.rs', lines 38:0-46:1 -/
+def util.checks.check_arithmetic
+  (len : Std.Usize)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) :
+  Result Unit
+  := do
+  let i ←
+    core.num.nonzero.NonZero.get
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
+  let b ← core.num.Usize.is_power_of_two i
+  if b
+  then
+    let remainder ← len % i
+    let i1 ← i - remainder
+    let padding ← i1 % i
+    let i2 ← util.padding_needed_for len align
+    massert (i2 = padding)
+    let i3 ← util.round_down_to_next_multiple_of_alignment len align
+    let i4 ← len - remainder
+    massert (i3 = i4)
+  else ok ()
+
 /-- [zerocopy::impls::_::{impl zerocopy::FromZeros for ()}::only_derive_is_allowed_to_implement_this_trait]:
     Source: 'src/util/macros.rs', lines 165:8-165:62
     Visibility: public -/
@@ -2072,41 +2129,8 @@ def core.cell.UnsafeCell.Insts.ZerocopyIntoBytes {T : Type} (IntoBytesInst :
     IntoBytesInst
 }
 
-/-- [zerocopy::util::padding_needed_for]:
-    Source: 'src/util/mod.rs', lines 168:0-228:1 -/
-def util.padding_needed_for
-  (len : Std.Usize)
-  (align : core.num.nonzero.NonZero Std.Usize
-  core.num.niche_types.NonZeroUsizeInner) :
-  Result Std.Usize
-  := do
-  let i ←
-    core.num.nonzero.NonZero.get
-      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
-  let mask ← i - 1#usize
-  let i1 ← lift (core.num.Usize.wrapping_sub len 1#usize)
-  let i2 ← lift (~~~ i1)
-  ok (i2 &&& mask)
-
-/-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
-    Source: 'src/util/mod.rs', lines 255:0-273:1 -/
-def util.round_down_to_next_multiple_of_alignment
-  (n : Std.Usize)
-  (align : core.num.nonzero.NonZero Std.Usize
-  core.num.niche_types.NonZeroUsizeInner) :
-  Result Std.Usize
-  := do
-  let align1 ←
-    core.num.nonzero.NonZero.get
-      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
-  let b ← core.num.Usize.is_power_of_two align1
-  massert b
-  let i ← align1 - 1#usize
-  let mask ← lift (~~~ i)
-  ok (n &&& mask)
-
 /-- [zerocopy::util::max]:
-    Source: 'src/util/mod.rs', lines 282:0-288:1 -/
+    Source: 'src/util/mod.rs', lines 295:0-301:1 -/
 def util.max
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -2126,7 +2150,7 @@ def util.max
   else ok a
 
 /-- [zerocopy::util::min]:
-    Source: 'src/util/mod.rs', lines 297:0-303:1 -/
+    Source: 'src/util/mod.rs', lines 311:0-317:1 -/
 def util.min
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean
index 5b4246f474..278da9ebb6 100644
--- a/verification/aeneas/golden/FunsExternal_Template.lean
+++ b/verification/aeneas/golden/FunsExternal_Template.lean
@@ -75,12 +75,12 @@ axiom core.num.nonzero.NonZero.get
   core.num.nonzero.NonZero T Clause0_NonZeroInner → Result T
 
 /-- [zerocopy::util::copy_unchecked]:
-    Source: 'src/util/mod.rs', lines 315:0-330:1 -/
+    Source: 'src/util/mod.rs', lines 329:0-344:1 -/
 axiom util.copy_unchecked
   : Slice Std.U8 → Slice Std.U8 → Result (Slice Std.U8)
 
 /-- [zerocopy::util::copy_unchecked_at]:
-    Source: 'src/util/mod.rs', lines 344:0-355:1 -/
+    Source: 'src/util/mod.rs', lines 358:0-369:1 -/
 axiom util.copy_unchecked_at
   : Slice Std.U8 → Slice Std.U8 → Std.Usize → Result (Slice Std.U8)
 
@@ -141,7 +141,7 @@ axiom Array.Insts.ZerocopyTryFromBytes.is_safe
     Bool
 
 /-- [zerocopy::util::transmute_unchecked]:
-    Source: 'src/util/mod.rs', lines 367:0-396:1 -/
+    Source: 'src/util/mod.rs', lines 381:0-410:1 -/
 axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst
 
 /-- [zerocopy::util::validity::read_byte]:
diff --git a/verification/aeneas/lean/Arithmetic.lean b/verification/aeneas/lean/Arithmetic.lean
new file mode 100644
index 0000000000..3282d94d0e
--- /dev/null
+++ b/verification/aeneas/lean/Arithmetic.lean
@@ -0,0 +1,139 @@
+/- Copyright 2026 The Fuchsia Authors
+
+Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+<LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+This file may not be copied, modified, or distributed except according to
+those terms. -/
+
+module
+public import Aeneas
+public import Rust.Arithmetic
+import all Init.Data.Nat.Power2.Basic
+@[expose] public section
+
+/-!
+Rust implements alignment operations with bounded words and bit masks. The
+contracts describe those results with unbounded natural numbers. This module
+proves the arithmetic facts needed to connect the two descriptions: why
+clearing low bits rounds down, why the padding mask yields the least aligned
+increment, and why wrapping at zero does not invalidate that increment. It
+contains no claims about the control flow of a zerocopy function; Proofs.Util
+applies these facts while stepping through the extracted implementations.
+-/
+open Aeneas Aeneas.Std
+namespace Zerocopy.Arithmetic
+
+/-- Scalar minimum agrees with mathematical minimum. -/
+theorem coe_min (a b : Usize) :
+    ((min a b : Usize) : Nat) = Nat.min (a : Nat) (b : Nat) := by
+  by_cases h : a ≤ b
+  · rw [min_eq_left h]
+    exact (Nat.min_eq_left ((UScalar.le_equiv _ _).mp h)).symm
+  · have hba : b ≤ a := le_of_not_ge h
+    rw [min_eq_right hba]
+    exact (Nat.min_eq_right ((UScalar.le_equiv _ _).mp hba)).symm
+
+/-- The unique bounded padding that makes the sum divisible by alignment. -/
+theorem padding_unique (len align p : Nat) (hpos : 0 < align)
+    (hlt : p < align) (haligned : (len + p) % align = 0) :
+    p = (align - len % align) % align :=
+  Rust.Arithmetic.padding_unique len align p hpos hlt haligned
+
+/-- Exact padding also gives minimality and the zero-padding criterion. -/
+theorem padding_properties (len align p : Nat) (hpos : 0 < align)
+    (hlt : p < align) (haligned : (len + p) % align = 0) :
+    p = (align - len % align) % align ∧
+    (∀ q : Nat, (len + q) % align = 0 → p ≤ q) ∧
+    (p = 0 ↔ len % align = 0) :=
+  Rust.Arithmetic.padding_properties len align p hpos hlt haligned
+
+/-- Clearing and retaining a bit mask partition the original word exactly. -/
+theorem mask_partition (n mask : Usize) :
+    (n &&& ~~~mask).val + (n &&& mask).val = n.val := by
+  have hdisjoint : (n.bv &&& ~~~mask.bv) &&& (n.bv &&& mask.bv) = 0 := by
+    ext i
+    simp only [BitVec.getElem_and, BitVec.getElem_not]
+    cases n.bv[i] <;> cases mask.bv[i] <;> simp
+  have hjoin : (n.bv &&& ~~~mask.bv) ||| (n.bv &&& mask.bv) = n.bv := by
+    ext i
+    simp only [BitVec.getElem_or, BitVec.getElem_and, BitVec.getElem_not]
+    cases n.bv[i] <;> cases mask.bv[i] <;> decide
+  have hsum := BitVec.add_eq_or_of_and_eq_zero _ _ hdisjoint
+  rw [hjoin] at hsum
+  have := congrArg BitVec.toNat hsum
+  rw [BitVec.toNat_add_of_and_eq_zero hdisjoint] at this
+  exact this
+
+/-- A power-of-two alignment divides the word modulus. -/
+theorem alignment_dvd_size (align : Usize) (h : align.val.isPowerOfTwo) :
+    align.val ∣ UScalar.size .Usize := by
+  obtain ⟨k, hk⟩ := h
+  have hsize := UScalar.hSize align
+  rw [UScalar.size, hk] at hsize ⊢
+  exact Nat.pow_dvd_pow 2 ((Nat.pow_le_pow_iff_right (a := 2) (by decide)).mp (by omega))
+
+/-- Complementing the wrapping predecessor produces modular negation. -/
+theorem complement_predecessor (len : Usize) :
+    (~~~(core.num.Usize.wrapping_sub len 1#usize)).val =
+      if len.val = 0 then 0 else UScalar.size .Usize - len.val := by
+  change (~~~(len.bv - (1#usize).bv)).toNat = _
+  rw [BitVec.toNat_not]
+  have hsize := UScalar.hSize len
+  have hone : (1#usize).val = 1 := by simp
+  by_cases hz : len.val = 0
+  · simp only [hz, if_true]
+    rw [BitVec.toNat_sub, UScalar.bv_toNat, UScalar.bv_toNat]
+    change 2 ^ System.Platform.numBits - 1 -
+      ((2 ^ System.Platform.numBits - (1#usize).val) + len.val) % 2 ^ System.Platform.numBits = 0
+    rw [hz, hone, Nat.add_zero, Nat.mod_eq_of_lt (by have := Nat.two_pow_pos System.Platform.numBits; omega)]
+    omega
+  · simp only [hz, if_false]
+    rw [BitVec.toNat_sub_of_le (by simpa only [BitVec.le_def, UScalar.bv_toNat, hone] using (show 1 ≤ len.val by omega)), UScalar.bv_toNat, UScalar.bv_toNat, hone]
+    change 2 ^ System.Platform.numBits - 1 - (len.val - 1) = UScalar.size .Usize - len.val
+    rw [UScalar.size] at hsize ⊢
+    change len.val < 2 ^ System.Platform.numBits at hsize
+    change 2 ^ System.Platform.numBits - 1 - (len.val - 1) =
+      2 ^ System.Platform.numBits - len.val
+    omega
+
+/-- The padding bit mask aligns the unbounded sum, including wrapping at zero. -/
+theorem padding_mask_aligned (len align mask : Usize)
+    (h : align.val.isPowerOfTwo) (hm : mask.val = align.val - 1) :
+    (len.val + (~~~(core.num.Usize.wrapping_sub len 1#usize) &&& mask).val)
+      % align.val = 0 := by
+  have hmod := Nat.mod_eq_zero_of_dvd (alignment_dvd_size align h)
+  have hsum : (len.val + (~~~(core.num.Usize.wrapping_sub len 1#usize)).val)
+      % align.val = 0 := by
+    rw [complement_predecessor]
+    split
+    · rename_i hz
+      simp only [hz, Nat.zero_add, Nat.zero_mod]
+    · have hsize := UScalar.hSize len
+      rw [Nat.add_sub_of_le (by omega)]
+      exact hmod
+  obtain ⟨k, hk⟩ := h
+  rw [UScalar.val_and, hm, hk, Nat.and_two_pow_sub_one_eq_mod]
+  rw [hk, Nat.add_mod] at hsum
+  rw [Nat.add_mod, Nat.mod_mod]
+  exact hsum
+
+/-- The exact arithmetic result of clearing the low alignment bits. -/
+theorem round_down_exact (n align mask : Usize)
+    (h : align.val.isPowerOfTwo) (hm : mask.val = align.val - 1) :
+    (n &&& ~~~mask).val = n.val - n.val % align.val := by
+  have hp := mask_partition n mask
+  have hlow : (n &&& mask).val = n.val % align.val := by
+    obtain ⟨k, hk⟩ := h
+    rw [UScalar.val_and, hm, hk, Nat.and_two_pow_sub_one_eq_mod]
+  rw [hlow] at hp
+  omega
+
+/-- An exact round-down result is aligned and the greatest such lower bound. -/
+theorem round_down_properties (n align m : Nat) (hpos : 0 < align)
+    (hm : m = n - n % align) :
+    m ≤ n ∧ m % align = 0 ∧ n < m + align ∧
+    (∀ q : Nat, q ≤ n → q % align = 0 → q ≤ m) :=
+  Rust.Arithmetic.round_down_properties n align m hpos hm
+
+end Zerocopy.Arithmetic
diff --git a/verification/aeneas/lean/Corollaries.lean b/verification/aeneas/lean/Corollaries.lean
new file mode 100644
index 0000000000..edab313551
--- /dev/null
+++ b/verification/aeneas/lean/Corollaries.lean
@@ -0,0 +1,85 @@
+/- Copyright 2026 The Fuchsia Authors
+
+Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+<LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+This file may not be copied, modified, or distributed except according to
+those terms. -/
+
+module
+public import Proofs
+public import Aeneas
+import all Init.Data.Nat.Power2.Basic
+@[expose] public section
+
+/-!
+A function contract is most useful when other proofs can consume it. These
+corollaries compose the checked arithmetic operation lemmas into further
+numeric consequences. They reuse the proved computation and discharge its
+stated requirements, rather than proving a different calculation in its
+place.
+
+The results remain conditional functional guarantees. They do not establish
+pointer safety or prove that every Rust caller meets the contract's
+requirements.
+-/
+open Aeneas Aeneas.Std Aeneas.Std.Result
+namespace Zerocopy.Corollaries
+open Proofs Proofs.Raw
+
+
+theorem max_preserves (a b : NonZeroUsize) (P : NonZeroUsize → Prop)
+    (ha : P a)
+    (hb : P b) :
+    util.max a b
+      ⦃ r => P r ⦄ := by
+  step with Proofs.Raw.max_spec a b as ⟨r, _, hchoice, _, _⟩
+  rcases hchoice with h | h
+  · simpa only [h] using ha
+  · simpa only [h] using hb
+
+theorem min_preserves (a b : NonZeroUsize) (P : NonZeroUsize → Prop)
+    (ha : P a)
+    (hb : P b) :
+    util.min a b
+      ⦃ r => P r ⦄ := by
+  step with Proofs.Raw.min_spec a b as ⟨r, _, hchoice, _, _⟩
+  rcases hchoice with h | h
+  · simpa only [h] using ha
+  · simpa only [h] using hb
+
+theorem round_down_aligned (n : Usize) (align : NonZeroUsize)
+    (hpow : (align.val : Nat).isPowerOfTwo)
+    (haligned : (n : Nat) % (align.val : Nat) = 0) :
+    util.round_down_to_next_multiple_of_alignment n align = .ok n := by
+  obtain ⟨m, hm, _, hexact, _, _, _⟩ :=
+    WP.spec_imp_exists (Proofs.Raw.round_down_spec n align hpow)
+  have heq : m = n := UScalar.eq_of_val_eq (by
+    simpa only [haligned, Nat.sub_zero] using hexact)
+  simpa only [heq] using hm
+
+theorem round_down_idempotent (n : Usize) (align : NonZeroUsize)
+    (hpow : (align.val : Nat).isPowerOfTwo) :
+    (do
+      let m ← util.round_down_to_next_multiple_of_alignment n align
+      let m' ← util.round_down_to_next_multiple_of_alignment m align
+      ok (m, m'))
+      ⦃ m m' => m' = m ⦄ := by
+  step with Proofs.Raw.round_down_spec n align hpow as ⟨m, _, _, haligned, _, _⟩
+  rw [round_down_aligned m align hpow haligned]
+  simp only [bind_ok, WP.spec_ok, WP.uncurry'_pair]
+
+theorem round_down_monotone (a b : Usize) (align : NonZeroUsize)
+    (hab : a ≤ b)
+    (hpow : (align.val : Nat).isPowerOfTwo) :
+    (do
+      let m ← util.round_down_to_next_multiple_of_alignment a align
+      let m' ← util.round_down_to_next_multiple_of_alignment b align
+      ok (m, m'))
+      ⦃ m m' => m ≤ m' ⦄ := by
+  step with Proofs.Raw.round_down_spec a align hpow as ⟨m, hbound, _, haligned, _, _⟩
+  step with Proofs.Raw.round_down_spec b align hpow as ⟨m', _, _, _, _, hgreatest⟩
+  apply (UScalar.le_equiv _ _).mpr
+  exact hgreatest m.val ((UScalar.le_equiv _ _).mp (le_trans hbound hab)) haligned
+
+end Zerocopy.Corollaries
diff --git a/verification/aeneas/lean/Obligations.lean b/verification/aeneas/lean/Obligations.lean
index c95854b591..e4d32f4ce8 100644
--- a/verification/aeneas/lean/Obligations.lean
+++ b/verification/aeneas/lean/Obligations.lean
@@ -10,6 +10,7 @@ module
 public import Zerocopy.Funs
 public import SpecPrelude
 public import MathViews
+public import Arithmetic
 @[expose] public section
 
 /-!
@@ -33,9 +34,9 @@ abbrev NonZeroUsize :=
 
 def max_spec_contract (a b : NonZeroUsize)
     (run : Result NonZeroUsize) : Prop :=
-  0 < a.val.val → 0 < b.val.val →
-    ∃ r, run = .ok r ∧ 0 < r.val.val ∧
-      r.val.val = Nat.max a.val.val b.val.val
+  0 < a.val.val → 0 < b.val.val → ∃ r, run = .ok r ∧ 0 < r.val.val ∧
+    r.val.val = Nat.max a.val.val b.val.val ∧ (r = a ∨ r = b) ∧
+      a.val.val ≤ r.val.val ∧ b.val.val ≤ r.val.val
 
 def max_spec : Prop :=
   ∀ (a b : NonZeroUsize),
@@ -43,18 +44,22 @@ def max_spec : Prop :=
 
 def min_spec_contract (a b : NonZeroUsize)
     (run : Result NonZeroUsize) : Prop :=
-  0 < a.val.val → 0 < b.val.val →
-    ∃ r, run = .ok r ∧ 0 < r.val.val ∧
-      r.val.val = Nat.min a.val.val b.val.val
+  0 < a.val.val → 0 < b.val.val → ∃ r, run = .ok r ∧ 0 < r.val.val ∧
+    r.val.val = Nat.min a.val.val b.val.val ∧ (r = a ∨ r = b) ∧
+      r.val.val ≤ a.val.val ∧ r.val.val ≤ b.val.val
 
 def min_spec : Prop :=
   ∀ (a b : NonZeroUsize),
     min_spec_contract a b (util.min a b)
 
-def padding_lt_alignment_contract (_len : Usize) (align : NonZeroUsize)
+def padding_lt_alignment_contract (len : Usize) (align : NonZeroUsize)
     (run : Result Usize) : Prop :=
-  ∀ (_valid : 0 < align.val.val),
-    run ⦃ p => p.val < align.val.val ⦄
+  ∀ (_valid : 0 < align.val.val) (_h : align.val.val.isPowerOfTwo),
+    run ⦃ p => p.val < align.val.val ∧
+      p.val = (align.val.val - len.val % align.val.val) % align.val.val ∧
+      (len.val + p.val) % align.val.val = 0 ∧
+      (∀ q : Nat, (len.val + q) % align.val.val = 0 → p.val ≤ q) ∧
+      (p.val = 0 ↔ len.val % align.val.val = 0) ⦄
 
 def padding_lt_alignment : Prop :=
   ∀ (len : Usize) (align : NonZeroUsize),
@@ -63,8 +68,10 @@ def padding_lt_alignment : Prop :=
 def round_down_spec_contract (n : Usize) (align : NonZeroUsize)
     (run : Result Usize) : Prop :=
   ∀ (_valid : 0 < align.val.val) (_h : align.val.val.isPowerOfTwo),
-    run
-      ⦃ m => m.val ≤ n.val ∧ m.val % align.val.val = 0 ⦄
+    run ⦃ m =>
+      m.val ≤ n.val ∧ m.val = n.val - n.val % align.val.val ∧
+      m.val % align.val.val = 0 ∧ n.val < m.val + align.val.val ∧
+      (∀ q : Nat, q ≤ n.val → q % align.val.val = 0 → q ≤ m.val) ⦄
 
 def round_down_spec : Prop :=
   ∀ (n : Usize) (align : NonZeroUsize),
@@ -72,3 +79,18 @@ def round_down_spec : Prop :=
 
 
 end Zerocopy.Obligations
+
+namespace Zerocopy.Obligations
+
+-- The source harness promises successful execution, including its assertions.
+-- The positive premise records the Rust NonZeroUsize input domain independently
+-- of the generated specification's decoding expansion.
+def arithmetic_checks_spec_contract (_len : Usize) (align : NonZeroUsize)
+    (run : Result Unit) : Prop :=
+  0 < align.val.val → run ⦃ _ => True ⦄
+
+def arithmetic_checks_spec : Prop :=
+  ∀ (len : Usize) (align : NonZeroUsize),
+    arithmetic_checks_spec_contract len align (util.checks.check_arithmetic len align)
+
+end Zerocopy.Obligations
diff --git a/verification/aeneas/lean/Proofs/ArithmeticChecks.lean b/verification/aeneas/lean/Proofs/ArithmeticChecks.lean
new file mode 100644
index 0000000000..596f49d20e
--- /dev/null
+++ b/verification/aeneas/lean/Proofs/ArithmeticChecks.lean
@@ -0,0 +1,54 @@
+/- Copyright 2026 The Fuchsia Authors
+
+Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+<LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+This file may not be copied, modified, or distributed except according to
+those terms. -/
+
+module
+public import Proofs.Util
+@[expose] public section
+
+/-!
+The Rust assertions are the application promise. These lemmas connect the
+extracted remainder calculations to the already proved bitwise helpers. The
+canonical theorem establishes successful execution of the entire harness,
+including both assertions, for every accepted input.
+-/
+open Aeneas Aeneas.Std
+namespace Zerocopy.Proofs.Raw
+
+theorem arithmetic_checks (len : Usize) (align : NonZeroUsize) :
+    util.checks.check_arithmetic len align ⦃ _ => True ⦄ := by
+  unfold util.checks.check_arithmetic
+  simp only [core.num.nonzero.NonZero.get, bind_ok]
+  step as ⟨pow2, hp⟩
+  split
+  · rename_i enabled
+    have power : align.val.val.isPowerOfTwo := by
+      exact Eq.mp hp enabled
+    have positive := Nat.pos_of_isPowerOfTwo power
+    step as ⟨remainder, hr⟩
+    step as ⟨gap, hg⟩
+    step as ⟨padding, hpadding⟩
+    step with padding_lt_alignment len align power as ⟨actual, _, exactPadding, _⟩
+    step
+    step with round_down_spec len align power as ⟨rounded, _, exactRounded, _⟩
+    step as ⟨expected, hexpected⟩
+    · rw [hr]
+      exact Nat.mod_le _ _
+    · step
+  · simp only [WP.spec_ok]
+
+end Zerocopy.Proofs.Raw
+
+namespace Zerocopy.Proofs
+
+theorem arithmetic_checks_spec : Specs.arithmetic_checks_spec := by
+  intro len align _ _ _ _
+  apply WP.spec_mono (Raw.arithmetic_checks len align)
+  intro result _
+  exact ⟨(), rfl, trivial⟩
+
+end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/Proofs/Util.lean b/verification/aeneas/lean/Proofs/Util.lean
index 61cb530625..b4556233db 100644
--- a/verification/aeneas/lean/Proofs/Util.lean
+++ b/verification/aeneas/lean/Proofs/Util.lean
@@ -20,101 +20,117 @@ specs, including successful input and result decoding.
 The notation computation ⦃ result => property ⦄ means that execution
 terminates successfully and its returned value satisfies property. Aeneas's
 step tactic uses a registered callee specification, generating its
-preconditions as proof goals. These proofs connect numeric facts to the
-specific zerocopy implementations.
+preconditions as proof goals. Pure scalar facts belong in Arithmetic; these
+proofs connect those facts to the specific zerocopy implementations.
 -/
 open Aeneas Aeneas.Std
 namespace Zerocopy.Proofs.Raw
 
+-- Raw contract requirements intentionally retain their descriptive proof names.
 set_option linter.unusedVariables false
 
 theorem padding_lt_alignment :
-  ∀ (len : Usize) (align : NonZeroUsize), ∀ (h : (0 < align.val.val : Prop)),
-    @Zerocopy.util.padding_needed_for len align ⦃ p => p.val < align.val.val ⦄ := by
+  ∀ (len : Usize) (align : NonZeroUsize), ∀ (h : ((align.val : Nat).isPowerOfTwo : Prop)),
+    @Zerocopy.util.padding_needed_for len align ⦃ p => p < align.val ∧
+    let L : Nat := len
+    let A : Nat := align.val
+    let P : Nat := p
+    P = (A - L % A) % A ∧ (L + P) % A = 0 ∧
+      (∀ q : Nat, (L + q) % A = 0 → P ≤ q) ∧ (P = 0 ↔ L % A = 0) ⦄ := by
   intro len align h
+  have hpos := Nat.pos_of_isPowerOfTwo h
   unfold util.padding_needed_for
   simp only [core.num.nonzero.NonZero.get, bind_ok]
   step
-  simp only [lift, bind_ok, WP.spec_ok, UScalar.val_and]
-  have hbound :
-      (~~~(core.num.Usize.wrapping_sub len 1#usize)).val &&& mask.val ≤ mask.val :=
-    Nat.and_le_right
-  omega
+  simp only [lift, bind_ok, WP.spec_ok]
+  have hbound : (~~~(core.num.Usize.wrapping_sub len 1#usize) &&& mask).val
+      < align.val.val := by
+    have := Nat.and_le_right (n := (~~~(core.num.Usize.wrapping_sub len 1#usize)).val)
+      (m := mask.val)
+    rw [UScalar.val_and]
+    omega
+  have haligned := Arithmetic.padding_mask_aligned len align.val mask h (by omega)
+  obtain ⟨hexact, hminimal, hzero⟩ :=
+    Arithmetic.padding_properties _ _ _ hpos hbound haligned
+  exact ⟨(UScalar.lt_equiv _ _).mpr hbound, hexact, haligned, hminimal, hzero⟩
 
 theorem round_down_spec :
-  ∀ (n : Usize) (align : NonZeroUsize), ∀ (hpos : (0 < align.val.val : Prop)), ∀ (h : (align.val.val.isPowerOfTwo : Prop)),
-    @Zerocopy.util.round_down_to_next_multiple_of_alignment n align ⦃ m => m.val ≤ n.val ∧ m.val % align.val.val = 0 ⦄ := by
-  intro n align hpos h
+  ∀ (n : Usize) (align : NonZeroUsize), ∀ (h : ((align.val : Nat).isPowerOfTwo : Prop)),
+    @Zerocopy.util.round_down_to_next_multiple_of_alignment n align ⦃ m => m ≤ n ∧
+    let N : Nat := n
+    let A : Nat := align.val
+    let M : Nat := m
+    M = N - N % A ∧ M % A = 0 ∧ N < M + A ∧
+      (∀ q : Nat, q ≤ N → q % A = 0 → q ≤ M) ⦄ := by
+  intro n align h
+  have hpos := Nat.pos_of_isPowerOfTwo h
   unfold util.round_down_to_next_multiple_of_alignment
   simp only [core.num.nonzero.NonZero.get, bind_ok]
   step
   step
   step with UScalar.sub_bv_spec as ⟨mask, hval, hle, hbv⟩
   simp only [lift, bind_ok, WP.spec_ok]
-  constructor
-  · simp only [UScalar.val_and]
-    exact Nat.and_le_left
-  · have clear : (n &&& ~~~mask).val &&& mask.val = 0 := by
-      rw [← UScalar.val_and]
-      change ((n.bv &&& ~~~mask.bv) &&& mask.bv).toNat = 0
-      simp [BitVec.and_assoc]
-    unfold Nat.isPowerOfTwo at h
-    rcases h with ⟨k, hk⟩
-    rw [hval, hk, Nat.and_two_pow_sub_one_eq_mod] at clear
-    simpa only [hk] using clear
+  have hexact := Arithmetic.round_down_exact n align.val mask h hval
+  obtain ⟨hbound, haligned, hnext, hgreatest⟩ :=
+    Arithmetic.round_down_properties _ _ _ hpos hexact
+  exact ⟨(UScalar.le_equiv _ _).mpr hbound, hexact, haligned, hnext, hgreatest⟩
 
 theorem max_spec :
   ∀ (a b : NonZeroUsize),
-    @Zerocopy.util.max a b ⦃ r => r.val.val = Nat.max a.val.val b.val.val ⦄ := by
+    @Zerocopy.util.max a b ⦃ r => r.val = max a.val b.val ∧ (r = a ∨ r = b) ∧
+    a.val ≤ r.val ∧ b.val ≤ r.val ⦄ := by
   intro a b
-  apply WP.exists_imp_spec
-  simp only [util.max, core.num.nonzero.NonZero.get, bind_ok, UScalar.lt_equiv]
+  simp only [util.max, core.num.nonzero.NonZero.get, bind_ok]
   split
   · rename_i h
-    exact ⟨b, rfl, (Nat.max_eq_right (by omega)).symm⟩
+    exact WP.spec.ret ⟨(max_eq_right (le_of_lt h)).symm, Or.inr rfl,
+      le_of_lt h, le_rfl⟩
   · rename_i h
-    exact ⟨a, rfl, (Nat.max_eq_left (by omega)).symm⟩
+    exact WP.spec.ret ⟨(max_eq_left (le_of_not_gt h)).symm, Or.inl rfl,
+      le_rfl, le_of_not_gt h⟩
 
 theorem min_spec :
   ∀ (a b : NonZeroUsize),
-    @Zerocopy.util.min a b ⦃ r => r.val.val = Nat.min a.val.val b.val.val ⦄ := by
+    @Zerocopy.util.min a b ⦃ r => r.val = min a.val b.val ∧ (r = a ∨ r = b) ∧
+    r.val ≤ a.val ∧ r.val ≤ b.val ⦄ := by
   intro a b
-  apply WP.exists_imp_spec
-  simp only [util.min, core.num.nonzero.NonZero.get, bind_ok, UScalar.lt_equiv]
+  simp only [util.min, core.num.nonzero.NonZero.get, bind_ok]
   split
   · rename_i h
-    exact ⟨b, rfl, (Nat.min_eq_right (by omega)).symm⟩
+    exact WP.spec.ret ⟨(min_eq_right (le_of_lt h)).symm, Or.inr rfl,
+      le_of_lt h, le_rfl⟩
   · rename_i h
-    exact ⟨a, rfl, (Nat.min_eq_left (by omega)).symm⟩
+    exact WP.spec.ret ⟨(min_eq_left (le_of_not_gt h)).symm, Or.inl rfl,
+      le_rfl, le_of_not_gt h⟩
 
 end Zerocopy.Proofs.Raw
 
+
 namespace Zerocopy.Proofs
 open AeneasSpecs
 
 theorem padding_lt_alignment : Zerocopy.Specs.padding_lt_alignment := by
-  intro len align _lenValue _hlen alignValue halign
+  intro len align lenValue hlen alignValue halign h
+  have hl := (decodeUScalar_iff len lenValue).mp hlen
   have ha := (decodeNonZeroUScalar_iff align alignValue).mp halign
-  have positive : 0 < align.val.val := by rw [ha]; exact alignValue.positive
-  apply WP.spec_mono (Raw.padding_lt_alignment len align positive)
-  intro output facts
-  refine ⟨unsignedWord output, rfl, ?_⟩
+  apply WP.spec_mono (Raw.padding_lt_alignment len align (by simpa only [ha] using h))
+  intro p facts
+  refine ⟨unsignedWord p, rfl, ?_⟩
   dsimp only
-  rw [← ha]
-  exact facts
+  rw [← hl, ← ha]
+  exact ⟨(UScalar.lt_equiv _ _).mp facts.1, facts.2⟩
 register_spec_step padding_lt_alignment
 
 theorem round_down_spec : Zerocopy.Specs.round_down_spec := by
-  intro n align nValue hn alignValue halign pow2
+  intro n align nValue hn alignValue halign h
   have hnv := (decodeUScalar_iff n nValue).mp hn
   have ha := (decodeNonZeroUScalar_iff align alignValue).mp halign
-  have positive : 0 < align.val.val := by rw [ha]; exact alignValue.positive
-  apply WP.spec_mono (Raw.round_down_spec n align positive (by simpa only [ha] using pow2))
-  intro output facts
-  refine ⟨unsignedWord output, rfl, ?_⟩
+  apply WP.spec_mono (Raw.round_down_spec n align (by simpa only [ha] using h))
+  intro m facts
+  refine ⟨unsignedWord m, rfl, ?_⟩
   dsimp only
   rw [← hnv, ← ha]
-  exact facts
+  exact ⟨(UScalar.le_equiv _ _).mp facts.1, facts.2⟩
 register_spec_step round_down_spec
 
 theorem max_spec : Zerocopy.Specs.max_spec := by
@@ -122,13 +138,22 @@ theorem max_spec : Zerocopy.Specs.max_spec := by
   have hav := (decodeNonZeroUScalar_iff a av).mp ha
   have hbv := (decodeNonZeroUScalar_iff b bv).mp hb
   apply WP.spec_mono (Raw.max_spec a b)
-  intro output facts
-  have positive : 0 < output.val.val := by
-    rw [facts, hav, hbv]
-    exact lt_of_lt_of_le av.positive (Nat.le_max_left _ _)
-  let value : NonZeroUsizeValue := ⟨unsignedWord output.val, positive⟩
-  refine ⟨value, (decodeNonZeroUScalar_iff output value).mpr rfl, ?_⟩
-  simpa only [value, unsignedWord, hav, hbv] using facts
+  intro r facts
+  rcases facts.2.1 with hr | hr
+  · subst r
+    refine ⟨av, ha, ?_⟩
+    dsimp only
+    rw [← hav, ← hbv]
+    exact ⟨by simpa only [UScalar.coe_max] using congrArg UScalar.val facts.1,
+      Or.inl rfl, (UScalar.le_equiv _ _).mp facts.2.2.1,
+      (UScalar.le_equiv _ _).mp facts.2.2.2⟩
+  · subst r
+    refine ⟨bv, hb, ?_⟩
+    dsimp only
+    rw [← hav, ← hbv]
+    exact ⟨by simpa only [UScalar.coe_max] using congrArg UScalar.val facts.1,
+      Or.inr rfl, (UScalar.le_equiv _ _).mp facts.2.2.1,
+      (UScalar.le_equiv _ _).mp facts.2.2.2⟩
 register_spec_step max_spec
 
 theorem min_spec : Zerocopy.Specs.min_spec := by
@@ -136,13 +161,22 @@ theorem min_spec : Zerocopy.Specs.min_spec := by
   have hav := (decodeNonZeroUScalar_iff a av).mp ha
   have hbv := (decodeNonZeroUScalar_iff b bv).mp hb
   apply WP.spec_mono (Raw.min_spec a b)
-  intro output facts
-  have positive : 0 < output.val.val := by
-    rw [facts, hav, hbv]
-    exact lt_min av.positive bv.positive
-  let value : NonZeroUsizeValue := ⟨unsignedWord output.val, positive⟩
-  refine ⟨value, (decodeNonZeroUScalar_iff output value).mpr rfl, ?_⟩
-  simpa only [value, unsignedWord, hav, hbv] using facts
+  intro r facts
+  rcases facts.2.1 with hr | hr
+  · subst r
+    refine ⟨av, ha, ?_⟩
+    dsimp only
+    rw [← hav, ← hbv]
+    exact ⟨(Nat.min_eq_left ((UScalar.le_equiv _ _).mp facts.2.2.2)).symm,
+      Or.inl rfl, (UScalar.le_equiv _ _).mp facts.2.2.1,
+      (UScalar.le_equiv _ _).mp facts.2.2.2⟩
+  · subst r
+    refine ⟨bv, hb, ?_⟩
+    dsimp only
+    rw [← hav, ← hbv]
+    exact ⟨(Nat.min_eq_right ((UScalar.le_equiv _ _).mp facts.2.2.1)).symm,
+      Or.inr rfl, (UScalar.le_equiv _ _).mp facts.2.2.1,
+      (UScalar.le_equiv _ _).mp facts.2.2.2⟩
 register_spec_step min_spec
 
 end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/RequiredModelContracts/Util.lean b/verification/aeneas/lean/RequiredModelContracts/Util.lean
index 674014acc6..ee8f971efc 100644
--- a/verification/aeneas/lean/RequiredModelContracts/Util.lean
+++ b/verification/aeneas/lean/RequiredModelContracts/Util.lean
@@ -9,6 +9,7 @@ those terms. -/
 module
 public import Obligations
 public import Specs
+public import MathViews
 @[expose] public section
 
 /-!
@@ -23,17 +24,21 @@ strong enough.
 open Aeneas Aeneas.Std AeneasSpecs
 namespace Zerocopy.Proofs
 
--- These bridges consume the supplied weak-stage model contract and recover
--- the unchanged independent c85 propositions. No raw function proof is used.
+attribute [contract_simps] option_admitted_explicit_iff admitted_some admitted_none
+  admitted_dite
+
+-- These implications consume a supplied model contract and recover the
+-- separately authored representation observations. They do not prove or
+-- select a function contract themselves.
 @[contract_simps] theorem required_padding (len : Usize) (align : NonZeroUsize)
     (run : Result Usize) (provided : Specs.padding_lt_alignment_contract len align run) :
     Obligations.padding_lt_alignment_contract len align run := by
-  intro positive
+  intro positive pow2
   let av : NonZeroUsizeValue := ⟨unsignedWord align.val, positive⟩
   have admitted := (decodeNonZeroUScalar_iff align av).mpr rfl
-  apply WP.spec_mono (provided (unsignedWord len) rfl av admitted)
-  rintro output ⟨value, decoded, facts⟩
-  have same := (decodeUScalar_iff output value).mp decoded
+  apply WP.spec_mono (provided (unsignedWord len) rfl av admitted pow2)
+  rintro p ⟨value, decoded, facts⟩
+  have same := (decodeUScalar_iff p value).mp decoded
   simpa only [unsignedWord, av, ← same] using facts
 
 @[contract_simps] theorem required_round_down (n : Usize) (align : NonZeroUsize)
@@ -47,6 +52,12 @@ namespace Zerocopy.Proofs
   have same := (decodeUScalar_iff output value).mp decoded
   simpa only [unsignedWord, av, ← same] using facts
 
+theorem nonzero_raw_eq_of_value_eq (a b : NonZeroUsize)
+    (same : a.val.val = b.val.val) : a = b := by
+  have hs := UScalar.eq_of_val_eq same
+  cases a; cases b
+  congr
+
 @[contract_simps] theorem required_max (a b : NonZeroUsize) (run : Result NonZeroUsize)
     (provided : Specs.max_spec_contract a b run) :
     Obligations.max_spec_contract a b run := by
@@ -57,11 +68,16 @@ namespace Zerocopy.Proofs
   have db := (decodeNonZeroUScalar_iff b bv).mpr rfl
   have result := provided av da bv db
   simp only [WP.spec_equiv_exists] at result
-  obtain ⟨output, call, value, decoded, facts⟩ := result
-  have same := (decodeNonZeroUScalar_iff output value).mp decoded
-  refine ⟨output, call, ?_, ?_⟩
+  obtain ⟨r, call, value, decoded, facts⟩ := result
+  have same := (decodeNonZeroUScalar_iff r value).mp decoded
+  refine ⟨r, call, ?_, ?_, ?_, ?_, ?_⟩
   · rw [same]; exact value.positive
-  · simpa only [av, bv, unsignedWord, ← same] using facts
+  · simpa only [av, bv, unsignedWord, ← same] using facts.1
+  · rcases facts.2.1 with h | h
+    · left; apply nonzero_raw_eq_of_value_eq; simp only [same, h, av, unsignedWord]
+    · right; apply nonzero_raw_eq_of_value_eq; simp only [same, h, bv, unsignedWord]
+  · simpa only [av, unsignedWord, ← same] using facts.2.2.1
+  · simpa only [bv, unsignedWord, ← same] using facts.2.2.2
 
 @[contract_simps] theorem required_min (a b : NonZeroUsize) (run : Result NonZeroUsize)
     (provided : Specs.min_spec_contract a b run) :
@@ -73,9 +89,29 @@ namespace Zerocopy.Proofs
   have db := (decodeNonZeroUScalar_iff b bv).mpr rfl
   have result := provided av da bv db
   simp only [WP.spec_equiv_exists] at result
-  obtain ⟨output, call, value, decoded, facts⟩ := result
-  have same := (decodeNonZeroUScalar_iff output value).mp decoded
-  refine ⟨output, call, ?_, ?_⟩
+  obtain ⟨r, call, value, decoded, facts⟩ := result
+  have same := (decodeNonZeroUScalar_iff r value).mp decoded
+  refine ⟨r, call, ?_, ?_, ?_, ?_, ?_⟩
   · rw [same]; exact value.positive
-  · simpa only [av, bv, unsignedWord, ← same] using facts
+  · simpa only [av, bv, unsignedWord, ← same] using facts.1
+  · rcases facts.2.1 with h | h
+    · left; apply nonzero_raw_eq_of_value_eq; simp only [same, h, av, unsignedWord]
+    · right; apply nonzero_raw_eq_of_value_eq; simp only [same, h, bv, unsignedWord]
+  · simpa only [av, unsignedWord, ← same] using facts.2.2.1
+  · simpa only [bv, unsignedWord, ← same] using facts.2.2.2
+
+end Zerocopy.Proofs
+
+namespace Zerocopy.Proofs
+
+@[contract_simps] theorem required_arithmetic_checks (len : Usize) (align : NonZeroUsize)
+    (run : Result Unit) (provided : Specs.arithmetic_checks_spec_contract len align run) :
+    Obligations.arithmetic_checks_spec_contract len align run := by
+  intro positive
+  let av : NonZeroUsizeValue := ⟨unsignedWord align.val, positive⟩
+  have admitted := (decodeNonZeroUScalar_iff align av).mpr rfl
+  apply WP.spec_mono (provided (unsignedWord len) rfl av admitted)
+  intro _ _
+  trivial
+
 end Zerocopy.Proofs
diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean
index 3c31859ab8..828f957bfc 100644
--- a/verification/aeneas/projections/Specs.lean
+++ b/verification/aeneas/projections/Specs.lean
@@ -11,6 +11,7 @@ public import Zerocopy.Funs
 public import SpecPrelude
 public import SpecsSyntax
 public import Models
+public import Arithmetic
 public import TraitLaws
 @[expose] public section
 
@@ -200,11 +201,25 @@ spec write_be_word_prefix_spec
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.write_be_word_prefix_spec for Zerocopy.util.bytewrite.be_word_prefix with 2
 
+check_model_inputs Zerocopy.util.checks.check_arithmetic with 0 type parameters
+aeneas_spec_begin
+spec arithmetic_checks_spec
+  for @Zerocopy.util.checks.check_arithmetic with 0 type parameters
+  ensures _ => True
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.arithmetic_checks_spec for Zerocopy.util.checks.check_arithmetic with 2
+
 check_model_inputs Zerocopy.util.padding_needed_for with 0 type parameters
 aeneas_spec_begin
 spec padding_lt_alignment
   for @Zerocopy.util.padding_needed_for with 0 type parameters
-  ensures p => (p : Nat) < (align : Nat)
+  requires h : (align : Nat).isPowerOfTwo
+  ensures p => (p : Nat) < (align : Nat) ∧
+    let L : Nat := len
+    let A : Nat := align
+    let P : Nat := p
+    P = (A - L % A) % A ∧ (L + P) % A = 0 ∧
+      (∀ q : Nat, (L + q) % A = 0 → P ≤ q) ∧ (P = 0 ↔ L % A = 0)
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.padding_lt_alignment for Zerocopy.util.padding_needed_for with 2
 
@@ -213,7 +228,12 @@ aeneas_spec_begin
 spec round_down_spec
   for @Zerocopy.util.round_down_to_next_multiple_of_alignment with 0 type parameters
   requires h : (align : Nat).isPowerOfTwo
-  ensures m => (m : Nat) ≤ (n : Nat) ∧ (m : Nat) % (align : Nat) = 0
+  ensures m => (m : Nat) ≤ (n : Nat) ∧
+    let N : Nat := n
+    let A : Nat := align
+    let M : Nat := m
+    M = N - N % A ∧ M % A = 0 ∧ N < M + A ∧
+      (∀ q : Nat, q ≤ N → q % A = 0 → q ≤ M)
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.round_down_spec for Zerocopy.util.round_down_to_next_multiple_of_alignment with 2
 
@@ -221,7 +241,8 @@ check_model_inputs Zerocopy.util.max with 0 type parameters
 aeneas_spec_begin
 spec max_spec
   for @Zerocopy.util.max with 0 type parameters
-  ensures r => (r : Nat) = Nat.max (a : Nat) (b : Nat)
+  ensures r => (r : Nat) = max (a : Nat) (b : Nat) ∧ (r = a ∨ r = b) ∧
+    (a : Nat) ≤ (r : Nat) ∧ (b : Nat) ≤ (r : Nat)
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.max_spec for Zerocopy.util.max with 2
 
@@ -229,7 +250,8 @@ check_model_inputs Zerocopy.util.min with 0 type parameters
 aeneas_spec_begin
 spec min_spec
   for @Zerocopy.util.min with 0 type parameters
-  ensures r => (r : Nat) = Nat.min (a : Nat) (b : Nat)
+  ensures r => (r : Nat) = min (a : Nat) (b : Nat) ∧ (r = a ∨ r = b) ∧
+    (r : Nat) ≤ (a : Nat) ∧ (r : Nat) ≤ (b : Nat)
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.min_spec for Zerocopy.util.min with 2
 
diff --git a/verification/aeneas/projections/TraitLaws.lean b/verification/aeneas/projections/TraitLaws.lean
index c47a29cc66..1abd631a86 100644
--- a/verification/aeneas/projections/TraitLaws.lean
+++ b/verification/aeneas/projections/TraitLaws.lean
@@ -9,6 +9,7 @@ those terms. -/
 module
 public import Zerocopy.Funs
 public import TraitLawsSupport
+public import Arithmetic
 @[expose] public section
 open Aeneas Aeneas.Std
 namespace Zerocopy.TraitLaws
diff --git a/zerocopy/src/util/checks.rs b/zerocopy/src/util/checks.rs
new file mode 100644
index 0000000000..38147e3db4
--- /dev/null
+++ b/zerocopy/src/util/checks.rs
@@ -0,0 +1,61 @@
+// SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+//
+// Copyright 2026 The Fuchsia Authors
+//
+// Licensed under the 2-Clause BSD License <LICENSE-BSD or
+// https://opensource.org/license/bsd-2-clause>, Apache License, Version 2.0
+// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+// This file may not be copied, modified, or distributed except according to
+// those terms.
+
+//! Rust assertions describe the arithmetic promises checked by Aeneas.
+//!
+//! A total specification with postcondition `True` still requires successful
+//! termination: every assertion must pass. The independent calculations below
+//! use division and remainder, rather than the production bitwise algorithms.
+//! The module is part of the ordinary library so extraction sees exactly the
+//! source reviewed here. Its private functions have no runtime callers outside
+//! tests; optimized builds can discard them.
+
+// Read the integer explicitly so extraction uses the ordinary scalar remainder
+// operation. The proof checks that these guarded arithmetic operations are safe.
+#![allow(dead_code, clippy::needless_nonzero_get)]
+
+use core::num::NonZeroUsize;
+
+/// Checks padding and rounding down for every length and supported alignment.
+///
+/// The explicit guard describes the domain: these helpers require a
+/// power-of-two alignment. There is no bound on `len` beyond its Rust type.
+/// Neither comparison adds padding to `len`, so `usize::MAX` remains covered.
+///
+/// ```aeneas
+/// spec arithmetic_checks_spec
+///   ensures _ => True
+/// ```
+#[allow(clippy::arithmetic_side_effects)]
+fn check_arithmetic(len: usize, align: NonZeroUsize) {
+    if !align.get().is_power_of_two() {
+        return;
+    }
+    let remainder = len % align.get();
+    let padding = (align.get() - remainder) % align.get();
+    assert!(super::padding_needed_for(len, align) == padding);
+    assert!(super::round_down_to_next_multiple_of_alignment(len, align) == len - remainder);
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn arithmetic_boundaries() {
+        for align in [1, 2, 4, 8, 1 << (usize::BITS - 1), 3] {
+            let align = NonZeroUsize::new(align).unwrap();
+            for len in [0, 1, 7, 8, 9, usize::MAX - 1, usize::MAX] {
+                check_arithmetic(len, align);
+            }
+        }
+    }
+}
diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs
index 97d5315413..8e8775cae8 100644
--- a/zerocopy/src/util/mod.rs
+++ b/zerocopy/src/util/mod.rs
@@ -15,6 +15,7 @@ pub(crate) mod macros;
 pub mod macro_util;
 
 pub(crate) mod bytewrite;
+mod checks;
 #[cfg(target_endian = "little")]
 #[allow(dead_code)]
 mod owned_transmute;
@@ -163,7 +164,13 @@ pub(crate) fn validate_aligned_to<T: AsAddress, U>(t: T) -> Result<(), Alignment
 ///
 /// ```aeneas
 /// spec padding_lt_alignment
-///   ensures p => (p : Nat) < (align : Nat)
+///   requires h : (align : Nat).isPowerOfTwo
+///   ensures p => (p : Nat) < (align : Nat) ∧
+///     let L : Nat := len
+///     let A : Nat := align
+///     let P : Nat := p
+///     P = (A - L % A) % A ∧ (L + P) % A = 0 ∧
+///       (∀ q : Nat, (L + q) % A = 0 → P ≤ q) ∧ (P = 0 ↔ L % A = 0)
 /// ```
 pub(crate) const fn padding_needed_for(len: usize, align: NonZeroUsize) -> usize {
     #[cfg(kani)]
@@ -250,7 +257,12 @@ pub(crate) const fn padding_needed_for(len: usize, align: NonZeroUsize) -> usize
 /// ```aeneas
 /// spec round_down_spec
 ///   requires h : (align : Nat).isPowerOfTwo
-///   ensures m => (m : Nat) ≤ (n : Nat) ∧ (m : Nat) % (align : Nat) = 0
+///   ensures m => (m : Nat) ≤ (n : Nat) ∧
+///     let N : Nat := n
+///     let A : Nat := align
+///     let M : Nat := m
+///     M = N - N % A ∧ M % A = 0 ∧ N < M + A ∧
+///       (∀ q : Nat, q ≤ N → q % A = 0 → q ≤ M)
 /// ```
 pub(crate) const fn round_down_to_next_multiple_of_alignment(
     n: usize,
@@ -277,7 +289,8 @@ pub(crate) const fn round_down_to_next_multiple_of_alignment(
 ///
 /// ```aeneas
 /// spec max_spec
-///   ensures r => (r : Nat) = Nat.max (a : Nat) (b : Nat)
+///   ensures r => (r : Nat) = max (a : Nat) (b : Nat) ∧ (r = a ∨ r = b) ∧
+///     (a : Nat) ≤ (r : Nat) ∧ (b : Nat) ≤ (r : Nat)
 /// ```
 pub(crate) const fn max(a: NonZeroUsize, b: NonZeroUsize) -> NonZeroUsize {
     if a.get() < b.get() {
@@ -292,7 +305,8 @@ pub(crate) const fn max(a: NonZeroUsize, b: NonZeroUsize) -> NonZeroUsize {
 ///
 /// ```aeneas
 /// spec min_spec
-///   ensures r => (r : Nat) = Nat.min (a : Nat) (b : Nat)
+///   ensures r => (r : Nat) = min (a : Nat) (b : Nat) ∧ (r = a ∨ r = b) ∧
+///     (r : Nat) ≤ (a : Nat) ∧ (r : Nat) ≤ (b : Nat)
 /// ```
 pub(crate) const fn min(a: NonZeroUsize, b: NonZeroUsize) -> NonZeroUsize {
     if a.get() > b.get() {