Prove cast validation and exact metadata inference

verification/aeneas/README.md

@@ -170,6 +170,7 @@ added without extending the specification set.
 | `DstLayout::{extend,pad_to_align}` | Exact field placement, alignment, padding flags, and normalized size formulas; outer padding preserves each field's complete inner size. |
 | Trailing advancement and size-sequence comparison | Exact byte advancement; a positive comparison establishes equal sizes for every natural metadata value. |
 | `DstLayout::requires_dynamic_padding` | Exact flag result and a mathematical condition sufficient to eliminate dynamic padding for all metadata values. |
+| Cast validation and exact-size metadata | Alignment/size error priority, greatest fitting metadata, exact prefix/suffix split, and rejection of unattainable sizes. |
 
 Every registered function uses total `spec`: accepted raw representations,
 supplied mathematical ghosts, and explicit requirements imply successful
@@ -207,6 +208,10 @@ padding inside packed fields.
 A positive size-sequence comparison establishes equal sizes for every natural
 metadata value; a negative result does not assert that the sequences differ.
 
+Cast validation and exact metadata inference establish error priority, exact
+splits and rejection of unattainable sizes. Intentional zero-stride panic is
+checked separately.
+
 Plain arithmetic clauses use mathematical word values carrying machine bounds
 and NonZero positivity. Their Nat/Int arithmetic does not wrap; explicit raw
 clauses preserve the extracted representation vocabulary while retaining
@@ -506,6 +511,11 @@ audit checks those identities and their generated-module ownership in both
 directions, independently scans raw nominal types, and rejects missing or extra
 provider registrations. This reuses one verified table without another coverage roster.
 
+For cast validation and
+exact-size metadata, the required outcomes spell out error priority, split
+positions, exact size, and greatest-fitting metadata independently of the
+predicates used by the inline specs. `OutcomeTests.lean` pins distinguishing
+fixed-size, suffix-alignment, and padded-size plateau examples.
 `Check.lean` derives dependencies from elaborated theorem types and terms,
 following helpers across handwritten modules, including private helpers, and
 writes `proof-dependencies.json` in each proof workspace. It imports and audits all

verification/aeneas/golden/Funs.lean

@@ -1674,6 +1674,100 @@ def layout.DstLayout.requires_dynamic_padding
       then ok true
       else ok (¬ (i1 = 0#usize))
 
+/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::validate_cast_and_convert_metadata]:
+    Source: 'src/layout/mod.rs', lines 1839:4-1986:5 -/
+def layout.DstLayout.validate_cast_and_convert_metadata
+  (self : layout.DstLayout) (addr : Std.Usize) (bytes_len : Std.Usize)
+  (cast_type : layout.CastType) :
+  Result (core.result.Result (Std.Usize × Std.Usize) layout.MetadataCastError)
+  := do
+  let o ← layout.SizeInfoUsize.try_to_nonzero_elem_size self.size_info
+  match o with
+  | none => fail panic
+  | some size_info =>
+    let o1 ← lift (Usize.checked_add addr bytes_len)
+    let e := core.option.Option.is_some o1
+    massert e
+    let offset ←
+      match cast_type with
+      | layout.CastType.Prefix => ok 0#usize
+      | layout.CastType.Suffix => ok bytes_len
+    let i ← addr + offset
+    let i1 ←
+      core.num.nonzero.NonZero.get
+        Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner 
+        self.align
+    let i2 ← i % i1
+    if i2 != 0#usize
+    then ok (core.result.Result.Err layout.MetadataCastError.Alignment)
+    else
+      match size_info with
+      | layout.SizeInfo.Sized size =>
+        massert ((size > bytes_len) || (size <= bytes_len))
+        if size > bytes_len
+        then ok (core.result.Result.Err layout.MetadataCastError.Size)
+        else
+          match cast_type with
+          | layout.CastType.Prefix =>
+            ok (core.result.Result.Ok (0#usize, size))
+          | layout.CastType.Suffix =>
+            let split_at ← bytes_len - size
+            ok (core.result.Result.Ok (0#usize, split_at))
+      | layout.SizeInfo.SliceDst trailing =>
+        let o2 ←
+          layout.TrailingSliceLayout.max_trailing_bytes trailing bytes_len
+        match o2 with
+        | none => ok (core.result.Result.Err layout.MetadataCastError.Size)
+        | some bytes =>
+          let (elems, _) ←
+            layout.max_elems_for_bytes bytes trailing.elem_size
+          let size_align ←
+            layout.RoundingAlignAndPhase.align
+              trailing.size_rounding_align_and_phase
+          let i3 ←
+            core.num.nonzero.NonZero.get
+              Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner
+              trailing.elem_size
+          let unused_bytes ← bytes % i3
+          let unused_aligned_bytes ←
+            util.round_down_to_next_multiple_of_alignment unused_bytes
+              size_align
+          let i4 ← bytes_len - trailing.size_base
+          let max_rounded_bytes ←
+            util.round_down_to_next_multiple_of_alignment i4 size_align
+          let i5 ← max_rounded_bytes - unused_aligned_bytes
+          let self_bytes ← trailing.size_base + i5
+          massert (self_bytes <= bytes_len)
+          match cast_type with
+          | layout.CastType.Prefix =>
+            ok (core.result.Result.Ok (elems, self_bytes))
+          | layout.CastType.Suffix =>
+            let split_at ← bytes_len - self_bytes
+            ok (core.result.Result.Ok (elems, split_at))
+
+/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::metadata_for_exact_size]:
+    Source: 'src/layout/mod.rs', lines 1701:4-1724:5 -/
+def layout.DstLayout.metadata_for_exact_size
+  (self : layout.DstLayout) (size : Std.Usize) :
+  Result (Option Std.Usize)
+  := do
+  match self.size_info with
+  | layout.SizeInfo.Sized _ => ok none
+  | layout.SizeInfo.SliceDst tsl =>
+    match tsl.elem_size.val with
+    | 0 => ok none
+    | _ =>
+      let r ←
+        layout.DstLayout.validate_cast_and_convert_metadata self 0#usize size
+          layout.CastType.Prefix
+      match r with
+      | core.result.Result.Ok p =>
+        let (elems, object_size) := p
+        if object_size = size
+        then ok (some elems)
+        else ok none
+      | core.result.Result.Err _ => ok none
+
 /-- [zerocopy::layout::nested_reference::round_up]:
     Source: 'src/layout/nested_reference.rs', lines 46:0-56:1 -/
 def layout.nested_reference.round_up
@@ -1953,8 +2047,82 @@ def layout.tail_checks.reference_capacity
     let rounded_budget ← after_base - i1
     ok (Usize.checked_sub rounded_budget phase)
 
+/-- [zerocopy::layout::tail_checks::reference_metadata]:
+    Source: 'src/layout/tail_checks.rs', lines 78:0-104:1 -/
+def layout.tail_checks.reference_metadata
+  (runtime_layout : layout.DstLayout)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
+  (size : Std.Usize) :
+  Result (Option Std.Usize)
+  := do
+  match runtime_layout.size_info with
+  | layout.SizeInfo.Sized _ => ok none
+  | layout.SizeInfo.SliceDst tail =>
+    if tail.elem_size = 0#usize
+    then ok none
+    else
+      let o ← layout.tail_checks.reference_capacity tail align phase size
+      match o with
+      | none => ok none
+      | some bytes =>
+        let elems ← bytes / tail.elem_size
+        let o1 ← layout.tail_checks.reference_size tail align phase elems
+        let b ← layout.tail_checks.same_optional_usize o1 (some size)
+        if b
+        then ok (some elems)
+        else ok none
+
+/-- [zerocopy::layout::tail_checks::reference_cast]:
+    Source: 'src/layout/tail_checks.rs', lines 107:0-154:1 -/
+def layout.tail_checks.reference_cast
+  (runtime_layout : layout.DstLayout)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
+  (addr : Std.Usize) (length : Std.Usize) (side : layout.CastType) :
+  Result (core.result.Result (Std.Usize × Std.Usize) layout.MetadataCastError)
+  := do
+  let anchor ←
+    match side with
+    | layout.CastType.Prefix => ok addr
+    | layout.CastType.Suffix => addr + length
+  let i ←
+    core.num.nonzero.NonZero.get
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner
+      runtime_layout.align
+  let i1 ← anchor % i
+  if i1 != 0#usize
+  then ok (core.result.Result.Err layout.MetadataCastError.Alignment)
+  else
+    let candidate ←
+      match runtime_layout.size_info with
+      | layout.SizeInfo.Sized size =>
+        if size <= length
+        then ok (some (0#usize, size))
+        else ok none
+      | layout.SizeInfo.SliceDst tail =>
+        do
+        let o ← layout.tail_checks.reference_capacity tail align phase length
+        match o with
+        | none => ok none
+        | some bytes =>
+          let elems ← bytes / tail.elem_size
+          let o1 ← layout.tail_checks.reference_size tail align phase elems
+          match o1 with
+          | none => ok none
+          | some size => ok (some (elems, size))
+    match candidate with
+    | none => ok (core.result.Result.Err layout.MetadataCastError.Size)
+    | some p =>
+      let (elems, size) := p
+      match side with
+      | layout.CastType.Prefix => ok (core.result.Result.Ok p)
+      | layout.CastType.Suffix =>
+        let split ← length - size
+        ok (core.result.Result.Ok (elems, split))
+
 /-- [zerocopy::layout::tail_checks::trailing_arithmetic_check]:
-    Source: 'src/layout/tail_checks.rs', lines 88:0-111:1 -/
+    Source: 'src/layout/tail_checks.rs', lines 166:0-189:1 -/
 def layout.tail_checks.trailing_arithmetic_check
   (tail : layout.TrailingSliceLayout Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -1991,6 +2159,96 @@ def layout.tail_checks.trailing_arithmetic_check
     else ok ()
   else ok ()
 
+/-- [zerocopy::layout::tail_checks::layout_observations_check]:
+    Source: 'src/layout/tail_checks.rs', lines 204:0-247:1 -/
+def layout.tail_checks.layout_observations_check
+  (runtime_layout : layout.DstLayout)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
+  (size : Std.Usize) (addr : Std.Usize) (length : Std.Usize)
+  (side : layout.CastType) :
+  Result Unit
+  := do
+  let (si, encoding_matches) ←
+    match runtime_layout.size_info with
+    | layout.SizeInfo.Sized _ => ok (runtime_layout.size_info, true)
+    | layout.SizeInfo.SliceDst tail =>
+      do
+      let i ←
+        core.num.nonzero.NonZero.get
+          Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
+      let b ← core.num.Usize.is_power_of_two i
+      let b1 ←
+        if b
+        then
+          if phase < i
+          then
+            do
+            let o ← lift (Usize.checked_add i phase)
+            let i1 ←
+              core.num.nonzero.NonZero.get
+                Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner
+                tail.size_rounding_align_and_phase._0
+            layout.tail_checks.same_optional_usize o (some i1)
+          else ok false
+        else ok false
+      ok (runtime_layout.size_info, b1)
+  if encoding_matches
+  then
+    let o ←
+      layout.DstLayout.metadata_for_exact_size
+        { runtime_layout with size_info := si } size
+    let o1 ←
+      layout.tail_checks.reference_metadata
+        { runtime_layout with size_info := si } align phase size
+    let b ← layout.tail_checks.same_optional_usize o o1
+    massert b
+    let nonzero_stride ←
+      match si with
+      | layout.SizeInfo.Sized _ => ok true
+      | layout.SizeInfo.SliceDst tail => ok (tail.elem_size != 0#usize)
+    let o2 ← lift (Usize.checked_add addr length)
+    let b1 := core.option.Option.is_some o2
+    if b1
+    then
+      if nonzero_stride
+      then
+        let actual ←
+          layout.DstLayout.validate_cast_and_convert_metadata
+            { runtime_layout with size_info := si } addr length side
+        let expected ←
+          layout.tail_checks.reference_cast
+            { runtime_layout with size_info := si } align phase addr length
+            side
+        let same ←
+          match actual with
+          | core.result.Result.Ok p =>
+            match expected with
+            | core.result.Result.Ok p1 =>
+              let (elems, split) := p
+              let (expected_elems, expected_split) := p1
+              if elems = expected_elems
+              then ok (split = expected_split)
+              else ok false
+            | core.result.Result.Err _ => ok false
+          | core.result.Result.Err mce =>
+            match expected with
+            | core.result.Result.Ok _ => ok false
+            | core.result.Result.Err mce1 =>
+              match mce with
+              | layout.MetadataCastError.Alignment =>
+                match mce1 with
+                | layout.MetadataCastError.Alignment => ok true
+                | layout.MetadataCastError.Size => ok false
+              | layout.MetadataCastError.Size =>
+                match mce1 with
+                | layout.MetadataCastError.Alignment => ok false
+                | layout.MetadataCastError.Size => ok true
+        massert same
+      else ok ()
+    else ok ()
+  else ok ()
+
 /-- [zerocopy::layout::tail_transform_checks::witness_matches]:
     Source: 'src/layout/tail_transform_checks.rs', lines 30:0-37:1 -/
 def layout.tail_transform_checks.witness_matches

verification/aeneas/golden/Types.lean

@@ -154,6 +154,21 @@ structure layout.DstLayout where
   size_info : layout.SizeInfo Std.Usize
   statically_shallow_unpadded : Bool
 
+/-- [zerocopy::layout::CastType]
+    Source: 'src/layout/mod.rs', lines 913:0-916:1
+    Visibility: public -/
+@[discriminant isize]
+inductive layout.CastType where
+| Prefix : layout.CastType
+| Suffix : layout.CastType
+
+/-- [zerocopy::layout::MetadataCastError]
+    Source: 'src/layout/mod.rs', lines 920:0-923:1 -/
+@[discriminant isize]
+inductive layout.MetadataCastError where
+| Alignment : layout.MetadataCastError
+| Size : layout.MetadataCastError
+
 /-- [zerocopy::layout::nested_reference::NestedLayer]
     Source: 'src/layout/nested_reference.rs', lines 27:0-31:1 -/
 structure layout.nested_reference.NestedLayer where

verification/aeneas/lean/Corollaries.lean

@@ -166,4 +166,15 @@ theorem padding_matches_recursive (tail : layout.TrailingSliceLayout Usize)
   dsimp only [remaining, physical] at hcancel
   omega
 
+theorem validate_zero_stride (self : layout.DstLayout) (tail : layout.TrailingSliceLayout Usize)
+    (hs : self.size_info = .SliceDst tail) (he : tail.elem_size = 0#usize)
+    (addr length : Usize) (side : layout.CastType) :
+    layout.DstLayout.validate_cast_and_convert_metadata self addr length side = .fail .panic := by
+  have hp := Proofs.Raw.try_nonzero_spec self.size_info
+  obtain ⟨converted, hconverted, hv⟩ := WP.spec_imp_exists hp
+  simp only [hs, he, if_true] at hv
+  unfold layout.DstLayout.validate_cast_and_convert_metadata
+  rw [hconverted, hv]
+  simp only [bind_ok]
+
 end Zerocopy.Corollaries