Prove concrete pointer metadata operations

verification/aeneas/README.md

@@ -20,6 +20,12 @@ assertion to pass. Review the independent calculation, complete comparisons,
 and early returns together: returning early excludes that input from the
 comparison.
 
+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

@@ -1290,6 +1290,94 @@ def layout.tail_checks.trailing_arithmetic_check
     else ok ()
   else ok ()
 
+/-- [zerocopy::{impl zerocopy::PointerMetadata for ()}::from_elem_count]:
+    Source: 'src/lib.rs', lines 973:4-973: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 976:4-978: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 981:4-988: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 993:4-995: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 998:4-1000: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 1003:4-1010: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 1021:0-1023: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 1030:0-1032: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 1041:0-1043: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 1050:0-1052: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 1059:0-1061: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 1070:0-1075: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::util::checks::check_arithmetic]:
     Source: 'src/util/checks.rs', lines 38:0-46:1 -/
 def util.checks.check_arithmetic

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

verification/aeneas/lean/RequiredModelContracts/PointerMetadata.lean

@@ -0,0 +1,86 @@
+/- 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 Obligations.PointerMetadata
+public import RequiredModelContracts
+@[expose] public section
+
+open Aeneas Aeneas.Std AeneasSpecs
+namespace Zerocopy.Proofs
+
+/- Every adapter consumes the supplied contract for the same arbitrary run.
+No canonical implementation theorem is used to repair a weak specification. -/
+@[contract_simps] theorem required_pointer_metadata_unit_from_elem_count (elems : Usize)
+    (run : Result Unit)
+    (provided : Specs.pointer_metadata_unit_from_elem_count_spec_contract elems run) :
+    Obligations.pointer_metadata_unit_from_elem_count_spec_contract elems run := by
+  apply WP.spec_mono (provided (unsignedWord elems) rfl)
+  rintro result ⟨_value, _decoded, facts⟩
+  exact facts
+
+@[contract_simps] theorem required_pointer_metadata_unit_to_elem_count (run : Result Usize)
+    (provided : Specs.pointer_metadata_unit_to_elem_count_spec_contract run) :
+    Obligations.pointer_metadata_unit_to_elem_count_spec_contract run := by
+  apply WP.spec_mono provided
+  rintro result ⟨_value, _decoded, facts⟩
+  exact facts
+
+@[contract_simps] theorem required_pointer_metadata_usize_from_elem_count (elems : Usize)
+    (run : Result Usize)
+    (provided : Specs.pointer_metadata_usize_from_elem_count_spec_contract elems run) :
+    Obligations.pointer_metadata_usize_from_elem_count_spec_contract elems run := by
+  apply WP.spec_mono (provided (unsignedWord elems) rfl)
+  rintro result ⟨_value, _decoded, facts⟩
+  exact congrArg UScalar.val facts
+
+@[contract_simps] theorem required_pointer_metadata_usize_to_elem_count (metadata : Usize)
+    (run : Result Usize)
+    (provided : Specs.pointer_metadata_usize_to_elem_count_spec_contract metadata run) :
+    Obligations.pointer_metadata_usize_to_elem_count_spec_contract metadata run := by
+  apply WP.spec_mono (provided (unsignedWord metadata) rfl)
+  rintro result ⟨_value, _decoded, facts⟩
+  exact congrArg UScalar.val facts
+
+@[contract_simps] theorem required_pointer_metadata_unit_size_for_metadata (runtime_layout : layout.DstLayout) (run : Result (Option Usize))
+    (provided : Specs.pointer_metadata_unit_size_for_metadata_spec_contract runtime_layout run) :
+    Obligations.pointer_metadata_unit_size_for_metadata_spec_contract runtime_layout run := by
+  intro valid
+  obtain ⟨value, decoded⟩ := (layout_valid_iff runtime_layout).mpr valid
+  apply WP.spec_mono (provided value decoded)
+  rintro result ⟨_value, _decoded, facts⟩
+  cases info : runtime_layout.size_info with
+  | Sized bytes =>
+    simp only [info] at facts ⊢
+    exact ⟨bytes, facts, rfl⟩
+  | SliceDst tail => simpa only [info] using facts
+
+@[contract_simps] theorem required_pointer_metadata_usize_size_for_metadata (metadata : Usize)
+    (runtime_layout : layout.DstLayout) (run : Result (Option Usize))
+    (provided : Specs.pointer_metadata_usize_size_for_metadata_spec_contract metadata runtime_layout run) :
+    Obligations.pointer_metadata_usize_size_for_metadata_spec_contract metadata runtime_layout run := by
+  intro valid
+  obtain ⟨value, decoded⟩ := (layout_valid_iff runtime_layout).mpr valid
+  apply WP.spec_mono (provided (unsignedWord metadata) rfl value decoded)
+  rintro result ⟨_value, _decoded, facts⟩
+  cases info : runtime_layout.size_info with
+  | Sized bytes =>
+    simp only [info] at facts ⊢
+    cases result <;> simp_all
+  | SliceDst tail =>
+    simp only [info] at facts ⊢
+    cases result with
+    | none =>
+      simp only [Option.map_none, LayoutMath.Formula.checkedSize] at facts
+      split at facts <;> simp_all
+    | some size =>
+      simp only [Option.map_some, LayoutMath.Formula.checkedSize] at facts
+      split at facts <;> simp_all
+
+end Zerocopy.Proofs