From 2592efcb0a40aeb4c8bb0f0155dc58afd85efa94 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 8 Oct 2026 21:45:14 -0400 Subject: [PATCH] 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 --- verification/aeneas/ADMISSION_DESIGN.md | 12 ++ verification/aeneas/external.json | 1 + verification/aeneas/golden/Funs.lean | 90 +++++++++- .../aeneas/golden/FunsExternal_Template.lean | 21 ++- .../aeneas/lean/Obligations/Validity.lean | 50 ++++++ .../aeneas/lean/Proofs/SafetyChecks.lean | 4 +- verification/aeneas/lean/Proofs/Validity.lean | 168 ++++++++++++++++++ .../lean/RequiredModelContracts/Validity.lean | 57 ++++++ verification/aeneas/lean/SafetyTests.lean | 5 + .../aeneas/lean/Zerocopy/FunsExternal.lean | 15 ++ verification/aeneas/projections/Specs.lean | 45 +++++ zerocopy/src/impls.rs | 13 +- zerocopy/src/util/mod.rs | 1 + zerocopy/src/util/safety_checks/mod.rs | 87 ++++++++- zerocopy/src/util/validity/mod.rs | 51 ++++++ 15 files changed, 605 insertions(+), 15 deletions(-) create mode 100644 verification/aeneas/lean/Obligations/Validity.lean create mode 100644 verification/aeneas/lean/Proofs/Validity.lean create mode 100644 verification/aeneas/lean/RequiredModelContracts/Validity.lean create mode 100644 zerocopy/src/util/validity/mod.rs diff --git a/verification/aeneas/ADMISSION_DESIGN.md b/verification/aeneas/ADMISSION_DESIGN.md index 16a1ff1a1b..22755945b3 100644 --- a/verification/aeneas/ADMISSION_DESIGN.md +++ b/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 diff --git a/verification/aeneas/external.json b/verification/aeneas/external.json index 8f79f04bda..4b04e20b84 100644 --- a/verification/aeneas/external.json +++ b/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"}, diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index a8d818d0c1..c6237d79f3 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/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 diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean index ce24b5be06..5b4246f474 100644 --- a/verification/aeneas/golden/FunsExternal_Template.lean +++ b/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}::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}::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 + diff --git a/verification/aeneas/lean/Obligations/Validity.lean b/verification/aeneas/lean/Obligations/Validity.lean new file mode 100644 index 0000000000..2a779c984a --- /dev/null +++ b/verification/aeneas/lean/Obligations/Validity.lean @@ -0,0 +1,50 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , 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 diff --git a/verification/aeneas/lean/Proofs/SafetyChecks.lean b/verification/aeneas/lean/Proofs/SafetyChecks.lean index ae2b1edcaa..5ca62b7a0e 100644 --- a/verification/aeneas/lean/Proofs/SafetyChecks.lean +++ b/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 diff --git a/verification/aeneas/lean/Proofs/Validity.lean b/verification/aeneas/lean/Proofs/Validity.lean new file mode 100644 index 0000000000..61abee7e12 --- /dev/null +++ b/verification/aeneas/lean/Proofs/Validity.lean @@ -0,0 +1,168 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Specs +public import Proofs.SafetyChecks +public import BytesAdapter +@[expose] public section +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +-- These are the predicates called by the production scalar validators. The +-- raw candidates include every u8/usize value, not just valid encodings. +theorem bool_encoding_raw (byte : U8) : + util.validity.bool_encoding byte ⦃ out => + out = decide (byte.val = 0 ∨ byte.val = 1) ⦄ := by + simp only [util.validity.bool_encoding, WP.spec_ok] + apply Bool.eq_iff_iff.mpr + simp only [UScalar.lt_equiv, UScalar.ofNatCore_val_eq, decide_eq_true_eq] + omega + +theorem nonzero_encoding_raw (n : Usize) : + util.validity.nonzero_encoding n ⦃ out => out = decide (n.val ≠ 0) ⦄ := by + simp only [util.validity.nonzero_encoding, WP.spec_ok] + apply Bool.eq_iff_iff.mpr + simp [bne_iff_ne, UScalar.eq_equiv] + +theorem bool_encoding_spec : Specs.bool_encoding_spec := by + intro byte _ _ + apply WP.spec_mono (bool_encoding_raw byte) + intro out facts + exact ⟨out, rfl, facts⟩ + +theorem nonzero_encoding_spec : Specs.nonzero_encoding_spec := by + intro n _ _ + apply WP.spec_mono (nonzero_encoding_raw n) + intro out facts + exact ⟨out, rfl, facts⟩ + +-- Successful construction must return the original word, with a nonzero raw +-- representation. The decoder therefore cannot hide an invalid zero result. +theorem checked_nonzero_raw (n : Usize) : + util.safety_checks.checked_nonzero n ⦃ out => match out with + | none => n.val = 0 + | some value => value.val = n ∧ 0 < value.val.val ⦄ := by + by_cases zero : n.val = 0 + · simp [util.safety_checks.checked_nonzero, util.validity.nonzero_encoding, + UScalar.eq_equiv, zero, bind_ok] + · have positive : 0 < n.val := by omega + simp [util.safety_checks.checked_nonzero, util.validity.nonzero_encoding, + core.num.nonzero.NonZero.new, bne_iff_ne, UScalar.eq_equiv, zero, + positive, bind_ok] + +theorem checked_nonzero_spec : Specs.checked_nonzero_spec := by + intro n _ _ + apply WP.spec_mono (checked_nonzero_raw n) + intro out facts + cases out with + | none => exact ⟨none, rfl, facts⟩ + | some value => + refine ⟨some ⟨unsignedWord value.val, facts.2⟩, ?_, facts⟩ + simp only [RustModel.decode, facts.2, ↓reduceDIte, Option.map_some] + +-- The fixed array bridge reads bytes before their Boolean validity is known. +-- Both reads have statically proved bounds; construction uses the checked +-- scalar conversion, so no invalid Bool can disappear through the carrier. +theorem checked_bool_pair_raw (bytes : Aeneas.Std.Array U8 2#usize) : + util.safety_checks.checked_bool_pair bytes ⦃ 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 ⦄ := by + obtain ⟨left, right, same⟩ := List.length_eq_two.mp + (show bytes.val.length = 2 by simp) + by_cases hl : left.val ≤ 1 <;> by_cases hr : right.val ≤ 1 <;> + simp [util.safety_checks.checked_bool_pair, Array.to_slice, + util.validity.read_byte, util.safety_checks.checked_bool, + util.validity.bool_encoding, util.transmute_unchecked, + UScalar.lt_equiv, UScalar.ofNatCore_val_eq, lift, bind_ok, same, hl, hr] <;> omega + +private theorem decode_bool_list (values : List Bool) : + decodeList (modelBool).decode values = some values := by + change decodeList some values = some values + induction values with + | nil => rfl + | cons head tail ih => simp [decodeList, ih] + +private def boolArray (raw : Aeneas.Std.Array Bool 2#usize) : ArrayValue Bool 2#usize := + ⟨raw.val, raw.property⟩ + +private theorem decode_bool_array (raw : Aeneas.Std.Array Bool 2#usize) : + (modelArray 2#usize).decode raw = some (boolArray raw) := by + apply (decodeArray_iff modelBool 2#usize raw (boolArray raw)).mpr + exact decode_bool_list raw.val + +theorem checked_bool_pair_spec : Specs.checked_bool_pair_spec := by + intro bytes _ _ + apply WP.spec_mono (checked_bool_pair_raw bytes) + intro out facts + cases out with + | none => exact ⟨none, rfl, facts⟩ + | some values => + exact ⟨some (boolArray values), by + change Option.map some ((modelArray 2#usize).decode values) = + some (some (boolArray values)) + rw [decode_bool_array values] + rfl, facts⟩ + +-- Unlike the layout adapter, this loop may finish early with false. Use the +-- upstream decreasing-natural rule directly, retaining the checked prefix. +theorem bool_slice_loop_raw (bytes : Slice U8) (i : Usize) + (bound : i.val ≤ bytes.val.length) + (checked : ∀ j, j < i.val → (bytes.val[j]!).val < 2) : + util.safety_checks.bool_slice_valid_loop bytes i ⦃ out => + out = decide (∀ byte ∈ bytes.val, byte.val < 2) ⦄ := by + unfold util.safety_checks.bool_slice_valid_loop + apply loop.spec_decr_nat + (fun i : Usize => bytes.val.length - i.val) + (fun i => i.val ≤ bytes.val.length ∧ ∀ j, j < i.val → (bytes.val[j]!).val < 2) + · intro idx ⟨bound, checked⟩ + unfold util.safety_checks.bool_slice_valid_loop.body + simp only [UScalar.lt_equiv, Slice.len_val, Slice.length] + split + · rename_i inside + simp only [util.validity.read_byte, inside, ↓reduceIte, bind_ok, + util.validity.bool_encoding, UScalar.lt_equiv, UScalar.ofNatCore_val_eq, decide_eq_true_eq] + split + · rename_i valid + step with Usize.add_spec (x := idx) (y := 1#usize) (by + have := bytes.property + simp only [UScalar.ofNatCore_val_eq] + omega) as ⟨next, advanced⟩ + refine ⟨by omega, ?_, by omega⟩ + intro j before + by_cases earlier : j < idx.val + · exact checked j earlier + · have same : j = idx.val := by omega + simpa only [same] using valid + · rename_i invalid + have rejected : ¬ (∀ byte ∈ bytes.val, byte.val < 2) := by + intro all + have member : bytes.val[idx.val]! ∈ bytes.val := by + simpa only [getElem!_pos bytes.val idx.val inside] using List.getElem_mem inside + exact invalid (all _ member) + simp only [WP.spec_ok] + exact (decide_eq_false rejected).symm + · rename_i finished + have at_end : idx.val = bytes.val.length := by omega + have all : ∀ byte ∈ bytes.val, byte.val < 2 := by + intro byte member + obtain ⟨j, hj, same⟩ := List.getElem_of_mem member + have good := checked j (by omega) + simpa only [getElem!_pos bytes.val j hj, same] using good + simp only [WP.spec_ok] + exact (decide_eq_true all).symm + · exact ⟨bound, checked⟩ + +theorem bool_slice_valid_spec : Specs.bool_slice_valid_spec := by + intro bytes _ _ + apply WP.spec_mono (bool_slice_loop_raw bytes 0#usize (by simp) (by simp)) + intro out facts + exact ⟨out, rfl, facts⟩ + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RequiredModelContracts/Validity.lean b/verification/aeneas/lean/RequiredModelContracts/Validity.lean new file mode 100644 index 0000000000..94da37a22f --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/Validity.lean @@ -0,0 +1,57 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import RequiredContracts +public import Proofs.Validity +public import Obligations.Validity +@[expose] public section +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +-- Supply an independent admission witness for EVERY raw input. The subsequent +-- implications consume only the authored postcondition, for any execution. +@[contract_simps] theorem required_bool_encoding (byte : U8) (run : Result Bool) + (provided : Specs.bool_encoding_spec_contract byte run) : + Obligations.bool_encoding_spec_contract byte run := by + apply WP.spec_mono (provided (unsignedWord byte) rfl) + rintro out ⟨_, _, facts⟩ + exact facts + +@[contract_simps] theorem required_nonzero_encoding (n : Usize) (run : Result Bool) + (provided : Specs.nonzero_encoding_spec_contract n run) : + Obligations.nonzero_encoding_spec_contract n run := by + apply WP.spec_mono (provided (unsignedWord n) rfl) + rintro out ⟨_, _, facts⟩ + exact facts + +@[contract_simps] theorem required_checked_nonzero (n : Usize) + (run : Result (Option (core.num.nonzero.NonZero Usize + core.num.niche_types.NonZeroUsizeInner))) + (provided : Specs.checked_nonzero_spec_contract n run) : + Obligations.checked_nonzero_spec_contract n run := by + apply WP.spec_mono (provided (unsignedWord n) rfl) + rintro out ⟨_, _, facts⟩ + exact facts + +@[contract_simps] theorem required_checked_bool_pair (bytes : Aeneas.Std.Array U8 2#usize) + (run : Result (Option (Aeneas.Std.Array Bool 2#usize))) + (provided : Specs.checked_bool_pair_spec_contract bytes run) : + Obligations.checked_bool_pair_spec_contract bytes run := by + apply WP.spec_mono (provided (unsignedArray bytes) (decodeArray_unsigned bytes)) + rintro out ⟨_, _, facts⟩ + exact facts + +@[contract_simps] theorem required_bool_slice_valid (bytes : Slice U8) (run : Result Bool) + (provided : Specs.bool_slice_valid_spec_contract bytes run) : + Obligations.bool_slice_valid_spec_contract bytes run := by + apply WP.spec_mono (provided (byteSlice bytes) (decode_byte_slice bytes)) + rintro out ⟨_, _, facts⟩ + exact facts + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/SafetyTests.lean b/verification/aeneas/lean/SafetyTests.lean index e374074266..554daab40a 100644 --- a/verification/aeneas/lean/SafetyTests.lean +++ b/verification/aeneas/lean/SafetyTests.lean @@ -38,6 +38,11 @@ theorem offset_copy_rejects_oversize (src dst : Slice U8) (start : Usize) simp [util.copy_unchecked_at, Zerocopy.forbiddenExecution, inside, Nat.not_le.mpr oversize] +theorem byte_read_rejects_outside (bytes : Slice U8) (index : Usize) + (outside : bytes.val.length ≤ index.val) : + util.validity.read_byte bytes index = .fail .panic := by + simp [util.validity.read_byte, Nat.not_lt.mpr outside] + -- This is the model of an unsafe producer with an invalid bit pattern. These -- examples execute no Rust UB: they examine its forbidden abstract outcome. noncomputable def badBool : Result Bool := util.transmute_unchecked Bool (2#u8) diff --git a/verification/aeneas/lean/Zerocopy/FunsExternal.lean b/verification/aeneas/lean/Zerocopy/FunsExternal.lean index 6b58a42033..89b3bc79de 100644 --- a/verification/aeneas/lean/Zerocopy/FunsExternal.lean +++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean @@ -107,6 +107,11 @@ def util.copy_unchecked_at (src dst : Slice U8) (start : Usize) : Result (Slice else forbiddenExecution else .fail .panic +-- Reading bytes never assumes the validity of the type they might encode. +-- Bounds are checked at execution, including when the caller discards the byte. +def util.validity.read_byte (bytes : Slice U8) (index : Usize) : Result U8 := + if index.val < bytes.val.length then .ok bytes.val[index.val]! else .fail .panic + -- Only the u8-to-bool instantiation is supported. The admission checker also -- checks the original Rust type arguments, before Aeneas can erase them. This -- guard checks bit validity BEFORE creating a Bool, whose Lean carrier cannot @@ -153,3 +158,13 @@ def core.intrinsics.transmute {Src : Type} (Dst : Type) @[simp] def core.num.nonzero.NonZero.get {T Inner : Type} (_inst : core.num.nonzero.ZeroablePrimitive T Inner) (x : core.num.nonzero.NonZero T Inner) : Result T := .ok x.val + +-- The extracted call sites instantiate this primitive only at Usize. Other +-- types are unsupported, so the model cannot promise a recoverable panic. +@[simp] noncomputable def core.num.nonzero.NonZero.new + {T Inner : Type} (_inst : core.num.nonzero.ZeroablePrimitive T Inner) + (x : T) : Result (Option (core.num.nonzero.NonZero T Inner)) := by + classical + exact if h : T = Usize then + if (cast h x : Usize) = 0#usize then .ok none else .ok (some ⟨x⟩) + else forbiddenExecution diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index febac5a7e4..3c31859ab8 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/verification/aeneas/projections/Specs.lean @@ -287,4 +287,49 @@ spec checked_copy_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.checked_copy_spec for Zerocopy.util.safety_checks.checked_copy with 2 +check_model_inputs Zerocopy.util.safety_checks.checked_nonzero with 0 type parameters +aeneas_spec_begin +spec checked_nonzero_spec + for @Zerocopy.util.safety_checks.checked_nonzero with 0 type parameters + ensures(raw) r => match r with + | none => n.val = 0 + | some value => value.val = n ∧ 0 < value.val.val +aeneas_spec_end +check_spec_binding Zerocopy.Specs.checked_nonzero_spec for Zerocopy.util.safety_checks.checked_nonzero with 1 + +check_model_inputs Zerocopy.util.safety_checks.checked_bool_pair with 0 type parameters +aeneas_spec_begin +spec checked_bool_pair_spec + for @Zerocopy.util.safety_checks.checked_bool_pair with 0 type parameters + ensures(raw) r => match r 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 +aeneas_spec_end +check_spec_binding Zerocopy.Specs.checked_bool_pair_spec for Zerocopy.util.safety_checks.checked_bool_pair with 1 + +check_model_inputs Zerocopy.util.safety_checks.bool_slice_valid with 0 type parameters +aeneas_spec_begin +spec bool_slice_valid_spec + for @Zerocopy.util.safety_checks.bool_slice_valid with 0 type parameters + ensures(raw) r => r = decide (∀ byte ∈ bytes.val, byte.val < 2) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.bool_slice_valid_spec for Zerocopy.util.safety_checks.bool_slice_valid with 1 + +check_model_inputs Zerocopy.util.validity.bool_encoding with 0 type parameters +aeneas_spec_begin +spec bool_encoding_spec + for @Zerocopy.util.validity.bool_encoding with 0 type parameters + ensures(raw) r => r = decide (byte.val = 0 ∨ byte.val = 1) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.bool_encoding_spec for Zerocopy.util.validity.bool_encoding with 1 + +check_model_inputs Zerocopy.util.validity.nonzero_encoding with 0 type parameters +aeneas_spec_begin +spec nonzero_encoding_spec + for @Zerocopy.util.validity.nonzero_encoding with 0 type parameters + ensures(raw) r => r = decide (n.val ≠ 0) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.nonzero_encoding_spec for Zerocopy.util.validity.nonzero_encoding with 1 + end Zerocopy.Specs diff --git a/zerocopy/src/impls.rs b/zerocopy/src/impls.rs index 48f1f24774..87965aa194 100644 --- a/zerocopy/src/impls.rs +++ b/zerocopy/src/impls.rs @@ -226,7 +226,7 @@ assert_unaligned!(bool); const _: () = unsafe { unsafe_impl!(=> TryFromBytes for bool; |byte| { let byte = byte.transmute_with::(); - *byte.unaligned_as_ref() < 2 + util::validity::bool_encoding(*byte.unaligned_as_ref()) }) }; @@ -302,11 +302,20 @@ const _: () = unsafe { }; macro_rules! unsafe_impl_try_from_bytes_for_nonzero { + // Expose the word predicate to Lean without changing the other scalar + // implementations. Their widths and standard-library carriers can be + // covered separately as those models are admitted. + (@validate NonZeroUsize, $value:expr) => { + util::validity::nonzero_encoding($value) + }; + (@validate $nonzero:ident, $value:expr) => { + $nonzero::new($value).is_some() + }; ($($nonzero:ident[$prim:ty]),*) => { $( unsafe_impl!(=> TryFromBytes for $nonzero; |n| { let n = n.transmute_with::, invariant::Safe, CastSizedExact, BecauseImmutable>(); - $nonzero::new(n.read().into_inner()).is_some() + unsafe_impl_try_from_bytes_for_nonzero!(@validate $nonzero, n.read().into_inner()) }); )* } diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs index f4c53b4428..97d5315413 100644 --- a/zerocopy/src/util/mod.rs +++ b/zerocopy/src/util/mod.rs @@ -19,6 +19,7 @@ pub(crate) mod bytewrite; #[allow(dead_code)] mod owned_transmute; mod safety_checks; +pub(crate) mod validity; use core::{ marker::PhantomData, diff --git a/zerocopy/src/util/safety_checks/mod.rs b/zerocopy/src/util/safety_checks/mod.rs index 29bde56082..1dcdd05e8c 100644 --- a/zerocopy/src/util/safety_checks/mod.rs +++ b/zerocopy/src/util/safety_checks/mod.rs @@ -26,7 +26,7 @@ /// ensures(raw) r => r = if byte.val < 2 then some (decide (byte.val = 1)) else none /// ``` fn checked_bool(byte: u8) -> Option { - if byte < 2 { + if super::validity::bool_encoding(byte) { // SAFETY: The branch restricts `byte` to 0 or 1, the two boolean bit // patterns. Both types have size one, satisfying the helper's size // assertion. The trusted interpretation checks this same condition @@ -60,9 +60,64 @@ fn checked_copy(src: &[u8], dst: &mut [u8]) -> bool { } } +/// Checks the same scalar predicate used by `NonZero`'s validator, then +/// constructs a nonzero word. Zero remains representable at the input boundary. +/// +/// ```aeneas +/// spec checked_nonzero_spec +/// ensures(raw) r => match r with +/// | none => n.val = 0 +/// | some value => value.val = n ∧ 0 < value.val.val +/// ``` +fn checked_nonzero(n: usize) -> Option { + if super::validity::nonzero_encoding(n) { + core::num::NonZeroUsize::new(n) + } else { + None + } +} + +/// Converts two raw candidate bytes using the checked scalar conversion. +/// Invalid candidates are never constructed as bools, even transiently. +/// +/// ```aeneas +/// spec checked_bool_pair_spec +/// ensures(raw) r => match r 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 +/// ``` +#[allow(clippy::question_mark)] // Keep branches first-order instead of using a Try dictionary. +fn checked_bool_pair(bytes: [u8; 2]) -> Option<[bool; 2]> { + let left = super::validity::read_byte(&bytes, 0); + let right = super::validity::read_byte(&bytes, 1); + let left = if let Some(left) = checked_bool(left) { left } else { return None }; + let right = if let Some(right) = checked_bool(right) { right } else { return None }; + Some([left, right]) +} + +/// Validates a concrete boolean slice by checking every raw candidate byte. +/// +/// ```aeneas +/// spec bool_slice_valid_spec +/// ensures(raw) r => r = decide (∀ byte ∈ bytes.val, byte.val < 2) +/// ``` +#[allow(clippy::arithmetic_side_effects)] // i < bytes.len() rules out overflow of i + 1. +fn bool_slice_valid(bytes: &[u8]) -> bool { + let mut i = 0; + while i < bytes.len() { + if !super::validity::bool_encoding(super::validity::read_byte(bytes, i)) { + return false; + } + i += 1; + } + true +} + #[cfg(test)] mod tests { use super::*; + use crate::TryFromBytes; #[test] fn all_boolean_bytes() { @@ -75,6 +130,36 @@ mod tests { _ => None, } ); + assert_eq!(checked_bool(byte), bool::try_read_from_bytes(&[byte]).ok()); + } + } + + #[test] + fn boolean_array_and_slice_candidates() { + for left in 0..=u8::MAX { + for right in 0..=u8::MAX { + let bytes = [left, right]; + assert_eq!(checked_bool_pair(bytes), <[bool; 2]>::try_read_from_bytes(&bytes).ok()); + assert_eq!(bool_slice_valid(&bytes), <[bool]>::try_ref_from_bytes(&bytes).is_ok()); + } + } + assert!(bool_slice_valid(&[])); + assert!(bool_slice_valid(&[0, 1, 0, 1])); + for invalid_index in 0..4 { + let mut bytes = [0, 1, 0, 1]; + bytes[invalid_index] = 2; + assert!(!bool_slice_valid(&bytes)); + <[bool]>::try_ref_from_bytes(&bytes).unwrap_err(); + } + } + + #[test] + fn nonzero_candidates() { + for n in [0, 1, 2, 255, 256, usize::MAX / 2, usize::MAX] { + assert_eq!( + checked_nonzero(n), + core::num::NonZeroUsize::try_read_from_bytes(&n.to_ne_bytes()).ok() + ); } } diff --git a/zerocopy/src/util/validity/mod.rs b/zerocopy/src/util/validity/mod.rs new file mode 100644 index 0000000000..60752712a4 --- /dev/null +++ b/zerocopy/src/util/validity/mod.rs @@ -0,0 +1,51 @@ +// SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT +// +// Copyright 2026 The Fuchsia Authors +// +// Licensed under the 2-Clause BSD License , Apache License, Version 2.0 +// , or the MIT +// license , at your option. +// This file may not be copied, modified, or distributed except according to +// those terms. + +//! Value predicates shared by the actual scalar `TryFromBytes` implementations. +//! +//! Candidates retain their integer representation until these checks finish. +//! In particular, a candidate for `bool` is a `u8`, not a Lean or Rust `bool` +//! which would already exclude invalid encodings. Reading the candidate through +//! `Maybe` remains the implementation's separate pointer safety argument. + +/// Accepts exactly the two boolean bit patterns. +/// +/// ```aeneas +/// spec bool_encoding_spec +/// ensures(raw) r => r = decide (byte.val = 0 ∨ byte.val = 1) +/// ``` +#[inline] +pub(crate) fn bool_encoding(byte: u8) -> bool { + byte < 2 +} + +/// Accepts exactly the nonzero word representations. +/// +/// ```aeneas +/// spec nonzero_encoding_spec +/// ensures(raw) r => r = decide (n.val ≠ 0) +/// ``` +#[inline] +pub(crate) fn nonzero_encoding(n: usize) -> bool { + n != 0 +} + +/// Reads an initialized raw byte, with the ordinary slice bounds check. +/// +/// This narrow, source-bound interpretation avoids importing the whole generic +/// indexing dictionary (including unsupported pointer operations) to read one +/// byte. It does not create a bool, a reference, or a possibly invalid integer. +/// Aeneas checks its complete guarded interpretation independently in Check. +#[inline] +#[allow(clippy::indexing_slicing)] // The model explicitly preserves this bounds check. +pub(crate) fn read_byte(bytes: &[u8], index: usize) -> u8 { + bytes[index] +}