From a33a68f2bb6520c009cfed3274533f50d9cddd31 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] Strengthen arithmetic specifications and prove arithmetic
 corollaries

Prove exact extrema, least padding and the greatest aligned predecessor.
Preserve broad Raw arithmetic results and derive recursive mathematical models
contracts; compose extrema and round-down corollaries. Layout padding is
introduced with its normalized implementation in the later padding proof layer.

Add total Rust assertion harnesses comparing padding and round-down with
independent division/remainder calculations, including usize boundary values.
Keep the comparisons and their power-of-two guard visible in Rust.

Validation: fresh pinned extraction and complete-model golden comparison;
independent golden/live Lean builds, required-contract checks, and the
transitive axiom audit.

gherrit-pr-id: Gxi6wprpgshggdrhvt64jphmjwhociog5
Agent-authored-by: AI agent acting on joshlf's behalf
---
 verification/aeneas/README.md                 |  16 +-
 verification/aeneas/golden/Funs.lean          |  52 +++--
 verification/aeneas/lean/Arithmetic.lean      | 178 ++++++++++++++++++
 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 +++++--
 zerocopy/src/util/checks.rs                   |  61 ++++++
 zerocopy/src/util/mod.rs                      |  23 ++-
 10 files changed, 621 insertions(+), 110 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 4ad4e27471..27ca5ef5d4 100644
--- a/verification/aeneas/README.md
+++ b/verification/aeneas/README.md
@@ -119,6 +119,8 @@ zerocopy's unsafe pointer operations are sound.
 
 ## 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. Every present
 fence must have a supported Rust owner, exact extraction binding, and the
@@ -128,10 +130,10 @@ added without extending the specification set.
 | Rust function | Checked property |
 | --- | --- |
 | Byteorder U16/U32 read, write, and set (both endiannesses) | Exact integer value, every encoded byte, and setter/getter equality for every typed input. |
-| `max` | Terminates successfully and returns the mathematical maximum. |
-| `min` | Terminates successfully and returns the mathematical minimum. |
-| `padding_needed_for` | For any positive alignment, succeeds with padding strictly below that alignment. |
-| `round_down_to_next_multiple_of_alignment` | For any positive power-of-two alignment, succeeds with a result no larger than the input and divisible by the alignment. |
+| `max` | Returns the mathematical maximum, selects an input, and bounds both inputs from above. |
+| `min` | Returns the mathematical minimum, selects an input, and bounds both inputs from below. |
+| `padding_needed_for` | For power-of-two alignment, returns padding below it and exactly `(align - len % align) % align`, the least padding making the sum aligned, with zero padding exactly when the input is aligned. |
+| `round_down_to_next_multiple_of_alignment` | For power-of-two alignment, returns exactly `n - n % align`, the greatest aligned value at most `n`; the next multiple exceeds `n`. |
 
 Every registered function uses total `spec`: accepted raw representations,
 supplied mathematical ghosts, and explicit requirements imply successful
@@ -139,9 +141,9 @@ termination, successful output decoding, and the postconditions. These are
 quantified conditional contracts, not finite test inputs. Broader ordinary Raw
 lemmas retain useful representation-level domains.
 
-This initial arithmetic scope establishes extrema, padding bounds and an
-aligned result no larger than the input. It does not claim least padding or
-the greatest aligned predecessor.
+`Corollaries.lean` composes the arithmetic proofs: extrema preserve a shared
+predicate, and round-down is monotone, aligned and idempotent under its stated
+conditions.
 
 Plain arithmetic clauses use mathematical word values carrying machine bounds
 and NonZero positivity. Their Nat/Int arithmetic does not wrap; explicit raw
diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean
index 5899738651..6bee28d103 100644
--- a/verification/aeneas/golden/Funs.lean
+++ b/verification/aeneas/golden/Funs.lean
@@ -642,8 +642,25 @@ def byteorder.verification.set_u32_be
       value n
   byteorder.U32.get byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder value1
 
+/-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
+    Source: 'src/util/mod.rs', lines 261:0-279: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 161:0-221:1 -/
+    Source: 'src/util/mod.rs', lines 169:0-229:1 -/
 def util.padding_needed_for
   (len : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -658,25 +675,32 @@ def util.padding_needed_for
   let i2 ← lift (~~~ i1)
   ok (i2 &&& mask)
 
-/-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
-    Source: 'src/util/mod.rs', lines 248:0-266:1 -/
-def util.round_down_to_next_multiple_of_alignment
-  (n : Std.Usize)
+/-- [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 Std.Usize
+  Result Unit
   := do
-  let align1 ←
+  let i ←
     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)
+  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::util::max]:
-    Source: 'src/util/mod.rs', lines 275:0-281:1 -/
+    Source: 'src/util/mod.rs', lines 289:0-295:1 -/
 def util.max
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -696,7 +720,7 @@ def util.max
   else ok a
 
 /-- [zerocopy::util::min]:
-    Source: 'src/util/mod.rs', lines 290:0-296:1 -/
+    Source: 'src/util/mod.rs', lines 305:0-311:1 -/
 def util.min
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
diff --git a/verification/aeneas/lean/Arithmetic.lean b/verification/aeneas/lean/Arithmetic.lean
new file mode 100644
index 0000000000..3abb9ac72f
--- /dev/null
+++ b/verification/aeneas/lean/Arithmetic.lean
@@ -0,0 +1,178 @@
+/- 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
+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 := by
+  have hr := Nat.mod_lt len hpos
+  have hsum : (len % align + p) % align = 0 := by
+    rw [Nat.add_mod, Nat.mod_eq_of_lt hlt] at haligned
+    exact haligned
+  by_cases hzero : len % align = 0
+  · simpa only [hzero, Nat.zero_add, Nat.mod_eq_of_lt hlt,
+      Nat.sub_zero, Nat.mod_self] using hsum
+  · have hge : align ≤ len % align + p := by
+      by_contra h
+      rw [Nat.mod_eq_of_lt (by omega)] at hsum
+      omega
+    rw [Nat.mod_eq_sub_mod hge, Nat.mod_eq_of_lt (by omega)] at hsum
+    rw [Nat.mod_eq_of_lt (by omega)]
+    omega
+
+/-- 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) := by
+  refine ⟨padding_unique len align p hpos hlt haligned, ?_, ?_⟩
+  · intro q hq
+    have hqm : (len + q % align) % align = 0 := by
+      rw [Nat.add_mod] at hq
+      rw [Nat.add_mod, Nat.mod_mod]
+      exact hq
+    have heq := padding_unique len align (q % align) hpos
+      (Nat.mod_lt q hpos) hqm
+    have hp := padding_unique len align p hpos hlt haligned
+    have := Nat.mod_le q align
+    omega
+  · constructor
+    · intro hp
+      simpa only [hp, Nat.add_zero] using haligned
+    · intro hl
+      have hp := padding_unique len align p hpos hlt haligned
+      simpa only [hl, Nat.sub_zero, Nat.mod_self] using hp
+
+/-- 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) := by
+  have hr := Nat.mod_lt n hpos
+  have hrle := Nat.mod_le n align
+  have hmul : m = (n / align) * align := by
+    rw [Nat.div_mul_self_eq_mod_sub_self, hm]
+  refine ⟨by omega, ?_, by omega, ?_⟩
+  · rw [hmul, Nat.mul_mod_left]
+  · intro q hqn hqa
+    have hdiv := Nat.div_le_div_right (c := align) hqn
+    have hle := Nat.mul_le_mul_right align hdiv
+    rw [Nat.div_mul_self_eq_mod_sub_self, Nat.div_mul_self_eq_mod_sub_self,
+      hqa, Nat.sub_zero, ← hm] at hle
+    exact hle
+
+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/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 a493f48f70..ddd876429a 100644
--- a/zerocopy/src/util/mod.rs
+++ b/zerocopy/src/util/mod.rs
@@ -14,6 +14,8 @@ pub(crate) mod macros;
 #[doc(hidden)]
 pub mod macro_util;
 
+mod checks;
+
 use core::{
     marker::PhantomData,
     mem::{self, ManuallyDrop},
@@ -156,7 +158,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)]
@@ -243,7 +251,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,
@@ -270,7 +283,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() {
@@ -285,7 +299,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() {