Prove advancement and padding-sequence decisions

verification/aeneas/README.md

@@ -268,7 +268,7 @@ whole-program unsafe-code certification.
 
 ## Scope and proofs
 
-Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs), [nested reference](../../zerocopy/src/layout/nested_reference.rs), [primitive assertions](../../zerocopy/src/layout/primitive_checks.rs), [tail assertions](../../zerocopy/src/layout/tail_checks.rs), [composition assertions](../../zerocopy/src/layout/composition_checks.rs).
+Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs), [nested reference](../../zerocopy/src/layout/nested_reference.rs), [primitive assertions](../../zerocopy/src/layout/primitive_checks.rs), [tail assertions](../../zerocopy/src/layout/tail_checks.rs), [composition assertions](../../zerocopy/src/layout/composition_checks.rs), [tail transformations](../../zerocopy/src/layout/tail_transform_checks.rs).
 
 Extraction starts from the function and nominal-type owners of every present
 `aeneas` fence in `zerocopy/src`, including their dependencies. The current
@@ -364,6 +364,9 @@ to the independent recursive semantics.
 Extension and normalized padding preserve complete inner sizes, including
 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.
+
 Plain arithmetic clauses use mathematical word values carrying machine bounds
 and, for NonZero, positivity. They coerce to `Nat` or `Int` without unwrapping
 raw fields. Binding `let N : Nat := n` makes addition and remainder ordinary

verification/aeneas/golden/Types.lean

@@ -203,28 +203,28 @@ structure layout.composition_checks.ReferenceLayout where
   unpadded : Bool
 
 /-- [zerocopy::layout::RoundingAlignAndPhase]
-    Source: 'src/layout/mod.rs', lines 90:0-90:54 -/
+    Source: 'src/layout/mod.rs', lines 93:0-93:54 -/
 structure layout.RoundingAlignAndPhase where
   _0 : core.num.nonzero.NonZero Std.Usize
     core.num.niche_types.NonZeroUsizeInner
 
 /-- [zerocopy::layout::TrailingSliceLayout]
-    Source: 'src/layout/mod.rs', lines 197:0-251:1 -/
+    Source: 'src/layout/mod.rs', lines 200:0-254:1 -/
 structure layout.TrailingSliceLayout (E : Type) where
   offset : Std.Usize
   elem_size : E
   size_base : Std.Usize
   size_rounding_align_and_phase : layout.RoundingAlignAndPhase
 
 /-- [zerocopy::layout::SizeInfo]
-    Source: 'src/layout/mod.rs', lines 59:0-62:1 -/
+    Source: 'src/layout/mod.rs', lines 62:0-65:1 -/
 @[discriminant isize]
 inductive layout.SizeInfo (E : Type) where
 | Sized : Std.Usize → layout.SizeInfo E
 | SliceDst : layout.TrailingSliceLayout E → layout.SizeInfo E
 
 /-- [zerocopy::layout::DstLayout]
-    Source: 'src/layout/mod.rs', lines 46:0-54:1
+    Source: 'src/layout/mod.rs', lines 49:0-57:1
     Visibility: public -/
 structure layout.DstLayout where
   align : core.num.nonzero.NonZero Std.Usize

verification/aeneas/lean/MathViews.lean

@@ -178,6 +178,14 @@ def layoutValid (self : layout.DstLayout) : Prop :=
   simpa only [trailingValid, encodingValid, scalar_valid_iff, true_and] using
     trailing_admitted_iff raw
 
+-- Optional traversal exposes the same fixed provider's named decoder directly.
+@[contract_simps] theorem trailing_usize_decoder_admitted_iff
+    (raw : layout.TrailingSliceLayout Usize) :
+    (∃ value : layout.TrailingSliceLayout.Fields (UnsignedWord .Usize),
+      layout.TrailingSliceLayout.decode Usize raw = some value) ↔
+      0 < raw.size_rounding_align_and_phase._0.val.val :=
+  trailing_usize_admitted_iff raw
+
 @[contract_simps] theorem normalized_nat_pos_iff (n : Nat) :
     Nat.le (Nat.succ 0) n ↔ 0 < n := Nat.succ_le_iff
 
@@ -203,11 +211,4 @@ attribute [contract_simps] encodingValid trailingValid sizeInfoValid layoutValid
 
 -- A named decoder can also occur after a surrounding structural traversal
 -- exposes the retained dictionary. These are the same admission equivalences.
-@[contract_simps] theorem trailing_usize_decoder_admitted_iff
-    (raw : layout.TrailingSliceLayout Usize) :
-    (∃ value : layout.TrailingSliceLayout.Fields (UnsignedWord .Usize),
-      layout.TrailingSliceLayout.decode Usize raw = some value) ↔
-      0 < raw.size_rounding_align_and_phase._0.val.val :=
-  trailing_usize_admitted_iff raw
-
 end Zerocopy.Proofs

verification/aeneas/lean/Obligations.lean

@@ -170,6 +170,31 @@ def size_for_elems_spec : Prop :=
   ∀ (t : layout.TrailingSliceLayout Usize) (n : Usize),
     size_for_elems_spec_contract t n (layout.TrailingSliceLayoutUsize.size_for_elems t n)
 
+def same_size_sequence_spec_contract (a b : layout.TrailingSliceLayout Usize)
+    (run : Result Bool) : Prop :=
+  0 < a.size_rounding_align_and_phase._0.val.val → 0 < b.size_rounding_align_and_phase._0.val.val →
+    ∃ same, run = .ok same ∧
+      (same = true → ∀ n : Nat, (trailingFormula a).size n = (trailingFormula b).size n)
+
+def same_size_sequence_spec : Prop :=
+  ∀ (a b : layout.TrailingSliceLayout Usize),
+    same_size_sequence_spec_contract a b
+      (layout.TrailingSliceLayoutUsize.has_same_size_sequence a b)
+
+def advance_spec_contract (t : layout.TrailingSliceLayout Usize) (bytes stride : Usize)
+    (run : Result (Option (layout.TrailingSliceLayout Usize))) : Prop :=
+  0 < t.size_rounding_align_and_phase._0.val.val →
+    run ⦃ r => (∀ next ∈ r, encodingValid next.size_rounding_align_and_phase) ∧
+      match r with
+      | none => Usize.max < ((trailingFormula t).advance bytes.val stride.val).base
+      | some next => trailingFormula next = (trailingFormula t).advance bytes.val stride.val ∧
+        ((trailingFormula t).advance bytes.val stride.val).base ≤ Usize.max ⦄
+
+def advance_spec : Prop :=
+  ∀ (t : layout.TrailingSliceLayout Usize) (bytes stride : Usize),
+    advance_spec_contract t bytes stride
+      (layout.TrailingSliceLayoutUsize.advance t bytes stride)
+
 def try_nonzero_spec_contract (si : layout.SizeInfo Usize)
     (run : Result (Option (layout.SizeInfo NonZeroUsize))) : Prop :=
   sizeInfoValid si → run ⦃ r => (∀ next ∈ r, sizeInfoValid next) ∧
@@ -309,6 +334,20 @@ def requires_static_padding_spec : Prop :=
   ∀ (self : layout.DstLayout),
     requires_static_padding_spec_contract self (layout.DstLayout.requires_static_padding self)
 
+def requires_dynamic_padding_spec_contract (self : layout.DstLayout)
+    (run : Result Bool) : Prop :=
+  layoutValid self →
+    ∃ r, run = .ok r ∧
+      (r = false ↔ match self.size_info with
+        | .Sized _ => True
+        | .SliceDst t => (trailingFormula t).size 0 = t.offset.val ∧
+          t.elem_size.val % (trailingFormula t).align = 0)
+
+def requires_dynamic_padding_spec : Prop :=
+  ∀ (self : layout.DstLayout),
+    requires_dynamic_padding_spec_contract self
+      (layout.DstLayout.requires_dynamic_padding self)
+
 
 end Zerocopy.Obligations
 

verification/aeneas/lean/Obligations/TailTransforms.lean

@@ -0,0 +1,58 @@
+/- 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
+
+/- These arbitrary-run contracts retain the full decoded machine-word domain.
+Their total True conclusions discharge the numerical assertions visible in
+Rust; the original natural-number method obligations remain independent.
+-/
+def tail_transformations_check_spec_contract
+    (tail : layout.TrailingSliceLayout Usize) (align : NonZeroUsize)
+    (phase bytes replacement_stride elems : Usize) (run : Result Unit) : Prop :=
+  0 < tail.size_rounding_align_and_phase._0.val.val → 0 < align.val.val →
+    run ⦃ _ => True ⦄
+
+def tail_transformations_check_spec : Prop :=
+  ∀ tail align phase bytes replacement_stride elems,
+    tail_transformations_check_spec_contract tail align phase bytes replacement_stride elems
+      (layout.tail_transform_checks.tail_transformations_check
+        tail align phase bytes replacement_stride elems)
+
+def tail_size_sequence_check_spec_contract
+    (left right : layout.TrailingSliceLayout Usize)
+    (left_align : NonZeroUsize) (left_phase : Usize)
+    (right_align : NonZeroUsize) (right_phase elems : Usize) (run : Result Unit) : Prop :=
+  0 < left.size_rounding_align_and_phase._0.val.val →
+    0 < right.size_rounding_align_and_phase._0.val.val →
+    0 < left_align.val.val → 0 < right_align.val.val → run ⦃ _ => True ⦄
+
+def tail_size_sequence_check_spec : Prop :=
+  ∀ left right left_align left_phase right_align right_phase elems,
+    tail_size_sequence_check_spec_contract left right left_align left_phase right_align right_phase elems
+      (layout.tail_transform_checks.tail_size_sequence_check
+        left right left_align left_phase right_align right_phase elems)
+
+def tail_dynamic_padding_check_spec_contract
+    (runtime_layout : layout.DstLayout) (align : NonZeroUsize) (phase : Usize)
+    (run : Result Unit) : Prop :=
+  layoutValid runtime_layout → 0 < align.val.val → run ⦃ _ => True ⦄
+
+def tail_dynamic_padding_check_spec : Prop :=
+  ∀ runtime_layout align phase,
+    tail_dynamic_padding_check_spec_contract runtime_layout align phase
+      (layout.tail_transform_checks.tail_dynamic_padding_check runtime_layout align phase)
+
+end Zerocopy.Obligations

verification/aeneas/lean/Proofs/Contracts.lean

@@ -131,6 +131,16 @@ theorem size_for_elems_spec : Zerocopy.Specs.size_for_elems_spec := by
   exact facts
 register_spec_step size_for_elems_spec
 
+/- Prove that a positive comparison implies equal sizes for all metadata. The
+negative branch deliberately promises no inequality between the sequences.
+-/
+theorem same_size_sequence_spec : Zerocopy.Specs.same_size_sequence_spec := by
+  unfold Zerocopy.Specs.same_size_sequence_spec
+  representation_simps
+  intro self other hs ho
+  exact Raw.same_size_sequence_spec self other hs ho
+register_spec_step same_size_sequence_spec
+
 theorem max_elems_for_bytes_spec : Zerocopy.Specs.max_elems_for_bytes_spec := by
   unfold Zerocopy.Specs.max_elems_for_bytes_spec
   representation_simps
@@ -203,11 +213,39 @@ theorem requires_static_padding_spec : Zerocopy.Specs.requires_static_padding_sp
   exact Raw.requires_static_padding_spec self
 register_spec_step requires_static_padding_spec
 
+theorem requires_dynamic_padding_spec : Zerocopy.Specs.requires_dynamic_padding_spec := by
+  unfold Zerocopy.Specs.requires_dynamic_padding_spec
+  representation_simps
+  intro self hv
+  apply Raw.requires_dynamic_padding_spec self
+  cases hs : self.size_info with
+  | Sized _ => trivial
+  | SliceDst _ => simpa only [hs] using hv.2
+register_spec_step requires_dynamic_padding_spec
+
 end Zerocopy.Proofs
 
 namespace Zerocopy.Proofs
 open AeneasSpecs
 
+/- Changing the byte origin must preserve the complete-size formula. Carry
+aligned bytes into base and keep the residual phase without losing physical
+offset.
+-/
+theorem advance_spec : Zerocopy.Specs.advance_spec := by
+  unfold Zerocopy.Specs.advance_spec
+  representation_simps
+  intro self bytes elem hv
+  apply WP.spec_mono (Raw.advance_spec self bytes elem hv)
+  rintro result ⟨accepted, facts⟩
+  refine ⟨?_, facts⟩
+  change isValid result
+  rw [option_valid_iff]
+  intro next member
+  rw [trailing_valid_iff]
+  exact ⟨by simp, accepted next member⟩
+register_spec_step advance_spec
+
 /- Explain both zero-stride rejection and successful conversion. The raw lemma
 retains broad representation coverage; the canonical spec adds recursive
 admission rather than silently changing that useful raw theorem.

verification/aeneas/lean/Proofs/Raw/Layout.lean

@@ -309,4 +309,101 @@ theorem theoretical_max_align_spec :
     ↓reduceDIte, ↓reduceIte, bind_ok, WP.spec_ok]
   exact hv
 
+theorem fill_low_bits (n k : Nat) : n ||| (2 ^ k - 1) = n - n % 2 ^ k + (2 ^ k - 1) := by
+  have h : (n - n % 2 ^ k) % 2 ^ k = 0 := by
+    rw [← Nat.div_mul_self_eq_mod_sub_self, Nat.mul_mod_left]
+  rw [← LayoutMath.aligned_or _ _ _ ⟨k, rfl⟩ h (by have := Nat.two_pow_pos k; omega)]
+  apply Nat.eq_of_testBit_eq
+  intro i
+  rw [Nat.testBit_or, Nat.testBit_or, Nat.testBit_two_pow_sub_one]
+  by_cases hi : i < k
+  · simp only [hi, decide_true, Bool.or_true]
+  · simp only [hi, decide_false, Bool.or_false]
+    rw [← Nat.div_mul_self_eq_mod_sub_self, ← Nat.shiftLeft_eq]
+    rw [Nat.testBit_shiftLeft]
+    rw [Nat.testBit_div_two_pow]
+    simp only [show k ≤ i by omega, decide_true, Bool.true_and,
+      show i - k + k = i by omega]
+
+/- Changing the byte origin must preserve the complete-size formula. Carry
+aligned bytes into base and keep the residual phase without losing physical
+offset.
+-/
+theorem advance_spec :
+  ∀ (self : layout.TrailingSliceLayout Usize) (bytes elem_size : Usize), ∀ (hn : (0 < self.size_rounding_align_and_phase._0.val.val : Prop)),
+    @Zerocopy.layout.TrailingSliceLayoutUsize.advance self bytes elem_size ⦃ result => (∀ t ∈ result, encodingValid t.size_rounding_align_and_phase) ∧ match result with
+    | none => Usize.max < ((trailingFormula self).advance bytes.val elem_size.val).base
+    | some t => trailingFormula t = (trailingFormula self).advance bytes.val elem_size.val ∧
+      ((trailingFormula self).advance bytes.val elem_size.val).base ≤ Usize.max ⦄ := by
+  intro self bytes elem hn
+  unfold layout.TrailingSliceLayoutUsize.advance
+  step with encoding_components_spec _ hn as ⟨a, p, ha, hp, hsum, halign, hphase⟩
+  have hv := trailing_view self a.val.val p.val ha hp hsum.symm
+  have apos := Nat.pos_of_isPowerOfTwo ha
+  simp only [core.num.nonzero.NonZero.get, bind_ok]
+  step with Usize.sub_spec (show (1#usize).val ≤ a.val.val by simpa using (show 1 ≤ a.val.val by omega)) as ⟨mask, hm, _⟩
+  step with Usize.sub_spec (show self.size_base.val ≤ core.num.Usize.MAX.val by scalar_tac) as ⟨available, hav, _⟩
+  let pc := available ||| mask
+  have hpc : pc.val = (Usize.max - self.size_base.val) -
+      (Usize.max - self.size_base.val) % a.val.val + (a.val.val - 1) := by
+    obtain ⟨k, hk⟩ := ha
+    rw [UScalar.val_or, hm, hav]
+    rw [hk, fill_low_bits]
+  have hpbound : p.val ≤ pc.val := by
+    have hor : mask.val ≤ pc.val := by
+      rw [UScalar.val_or]
+      exact Nat.right_le_or
+    omega
+  simp only [lift, bind_ok]
+  step with Usize.sub_spec hpbound as ⟨advance, hadv, _⟩
+  dsimp only [pc] at *
+  simp only [UScalar.lt_equiv]
+  split
+  · rename_i hlarge
+    simp only [WP.spec_ok, hv, LayoutMath.Formula.advance]
+    constructor
+    · simp
+    · have hcap := LayoutMath.floor_capacity (p.val + bytes.val)
+        (Usize.max - self.size_base.val) a.val.val apos
+      have hbase : self.size_base.val ≤ Usize.max := by scalar_tac
+      have hrem := Nat.mod_le (p.val + bytes.val) a.val.val
+      omega
+  · rename_i hsmall
+    have hshift : p.val + bytes.val ≤ (available ||| mask).val := by omega
+    have hword : (available ||| mask).val ≤ Usize.max := by
+      have h := UScalar.hSize (available ||| mask)
+      simp only [UScalar.size, Usize.max, Usize.numBits, UScalarTy.Usize_numBits_eq] at h ⊢
+      have := Nat.two_pow_pos System.Platform.numBits
+      omega
+    step with Usize.add_spec (x := p) (y := bytes) (by omega) as ⟨shifted, hshifted⟩
+    have hlow : (shifted &&& mask).val = shifted.val % a.val.val := by
+      obtain ⟨k, hk⟩ := ha
+      rw [UScalar.val_and, hm, hk, Nat.and_two_pow_sub_one_eq_mod]
+    step with round_down_spec shifted a ha as ⟨whole, _, hwhole, _, _, _⟩
+    have hbase : self.size_base.val + whole.val ≤ Usize.max := by
+      have hcap := (LayoutMath.floor_capacity (p.val + bytes.val)
+        (Usize.max - self.size_base.val) a.val.val apos).mpr (by omega)
+      rw [hwhole, hshifted]
+      have hb : self.size_base.val ≤ Usize.max := by scalar_tac
+      omega
+    step with Usize.add_spec (x := self.size_base) (y := whole) hbase as ⟨base, hb⟩
+    step with encoding_new_spec a (shifted &&& mask) ha (by rw [hlow]; exact Nat.mod_lt _ apos) as ⟨encoded, he⟩
+    have hnew := trailing_view
+      ({ self with elem_size := elem, size_base := base, size_rounding_align_and_phase := encoded })
+      a.val.val (shifted.val % a.val.val) ha (Nat.mod_lt _ apos) (by rw [he, hlow])
+    have hencoded : encodingValid encoded := by
+      unfold encodingValid
+      rw [he]
+      omega
+    simp only [hnew, hv, LayoutMath.Formula.advance]
+    refine ⟨?_, ?_, ?_⟩
+    · simpa using hencoded
+    · rw [hshifted, hb, hwhole, hshifted]
+      congr 1
+      have := Nat.mod_le (p.val + bytes.val) a.val.val
+      omega
+    · rw [hwhole, hshifted] at hbase
+      have := Nat.mod_le (p.val + bytes.val) a.val.val
+      omega
+
 end Zerocopy.Proofs.Raw