Prove and consume the Unaligned alignment law

verification/aeneas/ADMISSION_DESIGN.md

@@ -46,6 +46,16 @@ normalization must not lose a guarded call. Pinned builtin mapping and backend
 semantics remain trusted correspondence premises, rather than a translation
 certificate established by the report.
 
+The `Unaligned` trial admits only the standard-library `NonZeroUsize`
+constructor boundary. Before and after lowering, admission checks its exact
+unsafe signature and original `usize` instantiation. The native model guards
+zero before constructing a wrapper and leaves it forbidden even if discarded.
+The generic caller's extracted alignment read and both checked divisions remain
+visible; its exact trait law establishes alignment one and the nonzero argument.
+Kernel controls reject zero under total and partial `True` contracts and show
+that an alignment-two model cannot establish either execution contract without
+the law. No body of the new Rust caller is made opaque.
+
 The production `IntoBytes` methods delegate their write selection to
 `util::bytewrite::{exact,prefix,suffix}`. Their contracts prove exact byte
 contents, preservation of untouched destination regions, and unchanged

verification/aeneas/DESIGN.md

@@ -329,7 +329,8 @@ the library already models every part of Rust's abstract machine.
   const generics, associated-type trait laws, higher-ranked bounds, bounded
   nominal models, and escaping borrow reconstruction remain unsupported with
   explicit errors. The first trait-law bridge supports `Self`-only traits and
-  simple generic bounds, with a total byte codec as a checked example. Add semantics and admission checks before accepting
+  simple generic bounds, with `Unaligned` and a total byte codec as checked
+  examples. Add semantics and admission checks before accepting
   them. Stateful or nondeterministic APIs may need observable traces and
   effects, rather than only result contracts.
 - **Abstract storage and bit validity.** Check byte-to-value production before

verification/aeneas/SEMANTICS.md

@@ -82,9 +82,14 @@ not to replace the universal algebra proof.
 ## External inputs and trust
 
 Aeneas erases ABI layout information from generic Rust type parameters.
-`Zerocopy.RustLayout.size` and `Zerocopy.RustLayout.align` are therefore
+`Zerocopy.RustLayout.size` and `Zerocopy.RustLayout.alignInput` are
 uninterpreted **data inputs**, each of type `Type → Usize`. No proposition
-about their values is an axiom. The constructors' contracts explicitly
+about their values is an axiom. `RustLayout.align` uses alignment one for the
+concrete byte carrier `U8` and the abstract alignment input for every other
+carrier. That byte interpretation is an explicit compiler-correspondence
+premise, checked by a Rust compile-time assertion. It allows the concrete
+`u8: Unaligned` dictionary to discharge its trait law without assuming that
+all types have alignment one. The constructors' contracts explicitly
 require the relevant primitive reads and alignment properties. The audit
 admits exactly these two names and verifies their signatures. Changing an
 input to a proposition, or adding another axiom, fails the audit.

verification/aeneas/external.json

@@ -5,6 +5,7 @@
   {"rust": "core::num::{usize}::checked_mul", "signature": {"unsafe": false, "inputs": ["usize", "usize"], "output": "core::option::Option<usize>", "types": 0, "consts": 0}, "lean": "Usize.checked_mul"},
   {"rust": "core::num::nonzero::{core::num::nonzero::NonZero<T0,T1>}::get", "signature": {"unsafe": false, "inputs": ["core::num::nonzero::NonZero<T0,T1>"], "output": "T0", "types": 2, "consts": 0}, "lean": "core.num.nonzero.NonZero.get", "before": {"rust": "core::num::nonzero::{core::num::nonzero::NonZero<T0>}::get", "signature": {"unsafe": false, "inputs": ["core::num::nonzero::NonZero<T0>"], "output": "T0", "types": 1, "consts": 0}}},
   {"rust": "core::num::nonzero::{core::num::nonzero::NonZero<T0,T1>}::new", "signature": {"unsafe": false, "inputs": ["T0"], "output": "core::option::Option<core::num::nonzero::NonZero<T0,T1>>", "types": 2, "consts": 0}, "lean": "core.num.nonzero.NonZero.new", "before": {"rust": "core::num::nonzero::{core::num::nonzero::NonZero<T0>}::new", "signature": {"unsafe": false, "inputs": ["T0"], "output": "core::option::Option<core::num::nonzero::NonZero<T0>>", "types": 1, "consts": 0}}},
+  {"rust": "core::num::nonzero::{core::num::nonzero::NonZero<T0,T1>}::new_unchecked", "signature": {"unsafe": true, "inputs": ["T0"], "output": "core::num::nonzero::NonZero<T0,T1>", "types": 2, "consts": 0}, "lean": "core.num.nonzero.NonZero.new_unchecked", "before": {"rust": "core::num::nonzero::{core::num::nonzero::NonZero<T0>}::new_unchecked", "signature": {"unsafe": true, "inputs": ["T0"], "output": "core::num::nonzero::NonZero<T0>", "types": 1, "consts": 0}}},
   {"rust": "core::num::{usize}::checked_sub", "signature": {"unsafe": false, "inputs": ["usize", "usize"], "output": "core::option::Option<usize>", "types": 0, "consts": 0}, "lean": "Usize.checked_sub"},
   {"rust": "core::fmt::{core::fmt::Arguments}::from_str", "signature": {"unsafe": false, "inputs": ["&str"], "output": "core::fmt::Arguments", "types": 0, "consts": 0}, "lean": "core.fmt.Arguments.from_str"},
   {"rust": "core::slice::{[T0]}::len", "signature": {"unsafe": false, "inputs": ["&[T0]"], "output": "usize", "types": 1, "consts": 0}, "lean": "Slice.len"},

verification/aeneas/golden/Funs.lean

@@ -1077,20 +1077,83 @@ def layout.primitive_checks.check_empty_layout
 native_models def FromZeros.new_zeroed.default (Self : Type) : Result Self := do
   core.mem.zeroed Self
 
+/-- [zerocopy::trait_checks::unaligned_alignment]:
+    Source: 'src/trait_checks.rs', lines 25:0-27:1 -/
+def trait_checks.unaligned_alignment
+  {T : Type} (UnalignedInst : Unaligned T) : Result Std.Usize := do
+  core.mem.align_of T
+
+/-- [zerocopy::trait_checks::check_unaligned]:
+    Source: 'src/trait_checks.rs', lines 35:0-37:1 -/
+def trait_checks.check_unaligned
+  {T : Type} (UnalignedInst : Unaligned T) : Result Unit := do
+  let i ← trait_checks.unaligned_alignment UnalignedInst
+  massert (i = 1#usize)
+
+/-- [zerocopy::trait_checks::unused_unaligned_bound]:
+    Source: 'src/trait_checks.rs', lines 48:0-50:1 -/
+def trait_checks.unused_unaligned_bound
+  {T : Type} (UnalignedInst : Unaligned T) (value : Std.Usize) :
+  Result Std.Usize
+  := do
+  ok value
+
+/-- [zerocopy::impls::_#1::{impl zerocopy::Unaligned for u8}::only_derive_is_allowed_to_implement_this_trait]:
+    Source: 'src/util/macros.rs', lines 165:8-165:62
+    Visibility: public -/
+def U8.Insts.ZerocopyUnaligned.only_derive_is_allowed_to_implement_this_trait
+  : Result Unit := do
+  ok ()
+
+/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::Unaligned for u8}]
+    Source: 'src/util/macros.rs', lines 30:8-32:9 -/
+@[reducible]
+def U8.Insts.ZerocopyUnaligned : Unaligned Std.U8 := {
+  only_derive_is_allowed_to_implement_this_trait :=
+    U8.Insts.ZerocopyUnaligned.only_derive_is_allowed_to_implement_this_trait
+}
+
+/-- [zerocopy::trait_checks::check_byte_unaligned]:
+    Source: 'src/trait_checks.rs', lines 58:0-60:1 -/
+def trait_checks.check_byte_unaligned : Result Unit := do
+  trait_checks.check_unaligned U8.Insts.ZerocopyUnaligned
+
+/-- [zerocopy::trait_checks::divide_by_unaligned]:
+    Source: 'src/trait_checks.rs', lines 71:0-78:1 -/
+def trait_checks.divide_by_unaligned
+  {T : Type} (UnalignedInst : Unaligned T) (x : Std.Usize) :
+  Result Std.Usize
+  := do
+  let i ← core.mem.align_of T
+  let divisor ← 1#usize / i
+  let divisor1 ←
+    core.num.nonzero.NonZero.new_unchecked
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner divisor
+  let i1 ←
+    core.num.nonzero.NonZero.get
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner divisor1
+  x / i1
+
+/-- [zerocopy::trait_checks::divide_by_byte_alignment]:
+    Source: 'src/trait_checks.rs', lines 86:0-88:1 -/
+def trait_checks.divide_by_byte_alignment
+  (x : Std.Usize) : Result Std.Usize := do
+  trait_checks.divide_by_unaligned U8.Insts.ZerocopyUnaligned x
+
 /-- [zerocopy::trait_checks::{impl zerocopy::trait_checks::ByteCodec for zerocopy::trait_checks::XorCodec}::decode]:
-    Source: 'src/trait_checks.rs', lines 41:4-43:5 -/
+    Source: 'src/trait_checks.rs', lines 112:4-114:5 -/
 def trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec.decode
   (byte : Std.U8) : Result Std.U8 := do
   ok (byte ^^^ 170#u8)
 
 /-- [zerocopy::trait_checks::{impl zerocopy::trait_checks::ByteCodec for zerocopy::trait_checks::XorCodec}::encode]:
-    Source: 'src/trait_checks.rs', lines 37:4-39:5 -/
+    Source: 'src/trait_checks.rs', lines 108:4-110:5 -/
 def trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec.encode
   (byte : Std.U8) : Result Std.U8 := do
   ok (byte ^^^ 170#u8)
 
 /-- Trait implementation: [zerocopy::trait_checks::{impl zerocopy::trait_checks::ByteCodec for zerocopy::trait_checks::XorCodec}]
-    Source: 'src/trait_checks.rs', lines 36:0-44:1 -/
+    Source: 'src/trait_checks.rs', lines 107:0-115:1 -/
 @[reducible]
 def trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec :
   trait_checks.ByteCodec trait_checks.XorCodec := {
@@ -1099,23 +1162,23 @@ def trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec :
 }
 
 /-- [zerocopy::trait_checks::{impl zerocopy::trait_checks::ByteCodec for zerocopy::trait_checks::Forward<C>}::decode]:
-    Source: 'src/trait_checks.rs', lines 54:4-56:5 -/
+    Source: 'src/trait_checks.rs', lines 125:4-127:5 -/
 def trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec.decode
   {C : Type} (ByteCodecInst : trait_checks.ByteCodec C) (byte : Std.U8) :
   Result Std.U8
   := do
   ByteCodecInst.decode byte
 
 /-- [zerocopy::trait_checks::{impl zerocopy::trait_checks::ByteCodec for zerocopy::trait_checks::Forward<C>}::encode]:
-    Source: 'src/trait_checks.rs', lines 50:4-52:5 -/
+    Source: 'src/trait_checks.rs', lines 121:4-123:5 -/
 def trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec.encode
   {C : Type} (ByteCodecInst : trait_checks.ByteCodec C) (byte : Std.U8) :
   Result Std.U8
   := do
   ByteCodecInst.encode byte
 
 /-- Trait implementation: [zerocopy::trait_checks::{impl zerocopy::trait_checks::ByteCodec for zerocopy::trait_checks::Forward<C>}]
-    Source: 'src/trait_checks.rs', lines 49:0-57:1 -/
+    Source: 'src/trait_checks.rs', lines 120:0-128:1 -/
 @[reducible]
 def trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec {C : Type}
   (ByteCodecInst : trait_checks.ByteCodec C) : trait_checks.ByteCodec
@@ -1127,7 +1190,7 @@ def trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec {C : Type}
 }
 
 /-- [zerocopy::trait_checks::byte_codec_roundtrip]:
-    Source: 'src/trait_checks.rs', lines 63:0-65:1 -/
+    Source: 'src/trait_checks.rs', lines 134:0-136:1 -/
 def trait_checks.byte_codec_roundtrip
   {C : Type} (ByteCodecInst : trait_checks.ByteCodec C) (byte : Std.U8) :
   Result Std.U8
@@ -1136,14 +1199,14 @@ def trait_checks.byte_codec_roundtrip
   ByteCodecInst.decode i
 
 /-- [zerocopy::trait_checks::forwarded_byte_codec]:
-    Source: 'src/trait_checks.rs', lines 73:0-75:1 -/
+    Source: 'src/trait_checks.rs', lines 144:0-146:1 -/
 def trait_checks.forwarded_byte_codec (byte : Std.U8) : Result Std.U8 := do
   trait_checks.byte_codec_roundtrip
     (trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec
     trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec) byte
 
 /-- [zerocopy::trait_checks::require_into_bytes]:
-    Source: 'src/trait_checks.rs', lines 77:0-77:47 -/
+    Source: 'src/trait_checks.rs', lines 148:0-148:47 -/
 def trait_checks.require_into_bytes
   {T : Type} (IntoBytesInst : IntoBytes T) : Result Unit := do
   ok ()
@@ -1213,7 +1276,7 @@ def Tuple.Insts.ZerocopyIntoBytes : IntoBytes Unit := {
 }
 
 /-- [zerocopy::trait_checks::check_array_into_bytes]:
-    Source: 'src/trait_checks.rs', lines 92:0-98:1 -/
+    Source: 'src/trait_checks.rs', lines 163:0-169:1 -/
 def trait_checks.check_array_into_bytes : Result Unit := do
   trait_checks.require_into_bytes (Array.Insts.ZerocopyIntoBytes 3#usize
     Bool.Insts.ZerocopyIntoBytes)

verification/aeneas/golden/FunsExternal_Template.lean

@@ -77,6 +77,17 @@ axiom core.num.nonzero.NonZero.new
   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>}::new_unchecked]:
+    Source: '/rustc/library/core/src/num/nonzero.rs', lines 405:4-405:51
+    Name pattern: [core::num::nonzero::{core::num::nonzero::NonZero<@T, @Clause0_NonZeroInner>}::new_unchecked]
+    Visibility: public -/
+@[rust_fun
+  "core::num::nonzero::{core::num::nonzero::NonZero<@T, @Clause0_NonZeroInner>}::new_unchecked"]
+axiom core.num.nonzero.NonZero.new_unchecked
+  {T : Type} {Clause0_NonZeroInner : Type} (ZeroablePrimitiveInst :
+  core.num.nonzero.ZeroablePrimitive T Clause0_NonZeroInner) :
+  T → Result (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

@@ -303,18 +303,24 @@ structure FromBytes (Self : Type) where
 structure IntoBytes (Self : Type) where
   only_derive_is_allowed_to_implement_this_trait : Result Unit
 
+/-- Trait declaration: [zerocopy::Unaligned]
+    Source: 'src/lib.rs', lines 6564:0-6571:1
+    Visibility: public -/
+structure Unaligned (Self : Type) where
+  only_derive_is_allowed_to_implement_this_trait : Result Unit
+
 /-- Trait declaration: [zerocopy::trait_checks::ByteCodec]
-    Source: 'src/trait_checks.rs', lines 26:0-29:1 -/
+    Source: 'src/trait_checks.rs', lines 97:0-100:1 -/
 structure trait_checks.ByteCodec (Self : Type) where
   encode : Std.U8 → Result Std.U8
   decode : Std.U8 → Result Std.U8
 
 /-- [zerocopy::trait_checks::XorCodec]
-    Source: 'src/trait_checks.rs', lines 31:0-31:16 -/
+    Source: 'src/trait_checks.rs', lines 102:0-102:16 -/
 structure trait_checks.XorCodec where
 
 /-- [zerocopy::trait_checks::Forward]
-    Source: 'src/trait_checks.rs', lines 47:0-47:34 -/
+    Source: 'src/trait_checks.rs', lines 118:0-118:34 -/
 structure trait_checks.Forward (C : Type) where
   _0 : core.marker.PhantomData C
 

verification/aeneas/lean/NonZeroSafetyTests.lean

@@ -0,0 +1,70 @@
+/- 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 SpecsSyntax
+public import Zerocopy.Funs
+@[expose] public section
+open Aeneas Aeneas.Std AeneasSpecs Zerocopy
+namespace NonZeroSafetyTests
+
+-- These are model executions, not attempts to execute undefined Rust.
+noncomputable def zeroConstructor :=
+  core.num.nonzero.NonZero.new_unchecked
+    Zerocopy.Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner (0#usize)
+
+theorem zero_forbidden : zeroConstructor = .fail .undef := by
+  simp [zeroConstructor, core.num.nonzero.NonZero.new_unchecked,
+    Zerocopy.forbiddenExecution]
+
+example : ¬ WP.spec zeroConstructor (fun _ => True) := by simp [zero_forbidden]
+example : ¬ WP.dspec zeroConstructor (fun _ => True) := by simp [zero_forbidden]
+
+noncomputable def discardZero : Result Unit := do let _ ← zeroConstructor; .ok ()
+noncomputable def zeroBeforeDivergence : Result Unit := do let _ ← zeroConstructor; .div
+spec discarded for discardZero with 0 type parameters
+  ensures _ => True
+partial spec beforeDivergence for zeroBeforeDivergence with 0 type parameters
+  ensures _ => True
+
+example : ¬discarded := by simp [discarded, discardZero, zero_forbidden]
+example : ¬beforeDivergence := by
+  simp [beforeDivergence, zeroBeforeDivergence, zero_forbidden]
+
+theorem unsupported_carrier_forbidden {T Inner : Type}
+    (inst : core.num.nonzero.ZeroablePrimitive T Inner) (x : T) (unsupported : T ≠ Usize) :
+    core.num.nonzero.NonZero.new_unchecked inst x = .fail .undef := by
+  simp [core.num.nonzero.NonZero.new_unchecked, unsupported, Zerocopy.forbiddenExecution]
+
+-- A native dictionary alone supplies no alignment proposition. Without its
+-- law, an alignment-two model reaches a forbidden zero constructor. The
+-- premise here is a counterfactual model value, not an extra Rust assumption.
+theorem missing_law_forbidden (T : Type) (dictionary : Zerocopy.Unaligned T) (x : Usize)
+    (alignment : Zerocopy.RustLayout.align T = 2#usize) :
+    Zerocopy.trait_checks.divide_by_unaligned dictionary x = .fail .undef := by
+  have half : (1#usize / 2#usize : Result Usize) = .ok (0#usize) := by
+    obtain ⟨result, call, numeric⟩ :=
+      UScalar.div_spec (1#usize) (y := 2#usize) (by scalar_tac)
+    have zero : result = 0#usize := by
+      apply UScalar.eq_of_val_eq
+      simpa using numeric
+    simpa only [zero] using call
+  simp [Zerocopy.trait_checks.divide_by_unaligned, core.mem.align_of, alignment,
+    half, core.num.nonzero.NonZero.new_unchecked, Zerocopy.forbiddenExecution]
+
+example (T : Type) (dictionary : Zerocopy.Unaligned T) (x : Usize)
+    (alignment : Zerocopy.RustLayout.align T = 2#usize) :
+    ¬ WP.spec (Zerocopy.trait_checks.divide_by_unaligned dictionary x) (fun _ => True) := by
+  simp [missing_law_forbidden T dictionary x alignment]
+
+example (T : Type) (dictionary : Zerocopy.Unaligned T) (x : Usize)
+    (alignment : Zerocopy.RustLayout.align T = 2#usize) :
+    ¬ WP.dspec (Zerocopy.trait_checks.divide_by_unaligned dictionary x) (fun _ => True) := by
+  simp [missing_law_forbidden T dictionary x alignment]
+
+end NonZeroSafetyTests

verification/aeneas/lean/Obligations/TraitChecks.lean

@@ -42,6 +42,52 @@ def array_into_bytes_spec_contract (run : Result Unit) : Prop :=
 def array_into_bytes_spec : Prop :=
   array_into_bytes_spec_contract trait_checks.check_array_into_bytes
 
+def unaligned_alignment_spec_contract (T : Type) (dictionary : Unaligned T)
+    (run : Result Usize) : Prop :=
+  TraitLaws.unaligned T dictionary → run ⦃ alignment => alignment = 1#usize ⦄
+
+def unaligned_alignment_spec : Prop :=
+  ∀ (T : Type) (dictionary : Unaligned T),
+    unaligned_alignment_spec_contract T dictionary (trait_checks.unaligned_alignment dictionary)
+
+def unaligned_check_spec_contract (T : Type) (dictionary : Unaligned T)
+    (run : Result Unit) : Prop :=
+  TraitLaws.unaligned T dictionary → run ⦃ _ => True ⦄
+
+def unaligned_check_spec : Prop :=
+  ∀ (T : Type) (dictionary : Unaligned T),
+    unaligned_check_spec_contract T dictionary (trait_checks.check_unaligned dictionary)
+
+def unused_unaligned_bound_spec_contract (T : Type) (dictionary : Unaligned T)
+    (value : Usize) (run : Result Usize) : Prop :=
+  TraitLaws.unaligned T dictionary → run ⦃ result => result = value ⦄
+
+def unused_unaligned_bound_spec : Prop :=
+  ∀ (T : Type) (dictionary : Unaligned T) (value : Usize),
+    unused_unaligned_bound_spec_contract T dictionary value
+      (trait_checks.unused_unaligned_bound dictionary value)
+
+def concrete_unaligned_check_spec_contract (run : Result Unit) : Prop :=
+  run ⦃ _ => True ⦄
+
+def concrete_unaligned_check_spec : Prop :=
+  concrete_unaligned_check_spec_contract trait_checks.check_byte_unaligned
+
+def divide_by_unaligned_spec_contract (T : Type) (dictionary : Unaligned T)
+    (x : Usize) (run : Result Usize) : Prop :=
+  TraitLaws.unaligned T dictionary → run ⦃ result => result = x ⦄
+
+def divide_by_unaligned_spec : Prop :=
+  ∀ (T : Type) (dictionary : Unaligned T) (x : Usize),
+    divide_by_unaligned_spec_contract T dictionary x
+      (trait_checks.divide_by_unaligned dictionary x)
+
+def divide_by_byte_alignment_spec_contract (x : Usize) (run : Result Usize) : Prop :=
+  run ⦃ result => result = x ⦄
+
+def divide_by_byte_alignment_spec : Prop :=
+  ∀ (x : Usize), divide_by_byte_alignment_spec_contract x
+    (trait_checks.divide_by_byte_alignment x)
 
 def byte_codec_roundtrip_spec_contract (C : Type) (dictionary : trait_checks.ByteCodec C)
     (byte : U8) (run : Result U8) : Prop :=