Model alignment and phase encoding as a bounded mathematical pair

verification/aeneas/README.md

@@ -68,8 +68,9 @@ each tool answers a different question:
 
 The extracted model and the mathematical model have different purposes. The
 first represents the computation we prove properties about; the second supplies
-the vocabulary in which we state those properties. For example, a Rust nonzero word
-is interpreted as a natural number with machine bounds and a proof of positivity. Plain clauses use mathematical values; `(raw)`
+the vocabulary in which we state those properties. For example, Rust stores
+rounding alignment and phase in one nonzero word, while its mathematical model
+exposes two natural numbers. Plain clauses use mathematical values; `(raw)`
 clauses use extracted representations. Both execute the same extracted function
 on its original arguments and require the actual returned value to decode.
 
@@ -134,6 +135,7 @@ added without extending the specification set.
 | `min` | Returns the mathematical minimum, selects an input, and bounds both inputs from below. |
 | `padding_needed_for` | For power-of-two alignment, returns padding below it and exactly `(align - len % align) % align`, the least padding making the sum aligned, with zero padding exactly when the input is aligned. |
 | `round_down_to_next_multiple_of_alignment` | For power-of-two alignment, returns exactly `n - n % align`, the greatest aligned value at most `n`; the next multiple exceeds `n`. |
+| Alignment/phase encoder and decoders | Power-of-two alignment, bounded phase, and exact encoding round-trip. |
 
 Every registered function uses total `spec`: accepted raw representations,
 supplied mathematical ghosts, and explicit requirements imply successful
@@ -151,6 +153,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 NonZero positivity. Their Nat/Int arithmetic does not wrap; explicit raw
 clauses preserve the extracted representation vocabulary while retaining
@@ -336,7 +343,7 @@ comparison is part of the automatic-decoding audit.
 Generated modules follow the proof-construction dependency:
 
 ```text
-raw Types + ModelPrelude → ModelShapes → Models → Specs + Proofs
+raw Types + ModelPrelude → ModelShapes → ModelSupport → Models → Specs + Proofs
 ```
 
 `ModelShapes` declares nominal mathematical fields and inline model types in
@@ -472,14 +479,17 @@ modules must not create import cycles through generated `Required` or `Check`.
 Model fields declare ordinary Lean constraints. A decoder can supply only its
 data and use native `..` to omit proof fields:
 
-For a hypothetical type with a machine-word field `word`:
-
 ```lean
-model SuccessorValue where
-  value : Nat
-  positive : 0 < value
+model RoundingValue where
+  align : Nat
+  phase : Nat
+  align_pow2 : align.isPowerOfTwo
+  phase_lt : phase < align
+  fits : align + phase ≤ Usize.max
 decode self =>
-  { value := self.word.value + 1, .. }
+  let word := self._0.value
+  let align := 2 ^ Nat.log2 word
+  { align := align, phase := word - align, .. }
 ```
 
 Both `decode` and `decode?` implicitly use `model_value` completion on the whole
@@ -560,7 +570,7 @@ After a Lake build, inspect an effective compiled specification with:
 
 ```sh
 python3 -B verification/aeneas/workspace.py inspect verification/aeneas/lean \
-  --root "$PWD" --spec max_spec
+  --root "$PWD" --spec encoding_components_spec
 ```
 
 This reads compiled declarations without running another build. It displays the

verification/aeneas/golden/Funs.lean

@@ -642,6 +642,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::util::round_down_to_next_multiple_of_alignment]:
     Source: 'src/util/mod.rs', lines 261:0-279:1 -/
 def util.round_down_to_next_multiple_of_alignment

verification/aeneas/golden/FunsExternal_Template.lean

@@ -28,6 +28,13 @@ set_option maxHeartbeats 1000000
 set_option maxRecDepth 2048
 open Zerocopy
 
+/-- [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::num::niche_types::{impl core::clone::Clone for core::num::niche_types::NonZeroUsizeInner}::clone]:
     Source: '/rustc/library/core/src/num/niche_types.rs', lines 17:17-17:22
     Name pattern: [core::num::niche_types::{core::clone::Clone<core::num::niche_types::NonZeroUsizeInner>}::clone]
@@ -39,6 +46,17 @@ axiom core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone
   core.num.niche_types.NonZeroUsizeInner → Result
     core.num.niche_types.NonZeroUsizeInner
 
+/-- [core::num::nonzero::{core::num::nonzero::NonZero<T, Clause0_NonZeroInner>}::new]:
+    Source: '/rustc/library/core/src/num/nonzero.rs', lines 388:4-388:42
+    Name pattern: [core::num::nonzero::{core::num::nonzero::NonZero<@T, @Clause0_NonZeroInner>}::new]
+    Visibility: public -/
+@[rust_fun
+  "core::num::nonzero::{core::num::nonzero::NonZero<@T, @Clause0_NonZeroInner>}::new"]
+axiom core.num.nonzero.NonZero.new
+  {T : Type} {Clause0_NonZeroInner : Type} (ZeroablePrimitiveInst :
+  core.num.nonzero.ZeroablePrimitive T Clause0_NonZeroInner) :
+  T → Result (Option (core.num.nonzero.NonZero T Clause0_NonZeroInner))
+
 /-- [core::num::nonzero::{core::num::nonzero::NonZero<T, Clause0_NonZeroInner>}::get]:
     Source: '/rustc/library/core/src/num/nonzero.rs', lines 467:4-467:31
     Name pattern: [core::num::nonzero::{core::num::nonzero::NonZero<@T, @Clause0_NonZeroInner>}::get]

verification/aeneas/golden/Types.lean

@@ -99,4 +99,10 @@ structure byteorder.U32 (O : Type) where
   _0 : Array Std.U8 4#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
+
 end Zerocopy

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