Prove least padding and greatest aligned predecessors

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

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)

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]:

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

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