joshlf · Oct 2, 2026
diff --git 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,20 +130,20 @@ 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
 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
@@ -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
@@ -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
@@ -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