Verify Boolean and NonZeroUsize candidate predicates

Use extracted value predicates in the production TryFromBytes validators
for bool and NonZeroUsize. Keep Boolean candidates as bytes until validation,
so invalid encodings remain expressible in the model.

Prove scalar and pair conversions and a terminating Boolean-slice
validator, including rejected inputs. Reuse the production predicates and
compare the concrete candidates with public conversions, exhaustively for
Boolean bytes and pairs.

Register a narrow, source-bound byte read that preserves bounds failure.
Check its complete interpretation and reject an out-of-range-read mutant.
Reading through the generic Maybe pointer abstraction remains a separate
Rust safety premise.

gherrit-pr-id: G7q2xz2bs5ln4dfgckfspk2us4dhjperw
Agent-authored-by: AI agent acting on joshlf's behalf

Author: joshlf

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

@@ -1808,7 +1808,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
@@ -1824,7 +1824,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
@@ -1841,7 +1841,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)
@@ -1861,7 +1861,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)
@@ -1915,13 +1915,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]:
@@ -1937,4 +1943,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

@@ -46,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]
@@ -58,16 +69,20 @@ 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 340:0-351:1 -/
+    Source: 'src/util/mod.rs', lines 341:0-352:1 -/
 axiom util.copy_unchecked_at
   : Slice Std.U8 → Slice Std.U8 → Std.Usize → Result (Slice Std.U8)
 
 /-- [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