Verify Boolean and NonZeroUsize candidate predicates

verification/aeneas/ADMISSION_DESIGN.md

@@ -65,6 +65,18 @@ The local offset copy avoids admitting its interpretation, without modifying the
 pinned toolchain. A future builtin replacement needs an independent law for the
 reconstructed destination, including unchanged length and prefix preservation.
 
+`util::validity::read_byte` reads one initialized byte with a bounds check. It
+returns `.fail .panic` out of bounds; it never constructs the type whose bit
+validity is being tested. Its exact source body and complete model are checked.
+This narrow boundary avoids importing the generic indexing dictionary's unused
+pointer operations. It supplies no premise about arbitrary raw-pointer reads,
+uninitialized storage, or padding. Boolean and nonzero-word predicates are
+extracted from the helpers used by the production `TryFromBytes` implementations.
+The checked scalar/pair conversions and slice validator retain all raw integer
+and byte inputs, including rejected encodings. Native regression tests compare
+them with the public conversions; the generic `Maybe` pointer path still relies
+on its existing Rust safety arguments.
+
 The report lives in the existing `bindings.json`. It includes both AST digests,
 root coverage, visited executions, call boundaries, registry digest, source
 identity, Cargo configuration hashes, and patched-runtime provenance. Compiler

verification/aeneas/external.json

@@ -24,6 +24,7 @@
   {"rust": "zerocopy::util::transmute_unchecked", "signature": {"unsafe": true, "inputs": ["T0"], "output": "T1", "types": 2, "consts": 0}, "lean": "util.transmute_unchecked", "opaque": true, "source_body_sha256": "58ee51c915af14bac8c12d66d5ac65feadf59742212c869c7f45f57f847d48b6"},
   {"rust": "zerocopy::util::copy_unchecked", "signature": {"unsafe": true, "inputs": ["&[u8]", "&mut [u8]"], "output": "tuple0", "types": 0, "consts": 0}, "lean": "util.copy_unchecked", "opaque": true, "source_body_sha256": "e3529644308d0a3ce1a407d163f98676faa36a286ba4a85221b894930d54fa20"},
   {"rust": "zerocopy::util::copy_unchecked_at", "signature": {"unsafe": true, "inputs": ["&[u8]", "&mut [u8]", "usize"], "output": "tuple0", "types": 0, "consts": 0}, "lean": "util.copy_unchecked_at", "opaque": true, "source_body_sha256": "968dea5ce0ba53c6d5922cb87b936d5ed58e7e81dce4bc36459d7a42ae251569"},
+  {"rust": "zerocopy::util::validity::read_byte", "signature": {"unsafe": false, "inputs": ["&[u8]", "usize"], "output": "u8", "types": 0, "consts": 0}, "lean": "util.validity.read_byte", "opaque": true, "source_body_sha256": "35941f898b8ec4684e6f36fefab11d0804ad0c9baa4f151becfaa20ad862976b"},
   {"rust": "core::num::{u16}::from_be_bytes", "signature": {"unsafe": false, "inputs": ["[u8;2]"], "output": "u16", "types": 0, "consts": 0}, "lean": "core.num.U16.from_be_bytes"},
   {"rust": "core::num::{u16}::from_le_bytes", "signature": {"unsafe": false, "inputs": ["[u8;2]"], "output": "u16", "types": 0, "consts": 0}, "lean": "core.num.U16.from_le_bytes"},
   {"rust": "core::num::{u16}::to_be_bytes", "signature": {"unsafe": false, "inputs": ["u16"], "output": "[u8;2]", "types": 0, "consts": 0}, "lean": "core.num.U16.to_be_bytes"},

verification/aeneas/golden/Funs.lean

@@ -2073,7 +2073,7 @@ def core.cell.UnsafeCell.Insts.ZerocopyIntoBytes {T : Type} (IntoBytesInst :
 }
 
 /-- [zerocopy::util::padding_needed_for]:
-    Source: 'src/util/mod.rs', lines 167:0-227:1 -/
+    Source: 'src/util/mod.rs', lines 168:0-228:1 -/
 def util.padding_needed_for
   (len : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -2089,7 +2089,7 @@ def util.padding_needed_for
   ok (i2 &&& mask)
 
 /-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
-    Source: 'src/util/mod.rs', lines 254:0-272:1 -/
+    Source: 'src/util/mod.rs', lines 255:0-273:1 -/
 def util.round_down_to_next_multiple_of_alignment
   (n : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -2106,7 +2106,7 @@ def util.round_down_to_next_multiple_of_alignment
   ok (n &&& mask)
 
 /-- [zerocopy::util::max]:
-    Source: 'src/util/mod.rs', lines 281:0-287:1 -/
+    Source: 'src/util/mod.rs', lines 282:0-288:1 -/
 def util.max
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -2126,7 +2126,7 @@ def util.max
   else ok a
 
 /-- [zerocopy::util::min]:
-    Source: 'src/util/mod.rs', lines 296:0-302:1 -/
+    Source: 'src/util/mod.rs', lines 297:0-303:1 -/
 def util.min
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -2180,13 +2180,19 @@ def util.owned_transmute.round_trip_checks
   let restored ← util.owned_transmute.from_bytes bytes
   massert (restored = value)
 
+/-- [zerocopy::util::validity::bool_encoding]:
+    Source: 'src/util/validity/mod.rs', lines 26:0-28:1 -/
+def util.validity.bool_encoding (byte : Std.U8) : Result Bool := do
+  ok (byte < 2#u8)
+
 /-- [zerocopy::util::safety_checks::checked_bool]:
     Source: 'src/util/safety_checks/mod.rs', lines 28:0-38:1 -/
 def util.safety_checks.checked_bool
   (byte : Std.U8) : Result (Option Bool) := do
-  if byte < 2#u8
-  then let b ← util.transmute_unchecked Bool byte
-       ok (some b)
+  let b ← util.validity.bool_encoding byte
+  if b
+  then let b1 ← util.transmute_unchecked Bool byte
+       ok (some b1)
   else ok none
 
 /-- [zerocopy::util::safety_checks::checked_copy]:
@@ -2202,4 +2208,74 @@ def util.safety_checks.checked_copy
        ok (true, dst1)
   else ok (false, dst)
 
+/-- [zerocopy::util::validity::nonzero_encoding]:
+    Source: 'src/util/validity/mod.rs', lines 37:0-39:1 -/
+def util.validity.nonzero_encoding (n : Std.Usize) : Result Bool := do
+  ok (n != 0#usize)
+
+/-- [zerocopy::util::safety_checks::checked_nonzero]:
+    Source: 'src/util/safety_checks/mod.rs', lines 72:0-78:1 -/
+def util.safety_checks.checked_nonzero
+  (n : Std.Usize) :
+  Result (Option (core.num.nonzero.NonZero Std.Usize
+    core.num.niche_types.NonZeroUsizeInner))
+  := do
+  let b ← util.validity.nonzero_encoding n
+  if b
+  then
+    core.num.nonzero.NonZero.new
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner n
+  else ok none
+
+/-- [zerocopy::util::safety_checks::checked_bool_pair]:
+    Source: 'src/util/safety_checks/mod.rs', lines 91:0-97:1 -/
+def util.safety_checks.checked_bool_pair
+  (bytes : Array Std.U8 2#usize) : Result (Option (Array Bool 2#usize)) := do
+  let s ← lift (Array.to_slice bytes)
+  let left ← util.validity.read_byte s 0#usize
+  let s1 ← lift (Array.to_slice bytes)
+  let right ← util.validity.read_byte s1 1#usize
+  let o ← util.safety_checks.checked_bool left
+  match o with
+  | none => ok none
+  | some left1 =>
+    let o1 ← util.safety_checks.checked_bool right
+    match o1 with
+    | none => ok none
+    | some right1 => ok (some (Array.make 2#usize [ left1, right1 ]))
+
+/-- [zerocopy::util::safety_checks::bool_slice_valid]: loop body 0:
+    Source: 'src/util/safety_checks/mod.rs', lines 108:4-115:1 -/
+@[rust_loop_body]
+def util.safety_checks.bool_slice_valid_loop.body
+  (bytes : Slice Std.U8) (i : Std.Usize) :
+  Result (ControlFlow Std.Usize Bool)
+  := do
+  let i1 := Slice.len bytes
+  if i < i1
+  then
+    let i2 ← util.validity.read_byte bytes i
+    let b ← util.validity.bool_encoding i2
+    if b
+    then let i3 ← i + 1#usize
+         ok (cont i3)
+    else ok (done false)
+  else ok (done true)
+
+/-- [zerocopy::util::safety_checks::bool_slice_valid]: loop 0:
+    Source: 'src/util/safety_checks/mod.rs', lines 108:4-115:1 -/
+@[rust_loop]
+def util.safety_checks.bool_slice_valid_loop
+  (bytes : Slice Std.U8) (i : Std.Usize) : Result Bool := do
+  loop
+    (fun i1 => util.safety_checks.bool_slice_valid_loop.body bytes i1)
+    i
+
+/-- [zerocopy::util::safety_checks::bool_slice_valid]:
+    Source: 'src/util/safety_checks/mod.rs', lines 106:0-115:1 -/
+@[reducible]
+def util.safety_checks.bool_slice_valid
+  (bytes : Slice Std.U8) : Result Bool := do
+  util.safety_checks.bool_slice_valid_loop bytes 0#usize
+
 end Zerocopy

verification/aeneas/golden/FunsExternal_Template.lean

@@ -52,6 +52,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]
@@ -64,12 +75,12 @@ axiom core.num.nonzero.NonZero.get
   core.num.nonzero.NonZero T Clause0_NonZeroInner → Result T
 
 /-- [zerocopy::util::copy_unchecked]:
-    Source: 'src/util/mod.rs', lines 314:0-329:1 -/
+    Source: 'src/util/mod.rs', lines 315:0-330:1 -/
 axiom util.copy_unchecked
   : Slice Std.U8 → Slice Std.U8 → Result (Slice Std.U8)
 
 /-- [zerocopy::util::copy_unchecked_at]:
-    Source: 'src/util/mod.rs', lines 343:0-354:1 -/
+    Source: 'src/util/mod.rs', lines 344:0-355:1 -/
 axiom util.copy_unchecked_at
   : Slice Std.U8 → Slice Std.U8 → Std.Usize → Result (Slice Std.U8)
 
@@ -130,6 +141,10 @@ axiom Array.Insts.ZerocopyTryFromBytes.is_safe
     Bool
 
 /-- [zerocopy::util::transmute_unchecked]:
-    Source: 'src/util/mod.rs', lines 366:0-395:1 -/
+    Source: 'src/util/mod.rs', lines 367:0-396:1 -/
 axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst
 
+/-- [zerocopy::util::validity::read_byte]:
+    Source: 'src/util/validity/mod.rs', lines 49:0-51:1 -/
+axiom util.validity.read_byte : Slice Std.U8 → Std.Usize → Result Std.U8
+

verification/aeneas/lean/Obligations/Validity.lean

@@ -0,0 +1,50 @@
+/- 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
+@[expose] public section
+open Aeneas Aeneas.Std
+namespace Zerocopy.Obligations
+
+-- These expectations retain all raw candidate values. A decoder rejecting bad
+-- candidates at the INPUT would conceal precisely the cases being validated.
+def bool_encoding_spec_contract (byte : U8) (run : Result Bool) : Prop :=
+  run ⦃ out => out = decide (byte.val = 0 ∨ byte.val = 1) ⦄
+def bool_encoding_spec : Prop :=
+  ∀ byte, bool_encoding_spec_contract byte (util.validity.bool_encoding byte)
+
+def nonzero_encoding_spec_contract (n : Usize) (run : Result Bool) : Prop :=
+  run ⦃ out => out = decide (n.val ≠ 0) ⦄
+def nonzero_encoding_spec : Prop :=
+  ∀ n, nonzero_encoding_spec_contract n (util.validity.nonzero_encoding n)
+
+def checked_nonzero_spec_contract (n : Usize)
+    (run : Result (Option (core.num.nonzero.NonZero Usize
+      core.num.niche_types.NonZeroUsizeInner))) : Prop :=
+  run ⦃ out => match out with
+    | none => n.val = 0
+    | some value => value.val = n ∧ 0 < value.val.val ⦄
+def checked_nonzero_spec : Prop :=
+  ∀ n, checked_nonzero_spec_contract n (util.safety_checks.checked_nonzero n)
+
+def checked_bool_pair_spec_contract (bytes : Aeneas.Std.Array U8 2#usize)
+    (run : Result (Option (Aeneas.Std.Array Bool 2#usize))) : Prop :=
+  run ⦃ out => match out with
+    | none => ∃ byte ∈ bytes.val, 2 ≤ byte.val
+    | some values => values.val = bytes.val.map (fun byte => decide (byte.val = 1)) ∧
+        ∀ byte ∈ bytes.val, byte.val < 2 ⦄
+def checked_bool_pair_spec : Prop :=
+  ∀ bytes, checked_bool_pair_spec_contract bytes (util.safety_checks.checked_bool_pair bytes)
+
+def bool_slice_valid_spec_contract (bytes : Slice U8) (run : Result Bool) : Prop :=
+  run ⦃ out => out = decide (∀ byte ∈ bytes.val, byte.val < 2) ⦄
+def bool_slice_valid_spec : Prop :=
+  ∀ bytes, bool_slice_valid_spec_contract bytes (util.safety_checks.bool_slice_valid bytes)
+
+end Zerocopy.Obligations

verification/aeneas/lean/Proofs/SafetyChecks.lean

@@ -49,9 +49,9 @@ theorem checked_bool_raw (byte : U8) :
     util.safety_checks.checked_bool byte ⦃ out =>
       out = if byte.val < 2 then some (decide (byte.val = 1)) else none ⦄ := by
   by_cases valid : byte.val < 2
-  · simp [util.safety_checks.checked_bool, UScalar.lt_equiv,
+  · simp [util.safety_checks.checked_bool, util.validity.bool_encoding, UScalar.lt_equiv,
       UScalar.ofNatCore_val_eq, util.transmute_unchecked, valid, bind_ok]
-  · simp [util.safety_checks.checked_bool, UScalar.lt_equiv,
+  · simp [util.safety_checks.checked_bool, util.validity.bool_encoding, UScalar.lt_equiv,
       UScalar.ofNatCore_val_eq, valid]
 
 theorem checked_bool_spec : Specs.checked_bool_spec := by