Prove allocation size preparation and tail containment

verification/aeneas/README.md

@@ -40,6 +40,15 @@ equal sizes, including zero-sized layouts with different alignments. Rejection
 does not claim that a cast would be impossible. The proof covers the numerical
 decision and sizing comparison, not the resulting pointer's validity.
 
+The checks in [`util/allocation.rs`](../../zerocopy/src/util/allocation.rs) cover
+actual metadata sizing and exact preparation of allocator arguments. Preparation
+preserves every optional size and the supplied alignment, without adding a
+runtime validity filter. Under explicit correspondence to a valid recursive
+layout, separate lemmas establish complete size and tail containment. Numerical
+allocator admission additionally needs the outer alignment and the signed
+metadata-size bound. Allocator behavior, zeroing, and `Box` validity remain
+separate Rust obligations.
+
 These harnesses use the same annotation and proof rules as every other function.
 There is no root marker or separately maintained list of required functions.
 Every present specification must have its corresponding proof in both CI builds.

verification/aeneas/golden/Funs.lean

@@ -888,7 +888,7 @@ def layout.composition_checks.reference_pad
   else ok none
 
 /-- [zerocopy::util::min]:
-    Source: 'src/util/mod.rs', lines 305:0-311:1 -/
+    Source: 'src/util/mod.rs', lines 306:0-312:1 -/
 def util.min
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -908,7 +908,7 @@ def util.min
   else ok a
 
 /-- [zerocopy::util::max]:
-    Source: 'src/util/mod.rs', lines 289:0-295:1 -/
+    Source: 'src/util/mod.rs', lines 290:0-296:1 -/
 def util.max
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -928,7 +928,7 @@ def util.max
   else ok a
 
 /-- [zerocopy::util::padding_needed_for]:
-    Source: 'src/util/mod.rs', lines 169:0-229:1 -/
+    Source: 'src/util/mod.rs', lines 170:0-230:1 -/
 def util.padding_needed_for
   (len : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -1142,7 +1142,7 @@ def layout.composition_checks.check_extend
   else ok ()
 
 /-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
-    Source: 'src/util/mod.rs', lines 261:0-279:1 -/
+    Source: 'src/util/mod.rs', lines 262:0-280:1 -/
 def util.round_down_to_next_multiple_of_alignment
   (n : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -2487,6 +2487,105 @@ def split_at.numerical_checks.check_split_geometry
               else ok ()
   else ok ()
 
+/-- [zerocopy::util::allocation::prepare]:
+    Source: 'src/util/allocation.rs', lines 33:0-38:1 -/
+def util.allocation.prepare
+  (size : Option Std.Usize)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) :
+  Result (Option (Std.Usize × (core.num.nonzero.NonZero Std.Usize
+    core.num.niche_types.NonZeroUsizeInner)))
+  := do
+  match size with
+  | none => ok none
+  | some size1 => ok (some (size1, align))
+
+/-- [zerocopy::util::allocation::assert_preparation]:
+    Source: 'src/util/allocation.rs', lines 52:0-64:1 -/
+def util.allocation.assert_preparation
+  (size : Option Std.Usize)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) :
+  Result Unit
+  := do
+  let prepared ← util.allocation.prepare size align
+  match size with
+  | none => let b := core.option.Option.is_none prepared
+            massert b
+  | some size1 =>
+    match prepared with
+    | none => fail panic
+    | some p =>
+      let (actual_size, actual_align) := p
+      massert (actual_size = size1)
+      let i ←
+        core.num.nonzero.NonZero.get
+          Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner
+          actual_align
+      let i1 ←
+        core.num.nonzero.NonZero.get
+          Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
+      massert (i = i1)
+
+/-- [zerocopy::util::allocation::assert_allocation_size]:
+    Source: 'src/util/allocation.rs', lines 80:0-126:1 -/
+def util.allocation.assert_allocation_size
+  (runtime_layout : layout.DstLayout)
+  (rounding_align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
+  (metadata : Std.Usize) :
+  Result Unit
+  := do
+  match runtime_layout.size_info with
+  | layout.SizeInfo.Sized size =>
+    let actual ← pointer_metadata_unit_size_for_metadata runtime_layout
+    let b ← layout.tail_checks.same_optional_usize actual (some size)
+    massert b
+    util.allocation.assert_preparation actual runtime_layout.align
+    let o ← util.allocation.prepare actual runtime_layout.align
+    match o with
+    | none => ok ()
+    | some p =>
+      let (size1, _) := p
+      let b1 ←
+        layout.tail_checks.same_optional_usize (some size) (some size1)
+      massert b1
+  | layout.SizeInfo.SliceDst tail =>
+    let b ←
+      layout.tail_transform_checks.witness_matches tail rounding_align phase
+    if b
+    then
+      let actual ←
+        pointer_metadata_usize_size_for_metadata metadata runtime_layout
+      let expected ←
+        layout.tail_checks.reference_size tail rounding_align phase metadata
+      let b1 ← layout.tail_checks.same_optional_usize actual expected
+      massert b1
+      util.allocation.assert_preparation actual runtime_layout.align
+      let o ← util.allocation.prepare actual runtime_layout.align
+      match o with
+      | none => ok ()
+      | some p =>
+        let (size, _) := p
+        let b2 ← layout.tail_checks.same_optional_usize expected (some size)
+        massert b2
+        let o1 ← lift (Usize.checked_add tail.size_base phase)
+        match o1 with
+        | none => fail panic
+        | some start =>
+          if tail.offset > start
+          then ok ()
+          else
+            let o2 ← lift (Usize.checked_mul metadata tail.elem_size)
+            match o2 with
+            | none => fail panic
+            | some bytes =>
+              let o3 ← lift (Usize.checked_add tail.offset bytes)
+              match o3 with
+              | none => fail panic
+              | some «end» => massert («end» <= size)
+    else ok ()
+
 /-- [zerocopy::util::checks::check_arithmetic]:
     Source: 'src/util/checks.rs', lines 38:0-46:1 -/
 def util.checks.check_arithmetic

verification/aeneas/lean/Obligations/Allocation.lean

@@ -0,0 +1,47 @@
+/- 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 LayoutModel
+@[expose] public section
+
+open Aeneas Aeneas.Std
+namespace Zerocopy.Obligations
+open Zerocopy.Proofs
+
+/- This expectation independently classifies all optional machine sizes. The
+numerical preparation does not allocate or change the supplied metadata size.
+-/
+def allocation_prepare_spec_contract (size : Option Usize) (align : NonZeroUsize)
+    (run : Result (Option (Usize × NonZeroUsize))) : Prop :=
+  0 < align.val.val → run ⦃ result =>
+    result.map (fun pair => (pair.1.val, pair.2.val.val)) =
+      size.map (fun size => (size.val, align.val.val)) ⦄
+
+def allocation_prepare_spec : Prop :=
+  ∀ size align, allocation_prepare_spec_contract size align
+    (util.allocation.prepare size align)
+
+def allocation_preparation_check_spec_contract (_size : Option Usize) (align : NonZeroUsize)
+    (run : Result Unit) : Prop := 0 < align.val.val → run ⦃ _ => True ⦄
+
+def allocation_preparation_check_spec : Prop :=
+  ∀ size align, allocation_preparation_check_spec_contract size align
+    (util.allocation.assert_preparation size align)
+
+def allocation_size_check_spec_contract (runtime_layout : layout.DstLayout)
+    (rounding_align : NonZeroUsize) (_phase _metadata : Usize) (run : Result Unit) : Prop :=
+  0 < runtime_layout.align.val.val → canonicalLayout runtime_layout →
+  0 < rounding_align.val.val → run ⦃ _ => True ⦄
+
+def allocation_size_check_spec : Prop :=
+  ∀ runtime_layout rounding_align phase metadata,
+    allocation_size_check_spec_contract runtime_layout rounding_align phase metadata
+      (util.allocation.assert_allocation_size runtime_layout rounding_align phase metadata)
+
+end Zerocopy.Obligations