Prove unit and usize PointerMetadata operations

verification/aeneas/README.md

@@ -56,6 +56,12 @@ allocator admission additionally needs the outer alignment and the signed
 metadata-size bound. Allocator behavior, zeroing, and `Box` validity remain
 separate Rust obligations.
 
+Six concrete wrappers in [`lib.rs`](../../zerocopy/src/lib.rs) call the actual
+`PointerMetadata` implementations for `()` and `usize`. Their contracts check
+element-count conversion, layout-variant handling, and checked metadata sizing.
+Using these results for an arbitrary `KnownLayout` implementation requires
+separate layout correspondence.
+
 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

@@ -1298,8 +1298,96 @@ def layout.tail_checks.trailing_arithmetic_check
     else ok ()
   else ok ()
 
+/-- [zerocopy::{impl zerocopy::PointerMetadata for ()}::from_elem_count]:
+    Source: 'src/lib.rs', lines 975:4-975:46
+    Visibility: public -/
+def Tuple.Insts.ZerocopyPointerMetadata.from_elem_count
+  (_elems : Std.Usize) : Result Unit := do
+  ok ()
+
+/-- [zerocopy::{impl zerocopy::PointerMetadata for ()}::to_elem_count]:
+    Source: 'src/lib.rs', lines 978:4-980:5
+    Visibility: public -/
+def Tuple.Insts.ZerocopyPointerMetadata.to_elem_count
+  (_ : Unit) : Result Std.Usize := do
+  ok 0#usize
+
+/-- [zerocopy::{impl zerocopy::PointerMetadata for ()}::size_for_metadata]:
+    Source: 'src/lib.rs', lines 983:4-990:5
+    Visibility: public -/
+def Tuple.Insts.ZerocopyPointerMetadata.size_for_metadata
+  (_ : Unit) (runtime_layout : layout.DstLayout) :
+  Result (Option Std.Usize)
+  := do
+  match runtime_layout.size_info with
+  | layout.SizeInfo.Sized size => ok (some size)
+  | layout.SizeInfo.SliceDst _ => ok none
+
+/-- [zerocopy::{impl zerocopy::PointerMetadata for usize}::from_elem_count]:
+    Source: 'src/lib.rs', lines 995:4-997:5
+    Visibility: public -/
+def Usize.Insts.ZerocopyPointerMetadata.from_elem_count
+  (elems : Std.Usize) : Result Std.Usize := do
+  ok elems
+
+/-- [zerocopy::{impl zerocopy::PointerMetadata for usize}::to_elem_count]:
+    Source: 'src/lib.rs', lines 1000:4-1002:5
+    Visibility: public -/
+def Usize.Insts.ZerocopyPointerMetadata.to_elem_count
+  (self : Std.Usize) : Result Std.Usize := do
+  ok self
+
+/-- [zerocopy::{impl zerocopy::PointerMetadata for usize}::size_for_metadata]:
+    Source: 'src/lib.rs', lines 1005:4-1012:5
+    Visibility: public -/
+def Usize.Insts.ZerocopyPointerMetadata.size_for_metadata
+  (self : Std.Usize) (runtime_layout : layout.DstLayout) :
+  Result (Option Std.Usize)
+  := do
+  match runtime_layout.size_info with
+  | layout.SizeInfo.Sized _ => ok none
+  | layout.SizeInfo.SliceDst trailing =>
+    layout.TrailingSliceLayoutUsize.size_for_elems trailing self
+
+/-- [zerocopy::pointer_metadata_unit_from_elem_count]:
+    Source: 'src/lib.rs', lines 1023:0-1025:1 -/
+def pointer_metadata_unit_from_elem_count
+  (elems : Std.Usize) : Result Unit := do
+  Tuple.Insts.ZerocopyPointerMetadata.from_elem_count elems
+
+/-- [zerocopy::pointer_metadata_unit_to_elem_count]:
+    Source: 'src/lib.rs', lines 1032:0-1034:1 -/
+def pointer_metadata_unit_to_elem_count : Result Std.Usize := do
+  Tuple.Insts.ZerocopyPointerMetadata.to_elem_count ()
+
+/-- [zerocopy::pointer_metadata_unit_size_for_metadata]:
+    Source: 'src/lib.rs', lines 1043:0-1045:1 -/
+def pointer_metadata_unit_size_for_metadata
+  (runtime_layout : layout.DstLayout) : Result (Option Std.Usize) := do
+  Tuple.Insts.ZerocopyPointerMetadata.size_for_metadata () runtime_layout
+
+/-- [zerocopy::pointer_metadata_usize_from_elem_count]:
+    Source: 'src/lib.rs', lines 1052:0-1054:1 -/
+def pointer_metadata_usize_from_elem_count
+  (elems : Std.Usize) : Result Std.Usize := do
+  Usize.Insts.ZerocopyPointerMetadata.from_elem_count elems
+
+/-- [zerocopy::pointer_metadata_usize_to_elem_count]:
+    Source: 'src/lib.rs', lines 1061:0-1063:1 -/
+def pointer_metadata_usize_to_elem_count
+  (metadata : Std.Usize) : Result Std.Usize := do
+  Usize.Insts.ZerocopyPointerMetadata.to_elem_count metadata
+
+/-- [zerocopy::pointer_metadata_usize_size_for_metadata]:
+    Source: 'src/lib.rs', lines 1072:0-1077:1 -/
+def pointer_metadata_usize_size_for_metadata
+  (metadata : Std.Usize) (runtime_layout : layout.DstLayout) :
+  Result (Option Std.Usize)
+  := do
+  Usize.Insts.ZerocopyPointerMetadata.size_for_metadata metadata runtime_layout
+
 /-- [zerocopy::FromZeros::new_zeroed]:
-    Source: 'src/lib.rs', lines 3827:4-3833:5
+    Source: 'src/lib.rs', lines 3891:4-3897:5
     Visibility: public -/
 @[trait_default]
 native_models def FromZeros.new_zeroed.default (Self : Type) : Result Self := do

verification/aeneas/golden/Types.lean

@@ -272,7 +272,7 @@ structure pointer.invariant.Alignment (Self : Type) where
     T
 
 /-- Trait declaration: [zerocopy::TryFromBytes]
-    Source: 'src/lib.rs', lines 1901:0-3451:1
+    Source: 'src/lib.rs', lines 1965:0-3515:1
     Visibility: public -/
 structure TryFromBytes (Self : Type) where
   only_derive_is_allowed_to_implement_this_trait : Result Unit
@@ -283,28 +283,28 @@ structure TryFromBytes (Self : Type) where
     pointer.invariant.Initialized → Result Bool
 
 /-- Trait declaration: [zerocopy::FromZeros]
-    Source: 'src/lib.rs', lines 3708:0-4074:1
+    Source: 'src/lib.rs', lines 3772:0-4138:1
     Visibility: public -/
 structure FromZeros (Self : Type) where
   TryFromBytesInst : TryFromBytes Self
   only_derive_is_allowed_to_implement_this_trait : Result Unit
   new_zeroed : Result Self
 
 /-- Trait declaration: [zerocopy::FromBytes]
-    Source: 'src/lib.rs', lines 4302:0-5714:1
+    Source: 'src/lib.rs', lines 4366:0-5778:1
     Visibility: public -/
 structure FromBytes (Self : Type) where
   FromZerosInst : FromZeros Self
   only_derive_is_allowed_to_implement_this_trait : Result Unit
 
 /-- Trait declaration: [zerocopy::IntoBytes]
-    Source: 'src/lib.rs', lines 5953:0-6426:1
+    Source: 'src/lib.rs', lines 6017:0-6490:1
     Visibility: public -/
 structure IntoBytes (Self : Type) where
   only_derive_is_allowed_to_implement_this_trait : Result Unit
 
 /-- Trait declaration: [zerocopy::Unaligned]
-    Source: 'src/lib.rs', lines 6564:0-6571:1
+    Source: 'src/lib.rs', lines 6628:0-6635:1
     Visibility: public -/
 structure Unaligned (Self : Type) where
   only_derive_is_allowed_to_implement_this_trait : Result Unit

verification/aeneas/lean/Obligations/PointerMetadata.lean

@@ -0,0 +1,66 @@
+/- 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
+set_option linter.unusedVariables false
+
+/- Concrete wrappers call the actual trait implementations. These expectations
+retain their complete raw domain and distinguish overflow from execution
+failure, without using an extracted operation to define the expected result. -/
+def pointer_metadata_unit_from_elem_count_spec_contract (elems : Usize)
+    (run : Result Unit) : Prop := run ⦃ result => result = () ⦄
+def pointer_metadata_unit_from_elem_count_spec : Prop := ∀ elems,
+  pointer_metadata_unit_from_elem_count_spec_contract elems
+    (pointer_metadata_unit_from_elem_count elems)
+
+def pointer_metadata_unit_to_elem_count_spec_contract (run : Result Usize) : Prop := run ⦃ result => result.val = 0 ⦄
+def pointer_metadata_unit_to_elem_count_spec : Prop :=
+  pointer_metadata_unit_to_elem_count_spec_contract pointer_metadata_unit_to_elem_count
+
+def pointer_metadata_usize_from_elem_count_spec_contract (elems : Usize)
+    (run : Result Usize) : Prop := run ⦃ result => result.val = elems.val ⦄
+def pointer_metadata_usize_from_elem_count_spec : Prop := ∀ elems,
+  pointer_metadata_usize_from_elem_count_spec_contract elems
+    (pointer_metadata_usize_from_elem_count elems)
+
+def pointer_metadata_usize_to_elem_count_spec_contract (metadata : Usize)
+    (run : Result Usize) : Prop := run ⦃ result => result.val = metadata.val ⦄
+def pointer_metadata_usize_to_elem_count_spec : Prop := ∀ metadata,
+  pointer_metadata_usize_to_elem_count_spec_contract metadata
+    (pointer_metadata_usize_to_elem_count metadata)
+
+def pointer_metadata_unit_size_for_metadata_spec_contract (runtime_layout : layout.DstLayout) (run : Result (Option Usize)) : Prop :=
+  layoutValid runtime_layout → run ⦃ result =>
+    match runtime_layout.size_info with
+    | .Sized bytes => ∃ size, result = some size ∧ size.val = bytes.val
+    | .SliceDst _ => result = none ⦄
+def pointer_metadata_unit_size_for_metadata_spec : Prop := ∀ runtime_layout,
+  pointer_metadata_unit_size_for_metadata_spec_contract runtime_layout
+    (pointer_metadata_unit_size_for_metadata runtime_layout)
+
+def pointer_metadata_usize_size_for_metadata_spec_contract (metadata : Usize)
+    (runtime_layout : layout.DstLayout) (run : Result (Option Usize)) : Prop :=
+  layoutValid runtime_layout → run ⦃ result =>
+    match runtime_layout.size_info with
+    | .Sized _ => result = none
+    | .SliceDst tail => match result with
+      | none => Usize.max < (trailingFormula tail).size metadata.val
+      | some size => size.val = (trailingFormula tail).size metadata.val ∧
+        (trailingFormula tail).size metadata.val ≤ Usize.max ⦄
+def pointer_metadata_usize_size_for_metadata_spec : Prop := ∀ metadata runtime_layout,
+  pointer_metadata_usize_size_for_metadata_spec_contract metadata runtime_layout
+    (pointer_metadata_usize_size_for_metadata metadata runtime_layout)
+
+end Zerocopy.Obligations

verification/aeneas/lean/Proofs/PointerMetadata.lean

@@ -0,0 +1,121 @@
+/- 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 RequiredModelContracts.PointerMetadata
+@[expose] public section
+
+open Aeneas Aeneas.Std
+namespace Zerocopy.Proofs.Raw.PointerMetadata
+
+/- The wrapper unfolds to the extracted concrete trait method. These proofs
+retain that call, rather than substitute a second arithmetic implementation. -/
+theorem pointer_metadata_unit_from_elem_count_spec (elems : Usize) :
+    Zerocopy.pointer_metadata_unit_from_elem_count elems ⦃ result => result = () ⦄ := by
+  simp [Zerocopy.pointer_metadata_unit_from_elem_count,
+    Tuple.Insts.ZerocopyPointerMetadata.from_elem_count, WP.spec_ok]
+
+theorem pointer_metadata_unit_to_elem_count_spec :
+    Zerocopy.pointer_metadata_unit_to_elem_count ⦃ result => result.val = 0 ⦄ := by
+  simp [Zerocopy.pointer_metadata_unit_to_elem_count,
+    Tuple.Insts.ZerocopyPointerMetadata.to_elem_count, WP.spec_ok]
+
+theorem pointer_metadata_usize_from_elem_count_spec (elems : Usize) :
+    Zerocopy.pointer_metadata_usize_from_elem_count elems ⦃ result => result = elems ⦄ := by
+  simp [Zerocopy.pointer_metadata_usize_from_elem_count,
+    Usize.Insts.ZerocopyPointerMetadata.from_elem_count, WP.spec_ok]
+
+theorem pointer_metadata_usize_to_elem_count_spec (metadata : Usize) :
+    Zerocopy.pointer_metadata_usize_to_elem_count metadata ⦃ result => result = metadata ⦄ := by
+  simp [Zerocopy.pointer_metadata_usize_to_elem_count,
+    Usize.Insts.ZerocopyPointerMetadata.to_elem_count, WP.spec_ok]
+
+theorem pointer_metadata_unit_size_for_metadata_spec (runtime_layout : layout.DstLayout) :
+    Zerocopy.pointer_metadata_unit_size_for_metadata runtime_layout ⦃ result =>
+      result = match runtime_layout.size_info with
+        | .Sized size => some size
+        | .SliceDst _ => none ⦄ := by
+  unfold Zerocopy.pointer_metadata_unit_size_for_metadata
+    Tuple.Insts.ZerocopyPointerMetadata.size_for_metadata
+  cases runtime_layout.size_info <;> simp [WP.spec_ok]
+
+theorem pointer_metadata_usize_size_for_metadata_spec (metadata : Usize)
+    (runtime_layout : layout.DstLayout)
+    (positive : match runtime_layout.size_info with
+      | .Sized _ => True
+      | .SliceDst tail => 0 < tail.size_rounding_align_and_phase._0.val.val) :
+    Zerocopy.pointer_metadata_usize_size_for_metadata metadata runtime_layout ⦃ result =>
+      result.map UScalar.val = match runtime_layout.size_info with
+        | .Sized _ => none
+        | .SliceDst tail => (trailingFormula tail).checkedSize Usize.max metadata.val ⦄ := by
+  unfold Zerocopy.pointer_metadata_usize_size_for_metadata
+    Usize.Insts.ZerocopyPointerMetadata.size_for_metadata
+  cases info : runtime_layout.size_info with
+  | Sized size => simp [WP.spec_ok]
+  | SliceDst tail =>
+    simp only [info] at positive
+    exact Zerocopy.Proofs.Raw.size_for_elems_spec tail metadata positive
+
+end Zerocopy.Proofs.Raw.PointerMetadata
+
+namespace Zerocopy.Proofs
+open AeneasSpecs
+
+theorem pointer_metadata_unit_from_elem_count_spec : Specs.pointer_metadata_unit_from_elem_count_spec := by
+  unfold Specs.pointer_metadata_unit_from_elem_count_spec
+  representation_simps
+  intro elems
+  apply WP.spec_mono (Raw.PointerMetadata.pointer_metadata_unit_from_elem_count_spec elems)
+  intro result _facts
+  exact ⟨result, rfl⟩
+register_spec_step pointer_metadata_unit_from_elem_count_spec
+
+theorem pointer_metadata_unit_to_elem_count_spec : Specs.pointer_metadata_unit_to_elem_count_spec := by
+  unfold Specs.pointer_metadata_unit_to_elem_count_spec
+  representation_simps
+  exact Raw.PointerMetadata.pointer_metadata_unit_to_elem_count_spec
+register_spec_step pointer_metadata_unit_to_elem_count_spec
+
+theorem pointer_metadata_usize_from_elem_count_spec : Specs.pointer_metadata_usize_from_elem_count_spec := by
+  unfold Specs.pointer_metadata_usize_from_elem_count_spec
+  representation_simps
+  intro elems
+  exact Raw.PointerMetadata.pointer_metadata_usize_from_elem_count_spec elems
+register_spec_step pointer_metadata_usize_from_elem_count_spec
+
+theorem pointer_metadata_usize_to_elem_count_spec : Specs.pointer_metadata_usize_to_elem_count_spec := by
+  unfold Specs.pointer_metadata_usize_to_elem_count_spec
+  representation_simps
+  intro metadata
+  exact Raw.PointerMetadata.pointer_metadata_usize_to_elem_count_spec metadata
+register_spec_step pointer_metadata_usize_to_elem_count_spec
+
+theorem pointer_metadata_unit_size_for_metadata_spec : Specs.pointer_metadata_unit_size_for_metadata_spec := by
+  unfold Specs.pointer_metadata_unit_size_for_metadata_spec
+  representation_simps
+  intro runtime_layout _valid
+  exact Raw.PointerMetadata.pointer_metadata_unit_size_for_metadata_spec runtime_layout
+register_spec_step pointer_metadata_unit_size_for_metadata_spec
+
+theorem pointer_metadata_usize_size_for_metadata_spec : Specs.pointer_metadata_usize_size_for_metadata_spec := by
+  unfold Specs.pointer_metadata_usize_size_for_metadata_spec
+  representation_simps
+  intro metadata runtime_layout valid
+  have positive : match runtime_layout.size_info with
+      | .Sized _ => True
+      | .SliceDst tail => 0 < tail.size_rounding_align_and_phase._0.val.val := by
+    cases info : runtime_layout.size_info with
+    | Sized size => trivial
+    | SliceDst tail => simpa only [info] using valid.2
+  exact Raw.PointerMetadata.pointer_metadata_usize_size_for_metadata_spec
+    metadata runtime_layout positive
+register_spec_step pointer_metadata_usize_size_for_metadata_spec
+
+end Zerocopy.Proofs