Specify rounding encodings as alignment and phase

verification/aeneas/README.md

@@ -341,6 +341,11 @@ The mathematical layout semantics proves normalization across arbitrary
 nesting and metadata values. These algebraic laws do not themselves verify
 a Rust layout method.
 
+The nominal rounding wrapper decodes to `RoundingValue`, a power-of-two
+alignment and bounded phase with machine-fit proofs. Ordinary representation
+laws establish acceptance of every positive stored word and exact reconstruction
+from that pair. Zero is rejected by the native NonZero child decoder.
+
 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/Funs.lean

@@ -650,6 +650,72 @@ def byteorder.verification.set_u32_be
       value n
   byteorder.U32.get byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder value1
 
+/-- [zerocopy::layout::POINTER_WIDTH_BITS]
+    Source: 'src/layout/mod.rs', lines 17:0-17:62 -/
+@[global_simps, irreducible]
+def layout.POINTER_WIDTH_BITS : Result Std.Usize := do
+  let i ← core.mem.size_of Std.Usize
+  i * 8#usize
+
+/-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::new]:
+    Source: 'src/layout/mod.rs', lines 97:4-116:5 -/
+def layout.RoundingAlignAndPhase.new
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) :
+  Result layout.RoundingAlignAndPhase
+  := do
+  let i ←
+    core.num.nonzero.NonZero.get
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
+  let b ← core.num.Usize.is_power_of_two i
+  massert b
+  massert (phase < i)
+  let encoded ← lift (i ||| phase)
+  let o ←
+    core.num.nonzero.NonZero.new
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner encoded
+  match o with
+  | none => fail panic
+  | some encoded1 => ok { _0 := encoded1 }
+
+/-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::components]:
+    Source: 'src/layout/mod.rs', lines 130:4-157:5 -/
+def layout.RoundingAlignAndPhase.components
+  (self : layout.RoundingAlignAndPhase) :
+  Result ((core.num.nonzero.NonZero Std.Usize
+    core.num.niche_types.NonZeroUsizeInner) × Std.Usize)
+  := do
+  let i ← layout.POINTER_WIDTH_BITS
+  let i1 ← i - 1#usize
+  let i2 ←
+    core.num.nonzero.NonZero.get
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner self._0
+  let i3 ← lift (core.num.Usize.leading_zeros i2)
+  let i4 ← lift (UScalar.cast .Usize i3)
+  let shift ← i1 - i4
+  let align ← 1#usize <<< shift
+  let o ←
+    core.num.nonzero.NonZero.new
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
+  match o with
+  | none => fail panic
+  | some align1 =>
+    let i5 ←
+      core.num.nonzero.NonZero.get
+        Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align1
+    let phase ← lift (i2 ^^^ i5)
+    ok (align1, phase)
+
+/-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::align]:
+    Source: 'src/layout/mod.rs', lines 170:4-179:5 -/
+def layout.RoundingAlignAndPhase.align
+  (self : layout.RoundingAlignAndPhase) :
+  Result (core.num.nonzero.NonZero Std.Usize
+    core.num.niche_types.NonZeroUsizeInner)
+  := do
+  let (nz, _) ← layout.RoundingAlignAndPhase.components self
+  ok nz
+
 /-- [zerocopy::FromZeros::new_zeroed]:
     Source: 'src/lib.rs', lines 3827:4-3833:5
     Visibility: public -/

verification/aeneas/golden/FunsExternal_Template.lean

@@ -35,6 +35,13 @@ open Zerocopy
 @[rust_fun "core::intrinsics::transmute"]
 axiom core.intrinsics.transmute {Src : Type} (Dst : Type) : Src → Result Dst
 
+/-- [core::mem::size_of]:
+    Source: '/rustc/library/core/src/mem/mod.rs', lines 375:0-375:34
+    Name pattern: [core::mem::size_of]
+    Visibility: public -/
+@[rust_fun "core::mem::size_of"]
+axiom core.mem.size_of (T : Type) : Result Std.Usize
+
 /-- [core::mem::zeroed]:
     Source: '/rustc/library/core/src/mem/mod.rs', lines 755:0-755:36
     Name pattern: [core::mem::zeroed]

verification/aeneas/golden/Types.lean

@@ -177,6 +177,12 @@ structure byteorder.F64 (O : Type) where
   _0 : Array Std.U8 8#usize
   _1 : core.marker.PhantomData O
 
+/-- [zerocopy::layout::RoundingAlignAndPhase]
+    Source: 'src/layout/mod.rs', lines 78:0-78:54 -/
+structure layout.RoundingAlignAndPhase where
+  _0 : core.num.nonzero.NonZero Std.Usize
+    core.num.niche_types.NonZeroUsizeInner
+
 /-- [zerocopy::wrappers::read_only_def::ReadOnly]
     Source: 'src/wrappers.rs', lines 630:4-634:5
     Visibility: public -/

verification/aeneas/lean/LayoutModel.lean

@@ -0,0 +1,29 @@
+/- 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 Zerocopy.Funs
+public import SpecPrelude
+public import LayoutMath
+@[expose] public section
+
+/-!
+Extracted trailing records contain machine words and compressed rounding
+encodings. This module interprets those records as an unbounded complete-size
+formula and a separately observed physical slice offset. Its definitions do
+not call an extracted operation or assume that an operation is correct.
+
+Keeping physical offset separate from normalized base and phase is essential:
+inner padding can make them differ. Operation proofs use these observations
+to connect extracted arithmetic with the independent layout mathematics.
+-/
+open Aeneas Aeneas.Std
+namespace Zerocopy.Proofs
+
+
+end Zerocopy.Proofs

verification/aeneas/lean/MathViews.lean

@@ -34,6 +34,9 @@ set_option linter.unusedSimpArgs false
 -- Raw observations remain available independently of function contracts.
 -- They record the full positive encoding domain, including arbitrary stored
 -- words, and do not register a separately selectable validity interpretation.
+def encodingValid (code : layout.RoundingAlignAndPhase) : Prop :=
+  0 < code._0.val.val
+
 @[contract_simps] theorem admission_eq {Raw : Type u} (provider : RustModel Raw)
     (raw : Raw) : (∃ value, provider.decode raw = some value) =
       @isValid Raw provider raw := rfl
@@ -68,12 +71,22 @@ set_option linter.unusedSimpArgs false
 @[simp, contract_simps] theorem bool_valid_iff (x : Bool) : isValid x ↔ True := by
   simp [isValid, RustModel.decode, modelBool]
 
+@[simp, contract_simps] theorem encoding_valid_iff (code : layout.RoundingAlignAndPhase) :
+    isValid code ↔ encodingValid code := by
+  by_cases hp : 0 < code._0.val.val <;>
+    simp [isValid, RustModel.decode, layout.RoundingAlignAndPhase.aeneasModel,
+      layout.RoundingAlignAndPhase.decode, layout.RoundingAlignAndPhase.decodeFields,
+      modelNonZeroUScalar, hp, encodingValid]
+
 @[contract_simps] theorem scalar_admitted_iff (x : UScalar ty) :
     (∃ value, RustModel.decode x = some value) ↔ True := scalar_valid_iff x
 
 @[contract_simps] theorem nonzero_admitted_iff (x : NonZeroUsize) :
     (∃ value, RustModel.decode x = some value) ↔ 0 < x.val.val := nonzero_valid_iff x
 
+@[contract_simps] theorem encoding_admitted_iff (x : layout.RoundingAlignAndPhase) :
+    (∃ value, RustModel.decode x = some value) ↔ encodingValid x := encoding_valid_iff x
+
 @[contract_simps] theorem bool_admitted_iff (x : Bool) :
     (∃ value, RustModel.decode x = some value) ↔ True := bool_valid_iff x
 
@@ -86,11 +99,20 @@ set_option linter.unusedSimpArgs false
 
 -- A named decoder can also occur after a surrounding structural traversal
 -- exposes the retained dictionary. These are the same admission equivalences.
+@[contract_simps] theorem encoding_decoder_admitted_iff (raw : layout.RoundingAlignAndPhase) :
+    (∃ value, layout.RoundingAlignAndPhase.decode raw = some value) ↔
+      encodingValid raw := encoding_valid_iff raw
+
 @[contract_simps] theorem normalized_nat_pos_iff (n : Nat) :
     Nat.le (Nat.succ 0) n ↔ 0 < n := Nat.succ_le_iff
 
 attribute [contract_simps] option_valid_iff prod_valid_iff result_valid_iff
 
 attribute [contract_simps] and_true true_and and_self true_implies forall_true_iff
+attribute [contract_simps] encodingValid
+
+@[simp, contract_simps] theorem rounding_model_decode_eq
+    (raw : layout.RoundingAlignAndPhase) :
+    RustModel.decode raw = layout.RoundingAlignAndPhase.decode raw := rfl
 
 end Zerocopy.Proofs

verification/aeneas/lean/ModelSupport.lean

@@ -0,0 +1,56 @@
+/- 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 ModelShapes
+import all Mathlib.Data.Nat.Log
+import all Init.Data.Nat.Power2.Basic
+@[expose] public section
+
+/-!
+The inline rounding decoder constructs a constrained alignment/phase pair.
+These ordinary arithmetic lemmas explain why a positive word has the required
+components, and why those components are unique. This module imports model
+shapes rather than full providers, so it can be available while decoders are
+being elaborated. It supplies reusable facts, not a separate certification
+duty that every mathematical model must satisfy.
+-/
+open Aeneas Aeneas.Std AeneasSpecs
+
+namespace Zerocopy.RoundingFacts
+
+/-- A positive word has a unique highest power-of-two bit. -/
+theorem bounds (word : Nat) (positive : 0 < word) :
+    2 ^ Nat.log2 word ≤ word ∧ word < 2 ^ (Nat.log2 word + 1) :=
+  (Nat.log2_eq_iff (by omega)).mp rfl
+
+theorem reconstruction (word : Nat) (positive : 0 < word) :
+    2 ^ Nat.log2 word + (word - 2 ^ Nat.log2 word) = word := by
+  have := bounds word positive
+  omega
+
+/-- These are the exact components of every positive encoding, not a restricted
+constructor-only subset of the representation domain. -/
+theorem components_unique (word align phase : Nat)
+    (pow2 : align.isPowerOfTwo) (phase_lt : phase < align)
+    (encoding : word = align + phase) :
+    align = 2 ^ Nat.log2 word ∧ phase = word - 2 ^ Nat.log2 word := by
+  obtain ⟨k, rfl⟩ := pow2
+  have positive : 0 < word := by have := Nat.two_pow_pos k; omega
+  have hk : Nat.log2 word = k :=
+    (Nat.log2_eq_iff (by omega)).mpr (by rw [Nat.pow_succ]; omega)
+  rw [hk]
+  omega
+
+/-- Proof irrelevance makes equality depend only on the observed pair. -/
+@[ext] theorem value_ext
+    {a b : layout.RoundingAlignAndPhase.RoundingValue}
+    (ha : a.align = b.align) (hp : a.phase = b.phase) : a = b := by
+  cases a; cases b; simp_all
+
+end Zerocopy.RoundingFacts

verification/aeneas/lean/Obligations.lean

@@ -11,6 +11,7 @@ public import Zerocopy.Funs
 public import SpecPrelude
 public import MathViews
 public import Arithmetic
+public import LayoutModel
 @[expose] public section
 
 /-!
@@ -77,6 +78,35 @@ def round_down_spec : Prop :=
   ∀ (n : Usize) (align : NonZeroUsize),
     round_down_spec_contract n align (util.round_down_to_next_multiple_of_alignment n align)
 
+def encoding_new_spec_contract (a : NonZeroUsize) (p : Usize)
+    (run : Result layout.RoundingAlignAndPhase) : Prop :=
+  0 < a.val.val → a.val.val.isPowerOfTwo → p.val < a.val.val →
+    ∃ code, run = .ok code ∧ encodingValid code ∧ code._0.val.val = a.val.val + p.val
+
+def encoding_new_spec : Prop :=
+  ∀ (a : NonZeroUsize) (p : Usize),
+    encoding_new_spec_contract a p (layout.RoundingAlignAndPhase.new a p)
+
+def encoding_components_spec_contract (code : layout.RoundingAlignAndPhase)
+    (run : Result (NonZeroUsize × Usize)) : Prop :=
+  0 < code._0.val.val →
+    run ⦃ (a, p) =>
+      0 < a.val.val ∧ a.val.val.isPowerOfTwo ∧ p.val < a.val.val ∧ a.val.val + p.val = code._0.val.val ∧
+      a.val.val = 2 ^ code._0.val.val.log2 ∧ p.val = code._0.val.val - 2 ^ code._0.val.val.log2 ⦄
+
+def encoding_components_spec : Prop :=
+  ∀ (code : layout.RoundingAlignAndPhase),
+    encoding_components_spec_contract code (layout.RoundingAlignAndPhase.components code)
+
+def encoding_align_spec_contract (code : layout.RoundingAlignAndPhase)
+    (run : Result NonZeroUsize) : Prop :=
+  0 < code._0.val.val →
+    ∃ a, run = .ok a ∧ 0 < a.val.val ∧ a.val.val = 2 ^ code._0.val.val.log2
+
+def encoding_align_spec : Prop :=
+  ∀ (code : layout.RoundingAlignAndPhase),
+    encoding_align_spec_contract code (layout.RoundingAlignAndPhase.align code)
+
 
 end Zerocopy.Obligations
 

verification/aeneas/lean/Proofs.lean

@@ -7,40 +7,27 @@ This file may not be copied, modified, or distributed except according to
 those terms. -/
 
 module
-public import Specs
+public import Proofs.Contracts
 public import Proofs.Util
-public import Aeneas
-public import Loops
-public import LayoutMath
-import all Mathlib.Data.Nat.Log
-import all Init.Data.Nat.Power2.Basic
 @[expose] public section
 
 /-!
-This is the import root for contracts proved about actual Aeneas function
-definitions. Proofs.Util supplies the arithmetic theorems: its Raw namespace
-steps through the extracted computations, then canonical theorems prove the
-generated Specs propositions, including input and result decoding.
+This module proves contracts about the actual Aeneas function definitions.
+The Raw namespace steps through extracted control flow and machine
+arithmetic. Those lemmas deliberately retain useful representation domains,
+even when an inline specification admits a smaller domain through automatic
+decoding.
+
+The canonical theorems outside Raw prove the generated Specs propositions.
+They use the raw lemmas, decode accepted inputs, and establish that the
+actual returned representation decodes and has the requested mathematical
+properties. WP.spec_mono transfers a proved computation to a new
+postcondition; it cannot replace that computation. Registered specifications
+let later proofs reuse a callee's theorem instead of unfolding its
+implementation each time.
 
 Aeneas Result describes execution success, panic, or divergence. Rust Option
-and Rust Result values may themselves be successful payloads. These cases
-have different meanings and must remain distinct in function contracts.
+and Rust Result values may themselves be successful payloads. The proof must
+keep these cases distinct.
 -/
 open Aeneas Aeneas.Std
-namespace Zerocopy.Proofs.Raw
-
-set_option linter.unusedVariables false
-
-
-end Zerocopy.Proofs.Raw
-
-namespace Zerocopy.Proofs
-open AeneasSpecs
-
-
-end Zerocopy.Proofs
-
-namespace Zerocopy.Proofs
-open AeneasSpecs
-
-end Zerocopy.Proofs