From d00cb421e2aa7858f8ba6a6be5093b2f766730fe Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 8 Oct 2026 21:45:14 -0400 Subject: [PATCH] Verify the byte writers used by IntoBytes The public IntoBytes write methods previously kept their length selection inside pointer-bearing code. Route exact, prefix and suffix writes through extracted byte helpers so Lean checks the production decisions and complete destination updates. Prove acceptance, unchanged rejection and preservation of untouched regions. Compose the public big-endian word constructor and byte accessor with the prefix writer. Keep the typed-to-byte conversion and valid-reference conditions as explicit Rust premises. Add a self-contained offset-copy boundary with a source-bound, guarded interpretation and negative controls. This avoids the pinned backend's unsupported suffix reconstruction, which would otherwise lose the destination prefix. Regression tests exercise the public write methods. gherrit-pr-id: Gkipiolhcatlfs5igrsox32w4yivfp7k3 Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/ADMISSION_DESIGN.md | 21 ++- verification/aeneas/external.json | 1 + verification/aeneas/golden/Funs.lean | 66 +++++++- .../aeneas/golden/FunsExternal_Template.lean | 17 +- verification/aeneas/golden/Types.lean | 2 +- .../aeneas/lean/Obligations/ByteWrite.lean | 51 ++++++ .../aeneas/lean/Proofs/ByteWrite.lean | 127 +++++++++++++++ .../RequiredModelContracts/ByteWrite.lean | 55 +++++++ verification/aeneas/lean/SafetyTests.lean | 7 + .../aeneas/lean/Zerocopy/FunsExternal.lean | 17 ++ verification/aeneas/projections/Specs.lean | 40 +++++ zerocopy/src/lib.rs | 48 +----- zerocopy/src/util/bytewrite/mod.rs | 153 ++++++++++++++++++ zerocopy/src/util/mod.rs | 26 +++ 14 files changed, 579 insertions(+), 52 deletions(-) create mode 100644 verification/aeneas/lean/Obligations/ByteWrite.lean create mode 100644 verification/aeneas/lean/Proofs/ByteWrite.lean create mode 100644 verification/aeneas/lean/RequiredModelContracts/ByteWrite.lean create mode 100644 zerocopy/src/util/bytewrite/mod.rs diff --git a/verification/aeneas/ADMISSION_DESIGN.md b/verification/aeneas/ADMISSION_DESIGN.md index 0f9968be5d..16a1ff1a1b 100644 --- a/verification/aeneas/ADMISSION_DESIGN.md +++ b/verification/aeneas/ADMISSION_DESIGN.md @@ -35,7 +35,7 @@ storage, and general memory observations remain unsupported. Valid incoming references and Aeneas's reviewed borrow translation are explicit premises. `external.json` supplies exact reviewed leaves, including standard-library -builtins and two local unsafe helpers. Local opaque body hashes are checked +builtins and narrow local byte operations. Local opaque body hashes are checked against Rust-parser body boundaries. The only admitted generic transmutation instantiation is `u8 -> bool`; its interpretation rejects all other bytes and instantiations. Byte copying has explicit input and updated-output slices and @@ -46,6 +46,25 @@ 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 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 +rejection. The offset-copy boundary checks `start <= dst.len()` first, matching +Rust's checked subslicing, then requires `src.len() <= dst.len() - start` for the +unsafe copy. Its successful result is the original prefix, the source, and the +original suffix. Incoming slice references provide initialized bytes, access +permissions, disjointness, and allocation lifetime, just as for `copy_unchecked`. +The boundary's Rust body subslices and directly calls `copy_nonoverlapping`. +Keeping that body self-contained makes its source hash cover the actual pointer +operation; a change to another local helper cannot silently change its meaning. + +The pinned backend's `SliceIndexRangeFromUsizeSlice.get_mut` reconstructs a +modified suffix incorrectly: it prepends the modified suffix to the old suffix +instead of retaining the original prefix. That builtin remains unregistered. +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. + 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 e55775fc28..8f79f04bda 100644 --- a/verification/aeneas/external.json +++ b/verification/aeneas/external.json @@ -23,6 +23,7 @@ {"rust": "core::option::{core::option::Option}::unwrap", "signature": {"unsafe": false, "inputs": ["core::option::Option"], "output": "T0", "types": 1, "consts": 0}, "lean": "core.option.Option.unwrap"}, {"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": "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 c55c1bd583..a8d818d0c1 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -425,6 +425,13 @@ def byteorder.U32.from_bytes (O : Type) (bytes : Array Std.U8 4#usize) : Result (byteorder.U32 O) := do ok { _0 := bytes, _1 := core.marker.PhantomData.mk } +/-- [zerocopy::byteorder::{zerocopy::byteorder::U16}::to_bytes]: + Source: 'src/byteorder.rs', lines 578:12-580:13 + Visibility: public -/ +def byteorder.U16.to_bytes + {O : Type} (self : byteorder.U16 O) : Result (Array Std.U8 2#usize) := do + ok self._0 + /-- [zerocopy::byteorder::{zerocopy::byteorder::U16}::new]: Source: 'src/util/macros.rs', lines 568:21-568:88 Visibility: public -/ @@ -799,6 +806,57 @@ def trait_checks.check_array_into_bytes : Result Unit := do trait_checks.require_into_bytes (Array.Insts.ZerocopyIntoBytes 3#usize (Array.Insts.ZerocopyIntoBytes 2#usize Bool.Insts.ZerocopyIntoBytes)) +/-- [zerocopy::util::bytewrite::exact]: + Source: 'src/util/bytewrite/mod.rs', lines 27:0-37:1 -/ +def util.bytewrite.exact + (src : Slice Std.U8) (dst : Slice Std.U8) : + Result (Bool × (Slice Std.U8)) + := do + let i := Slice.len dst + let i1 := Slice.len src + if i = i1 + then let dst1 ← util.copy_unchecked src dst + ok (true, dst1) + else ok (false, dst) + +/-- [zerocopy::util::bytewrite::prefix]: + Source: 'src/util/bytewrite/mod.rs', lines 48:0-57:1 -/ +def util.bytewrite.prefix + (src : Slice Std.U8) (dst : Slice Std.U8) : + Result (Bool × (Slice Std.U8)) + := do + let i := Slice.len src + let i1 := Slice.len dst + if i <= i1 + then let dst1 ← util.copy_unchecked src dst + ok (true, dst1) + else ok (false, dst) + +/-- [zerocopy::util::bytewrite::suffix]: + Source: 'src/util/bytewrite/mod.rs', lines 68:0-79:1 -/ +def util.bytewrite.suffix + (src : Slice Std.U8) (dst : Slice Std.U8) : + Result (Bool × (Slice Std.U8)) + := do + let i := Slice.len dst + let i1 := Slice.len src + let o ← lift (Usize.checked_sub i i1) + match o with + | none => ok (false, dst) + | some start => + let dst1 ← util.copy_unchecked_at src dst start + ok (true, dst1) + +/-- [zerocopy::util::bytewrite::be_word_prefix]: + Source: 'src/util/bytewrite/mod.rs', lines 93:0-96:1 -/ +def util.bytewrite.be_word_prefix + (n : Std.U16) (dst : Slice Std.U8) : Result (Bool × (Slice Std.U8)) := do + let value ← + byteorder.U16.new byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder n + let a ← byteorder.U16.to_bytes value + let s ← lift (Array.to_slice a) + util.bytewrite.prefix s dst + /-- [zerocopy::impls::_::{impl zerocopy::FromZeros for ()}::only_derive_is_allowed_to_implement_this_trait]: Source: 'src/util/macros.rs', lines 165:8-165:62 Visibility: public -/ @@ -2015,7 +2073,7 @@ def core.cell.UnsafeCell.Insts.ZerocopyIntoBytes {T : Type} (IntoBytesInst : } /-- [zerocopy::util::padding_needed_for]: - Source: 'src/util/mod.rs', lines 166:0-226:1 -/ + Source: 'src/util/mod.rs', lines 167:0-227:1 -/ def util.padding_needed_for (len : Std.Usize) (align : core.num.nonzero.NonZero Std.Usize @@ -2031,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 253:0-271:1 -/ + Source: 'src/util/mod.rs', lines 254:0-272:1 -/ def util.round_down_to_next_multiple_of_alignment (n : Std.Usize) (align : core.num.nonzero.NonZero Std.Usize @@ -2048,7 +2106,7 @@ def util.round_down_to_next_multiple_of_alignment ok (n &&& mask) /-- [zerocopy::util::max]: - Source: 'src/util/mod.rs', lines 280:0-286:1 -/ + Source: 'src/util/mod.rs', lines 281:0-287:1 -/ def util.max (a : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner) @@ -2068,7 +2126,7 @@ def util.max else ok a /-- [zerocopy::util::min]: - Source: 'src/util/mod.rs', lines 295:0-301:1 -/ + Source: 'src/util/mod.rs', lines 296:0-302:1 -/ def util.min (a : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner) diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean index 598b7d38a4..ce24b5be06 100644 --- a/verification/aeneas/golden/FunsExternal_Template.lean +++ b/verification/aeneas/golden/FunsExternal_Template.lean @@ -63,6 +63,16 @@ axiom core.num.nonzero.NonZero.get core.num.nonzero.ZeroablePrimitive T Clause0_NonZeroInner) : core.num.nonzero.NonZero T Clause0_NonZeroInner → Result T +/-- [zerocopy::util::copy_unchecked]: + Source: 'src/util/mod.rs', lines 314:0-329: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 -/ +axiom util.copy_unchecked_at + : Slice Std.U8 → Slice Std.U8 → Std.Usize → Result (Slice Std.U8) + /-- [zerocopy::impls::_::{impl zerocopy::TryFromBytes for ()}::is_safe]: Source: 'src/util/macros.rs', lines 155:8-160:9 Visibility: public -/ @@ -119,12 +129,7 @@ axiom Array.Insts.ZerocopyTryFromBytes.is_safe pointer.invariant.Shared Alignment pointer.invariant.Initialized → Result Bool -/-- [zerocopy::util::copy_unchecked]: - Source: 'src/util/mod.rs', lines 313:0-328:1 -/ -axiom util.copy_unchecked - : Slice Std.U8 → Slice Std.U8 → Result (Slice Std.U8) - /-- [zerocopy::util::transmute_unchecked]: - Source: 'src/util/mod.rs', lines 340:0-369:1 -/ + Source: 'src/util/mod.rs', lines 366:0-395:1 -/ axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index 64ea9516f1..752b98e928 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -261,7 +261,7 @@ structure FromBytes (Self : Type) where only_derive_is_allowed_to_implement_this_trait : Result Unit /-- Trait declaration: [zerocopy::IntoBytes] - Source: 'src/lib.rs', lines 5953:0-6458:1 + Source: 'src/lib.rs', lines 5953:0-6426:1 Visibility: public -/ structure IntoBytes (Self : Type) where only_derive_is_allowed_to_implement_this_trait : Result Unit diff --git a/verification/aeneas/lean/Obligations/ByteWrite.lean b/verification/aeneas/lean/Obligations/ByteWrite.lean new file mode 100644 index 0000000000..3f73d6b748 --- /dev/null +++ b/verification/aeneas/lean/Obligations/ByteWrite.lean @@ -0,0 +1,51 @@ +/- 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 +public import Rust.Bytes +@[expose] public section +open Aeneas Aeneas.Std +namespace Zerocopy.Obligations + +-- Retain all raw inputs, including unsuccessful and empty writes. These +-- expectations are independent of the specification macro and its decoders. +def write_exact_spec_contract (src dst : Slice U8) + (run : Result (Bool × Slice U8)) : Prop := + run ⦃ out => out.1 = decide (src.val.length = dst.val.length) ∧ + out.2.val = if src.val.length = dst.val.length then src.val else dst.val ⦄ + +def write_prefix_spec_contract (src dst : Slice U8) + (run : Result (Bool × Slice U8)) : Prop := + run ⦃ out => out.1 = decide (src.val.length ≤ dst.val.length) ∧ + out.2.val = if src.val.length ≤ dst.val.length + then src.val ++ dst.val.drop src.val.length else dst.val ⦄ + +def write_suffix_spec_contract (src dst : Slice U8) + (run : Result (Bool × Slice U8)) : Prop := + run ⦃ out => out.1 = decide (src.val.length ≤ dst.val.length) ∧ + out.2.val = if src.val.length ≤ dst.val.length + then dst.val.take (dst.val.length - src.val.length) ++ src.val else dst.val ⦄ + +def write_exact_spec : Prop := + ∀ src dst, write_exact_spec_contract src dst (util.bytewrite.exact src dst) +def write_prefix_spec : Prop := + ∀ src dst, write_prefix_spec_contract src dst (util.bytewrite.prefix src dst) +def write_suffix_spec : Prop := + ∀ src dst, write_suffix_spec_contract src dst (util.bytewrite.suffix src dst) + +def write_be_word_prefix_spec_contract (n : U16) (dst : Slice U8) + (run : Result (Bool × Slice U8)) : Prop := + run ⦃ out => out.1 = decide (2 ≤ dst.val.length) ∧ + out.2.val.map U8.bv = if 2 ≤ dst.val.length + then Rust.Bytes.encodeBE 2 n.val ++ (dst.val.drop 2).map U8.bv + else dst.val.map U8.bv ⦄ +def write_be_word_prefix_spec : Prop := + ∀ n dst, write_be_word_prefix_spec_contract n dst (util.bytewrite.be_word_prefix n dst) + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs/ByteWrite.lean b/verification/aeneas/lean/Proofs/ByteWrite.lean new file mode 100644 index 0000000000..3543ed3bbb --- /dev/null +++ b/verification/aeneas/lean/Proofs/ByteWrite.lean @@ -0,0 +1,127 @@ +/- 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 Proofs.Byteorder +@[expose] public section + +/-! +These functions are the size selection and byte-copy implementation called by +IntoBytes's three public write methods. The proofs include unsuccessful writes +and the unaffected destination region, rather than merely checking copied bytes. +The source-bound copy interpretations retain the reference premises documented +in ADMISSION_DESIGN.md; their pointer implementations are not extracted. +-/ +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +private theorem decode_write (out : Bool × Slice U8) : + (inferInstance : RustModel (Bool × Slice U8)).decode out = + some (out.1, byteSlice out.2) := by + have decoded := decode_byte_slice out.2 + simp only [RustModel.decode] at decoded ⊢ + rw [decoded] + +theorem write_exact_raw (src dst : Slice U8) : + util.bytewrite.exact src dst ⦃ out => + out.1 = decide (src.val.length = dst.val.length) ∧ + out.2.val = if src.val.length = dst.val.length then src.val else dst.val ⦄ := by + by_cases same : src.val.length = dst.val.length + · simp [util.bytewrite.exact, Slice.len, + util.copy_unchecked, same, bind_ok] + · simp [util.bytewrite.exact, Slice.len, same, Ne.symm same] + +theorem write_prefix_raw (src dst : Slice U8) : + util.bytewrite.prefix src dst ⦃ out => + out.1 = decide (src.val.length ≤ dst.val.length) ∧ + out.2.val = if src.val.length ≤ dst.val.length + then src.val ++ dst.val.drop src.val.length else dst.val ⦄ := by + by_cases fits : src.val.length ≤ dst.val.length + · simp [util.bytewrite.prefix, Slice.len, UScalar.le_equiv, + util.copy_unchecked, fits, bind_ok] + · simp [util.bytewrite.prefix, Slice.len, UScalar.le_equiv, fits] + +theorem write_suffix_raw (src dst : Slice U8) : + util.bytewrite.suffix src dst ⦃ out => + out.1 = decide (src.val.length ≤ dst.val.length) ∧ + out.2.val = if src.val.length ≤ dst.val.length + then dst.val.take (dst.val.length - src.val.length) ++ src.val else dst.val ⦄ := by + unfold util.bytewrite.suffix + step as ⟨start, facts⟩ + cases start with + | none => + have unfit : ¬ src.val.length ≤ dst.val.length := by simpa [Slice.len] using facts + simp [unfit] + | some start => + have bounds : start.val = dst.val.length - src.val.length ∧ + src.val.length ≤ dst.val.length := by + simp only [Slice.len] at facts + exact ⟨facts.2.1, facts.1⟩ + have offset : start.val ≤ dst.val.length := by omega + have fits : src.val.length ≤ dst.val.length - start.val := by omega + have finish : start.val + src.val.length = dst.val.length := by omega + simp only [util.copy_unchecked_at, if_pos offset, dif_pos fits, bind_ok, WP.spec_ok] + simp [bounds.1, bounds.2] + +-- The concrete consumer uses the public byteorder operations, then the same +-- prefix writer as IntoBytes. Reuse the proved encoder rather than recalculate +-- its bitvector arithmetic inside this caller proof. +theorem write_be_word_prefix_raw (n : U16) (dst : Slice U8) : + util.bytewrite.be_word_prefix n dst ⦃ out => + out.1 = decide (2 ≤ dst.val.length) ∧ + out.2.val.map U8.bv = if 2 ≤ dst.val.length + then Rust.Bytes.encodeBE 2 n.val ++ (dst.val.drop 2).map U8.bv + else dst.val.map U8.bv ⦄ := by + have encoding_eq : (do + let value ← byteorder.U16.new byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder n + byteorder.U16.to_bytes value) = byteorder.verification.write_u16_be n := by + simp only [byteorder.verification.write_u16_be, core.convert.IntoFrom.into, + ArrayU82.Insts.CoreConvertFromU16.from, + byteorder.U16.to_bytes] + unfold util.bytewrite.be_word_prefix + rw [← Aeneas.Std.bind_assoc, encoding_eq] + step with Raw.write_u16_be n as ⟨bytes, encoded⟩ + simp only [lift, bind_ok] + apply WP.spec_mono (write_prefix_raw (Array.to_slice bytes) dst) + intro out facts + have length : bytes.val.length = 2 := by simp + simp only [Array.to_slice, Slice.from_val, length] at facts + refine ⟨facts.1, ?_⟩ + by_cases fits : 2 ≤ dst.val.length + · simp only [if_pos fits] at facts ⊢ + rw [facts.2, List.map_append, encoded] + · simp only [if_neg fits] at facts ⊢ + rw [facts.2] + +theorem write_exact_spec : Specs.write_exact_spec := by + intro src dst _ _ _ _ + apply WP.spec_mono (write_exact_raw src dst) + intro out facts + exact ⟨(out.1, byteSlice out.2), decode_write out, facts⟩ + +theorem write_prefix_spec : Specs.write_prefix_spec := by + intro src dst _ _ _ _ + apply WP.spec_mono (write_prefix_raw src dst) + intro out facts + exact ⟨(out.1, byteSlice out.2), decode_write out, facts⟩ + +theorem write_suffix_spec : Specs.write_suffix_spec := by + intro src dst _ _ _ _ + apply WP.spec_mono (write_suffix_raw src dst) + intro out facts + exact ⟨(out.1, byteSlice out.2), decode_write out, facts⟩ + +theorem write_be_word_prefix_spec : Specs.write_be_word_prefix_spec := by + intro n dst _ _ _ _ + apply WP.spec_mono (write_be_word_prefix_raw n dst) + intro out facts + exact ⟨(out.1, byteSlice out.2), decode_write out, facts⟩ + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RequiredModelContracts/ByteWrite.lean b/verification/aeneas/lean/RequiredModelContracts/ByteWrite.lean new file mode 100644 index 0000000000..79cf69d5b7 --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/ByteWrite.lean @@ -0,0 +1,55 @@ +/- 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.ByteWrite +public import Obligations.ByteWrite +@[expose] public section +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +-- Challenge each contract with an arbitrary execution outcome. Using only the +-- actual function's good behavior here could hide an accidentally weaker spec. +@[contract_simps] theorem required_write_exact (src dst : Slice U8) + (run : Result (Bool × Slice U8)) + (provided : Specs.write_exact_spec_contract src dst run) : + Obligations.write_exact_spec_contract src dst run := by + apply WP.spec_mono (provided (byteSlice src) (decode_byte_slice src) + (byteSlice dst) (decode_byte_slice dst)) + rintro out ⟨_, _, facts⟩ + exact facts + +@[contract_simps] theorem required_write_prefix (src dst : Slice U8) + (run : Result (Bool × Slice U8)) + (provided : Specs.write_prefix_spec_contract src dst run) : + Obligations.write_prefix_spec_contract src dst run := by + apply WP.spec_mono (provided (byteSlice src) (decode_byte_slice src) + (byteSlice dst) (decode_byte_slice dst)) + rintro out ⟨_, _, facts⟩ + exact facts + +@[contract_simps] theorem required_write_suffix (src dst : Slice U8) + (run : Result (Bool × Slice U8)) + (provided : Specs.write_suffix_spec_contract src dst run) : + Obligations.write_suffix_spec_contract src dst run := by + apply WP.spec_mono (provided (byteSlice src) (decode_byte_slice src) + (byteSlice dst) (decode_byte_slice dst)) + rintro out ⟨_, _, facts⟩ + exact facts + +@[contract_simps] theorem required_write_be_word_prefix (n : U16) (dst : Slice U8) + (run : Result (Bool × Slice U8)) + (provided : Specs.write_be_word_prefix_spec_contract n dst run) : + Obligations.write_be_word_prefix_spec_contract n dst run := by + apply WP.spec_mono (provided (unsignedWord n) rfl + (byteSlice dst) (decode_byte_slice dst)) + rintro out ⟨_, _, facts⟩ + exact facts + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/SafetyTests.lean b/verification/aeneas/lean/SafetyTests.lean index ec86c7c89e..e374074266 100644 --- a/verification/aeneas/lean/SafetyTests.lean +++ b/verification/aeneas/lean/SafetyTests.lean @@ -31,6 +31,13 @@ theorem copy_rejects_oversize (src dst : Slice U8) util.copy_unchecked src dst = .fail .undef := by simp [util.copy_unchecked, Zerocopy.forbiddenExecution, Nat.not_le.mpr oversize] +theorem offset_copy_rejects_oversize (src dst : Slice U8) (start : Usize) + (inside : start.val ≤ dst.val.length) + (oversize : dst.val.length - start.val < src.val.length) : + util.copy_unchecked_at src dst start = .fail .undef := by + simp [util.copy_unchecked_at, Zerocopy.forbiddenExecution, inside, + Nat.not_le.mpr oversize] + -- 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 f2eb383889..6b58a42033 100644 --- a/verification/aeneas/lean/Zerocopy/FunsExternal.lean +++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean @@ -90,6 +90,23 @@ def util.copy_unchecked (src dst : Slice U8) : Result (Slice U8) := omega)) else forbiddenExecution +-- The offset copy has the same reference premises. Check bounds before +-- constructing a subslice, and preserve BOTH untouched regions. A start past +-- the end panics at Rust's checked subslicing; an oversized copy is forbidden. +-- FIXME: Pinned SliceIndexRangeFromUsizeSlice.get_mut reconstructs its output +-- incorrectly (ca282ec, Aeneas/Std/Slice.lean). Do not admit that builtin until +-- its prefix-preservation law has been repaired and checked independently. +def util.copy_unchecked_at (src dst : Slice U8) (start : Usize) : Result (Slice U8) := + if start.val ≤ dst.val.length then + if h : src.val.length ≤ dst.val.length - start.val then + .ok (Slice.from + (dst.val.take start.val ++ src.val ++ dst.val.drop (start.val + src.val.length)) (by + have := dst.property + simp only [List.length_append, List.length_take, List.length_drop] + omega)) + else forbiddenExecution + 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 diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index e789f38735..febac5a7e4 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/verification/aeneas/projections/Specs.lean @@ -160,6 +160,46 @@ spec array_into_bytes_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.array_into_bytes_spec for Zerocopy.trait_checks.check_array_into_bytes with 0 +check_model_inputs Zerocopy.util.bytewrite.exact with 0 type parameters +aeneas_spec_begin +spec write_exact_spec + for @Zerocopy.util.bytewrite.exact with 0 type parameters + ensures(raw) out => out.1 = decide (src.val.length = dst.val.length) ∧ + out.2.val = if src.val.length = dst.val.length then src.val else dst.val +aeneas_spec_end +check_spec_binding Zerocopy.Specs.write_exact_spec for Zerocopy.util.bytewrite.exact with 2 + +check_model_inputs Zerocopy.util.bytewrite.prefix with 0 type parameters +aeneas_spec_begin +spec write_prefix_spec + for @Zerocopy.util.bytewrite.prefix with 0 type parameters + ensures(raw) out => out.1 = decide (src.val.length ≤ dst.val.length) ∧ + out.2.val = if src.val.length ≤ dst.val.length + then src.val ++ dst.val.drop src.val.length else dst.val +aeneas_spec_end +check_spec_binding Zerocopy.Specs.write_prefix_spec for Zerocopy.util.bytewrite.prefix with 2 + +check_model_inputs Zerocopy.util.bytewrite.suffix with 0 type parameters +aeneas_spec_begin +spec write_suffix_spec + for @Zerocopy.util.bytewrite.suffix with 0 type parameters + ensures(raw) out => out.1 = decide (src.val.length ≤ dst.val.length) ∧ + out.2.val = if src.val.length ≤ dst.val.length + then dst.val.take (dst.val.length - src.val.length) ++ src.val else dst.val +aeneas_spec_end +check_spec_binding Zerocopy.Specs.write_suffix_spec for Zerocopy.util.bytewrite.suffix with 2 + +check_model_inputs Zerocopy.util.bytewrite.be_word_prefix with 0 type parameters +aeneas_spec_begin +spec write_be_word_prefix_spec + for @Zerocopy.util.bytewrite.be_word_prefix with 0 type parameters + ensures(raw) out => out.1 = decide (2 ≤ dst.val.length) ∧ + out.2.val.map (fun byte => byte.bv) = if 2 ≤ dst.val.length + then Rust.Bytes.encodeBE 2 n.val ++ (dst.val.drop 2).map (fun byte => byte.bv) + else dst.val.map (fun byte => byte.bv) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.write_be_word_prefix_spec for Zerocopy.util.bytewrite.be_word_prefix with 2 + check_model_inputs Zerocopy.util.padding_needed_for with 0 type parameters aeneas_spec_begin spec padding_lt_alignment diff --git a/zerocopy/src/lib.rs b/zerocopy/src/lib.rs index 595b0c449d..6fb83f7a1a 100644 --- a/zerocopy/src/lib.rs +++ b/zerocopy/src/lib.rs @@ -6190,13 +6190,7 @@ pub unsafe trait IntoBytes { where Self: Immutable, { - let src = self.as_bytes(); - if dst.len() == src.len() { - // SAFETY: Within this branch of the conditional, we have ensured - // that `dst.len()` is equal to `src.len()`. Neither the size of the - // source nor the size of the destination change between the above - // size check and the invocation of `copy_unchecked`. - unsafe { util::copy_unchecked(src, dst) } + if util::bytewrite::exact(self.as_bytes(), dst) { Ok(()) } else { Err(SizeError::new(self)) @@ -6276,18 +6270,10 @@ pub unsafe trait IntoBytes { where Self: Immutable, { - let src = self.as_bytes(); - match dst.get_mut(..src.len()) { - Some(dst) => { - // SAFETY: Within this branch of the `match`, we have ensured - // through fallible subslicing that `dst.len()` is equal to - // `src.len()`. Neither the size of the source nor the size of - // the destination change between the above subslicing operation - // and the invocation of `copy_unchecked`. - unsafe { util::copy_unchecked(src, dst) } - Ok(()) - } - None => Err(SizeError::new(self)), + if util::bytewrite::prefix(self.as_bytes(), dst) { + Ok(()) + } else { + Err(SizeError::new(self)) } } @@ -6371,29 +6357,11 @@ pub unsafe trait IntoBytes { where Self: Immutable, { - let src = self.as_bytes(); - let start = if let Some(start) = dst.len().checked_sub(src.len()) { - start - } else { - return Err(SizeError::new(self)); - }; - let dst = if let Some(dst) = dst.get_mut(start..) { - dst + if util::bytewrite::suffix(self.as_bytes(), dst) { + Ok(()) } else { - // get_mut() should never return None here. We return a `SizeError` - // rather than .unwrap() because in the event the branch is not - // optimized away, returning a value is generally lighter-weight - // than panicking. - return Err(SizeError::new(self)); - }; - // SAFETY: Through fallible subslicing of `dst`, we have ensured that - // `dst.len()` is equal to `src.len()`. Neither the size of the source - // nor the size of the destination change between the above subslicing - // operation and the invocation of `copy_unchecked`. - unsafe { - util::copy_unchecked(src, dst); + Err(SizeError::new(self)) } - Ok(()) } /// Writes a copy of `self` to an `io::Write`. diff --git a/zerocopy/src/util/bytewrite/mod.rs b/zerocopy/src/util/bytewrite/mod.rs new file mode 100644 index 0000000000..edbdfbaeb4 --- /dev/null +++ b/zerocopy/src/util/bytewrite/mod.rs @@ -0,0 +1,153 @@ +// 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. + +//! The byte-writing part of `IntoBytes`. +//! +//! Keeping size selection here lets Lean check the code used by all three +//! public methods. Obtaining `src` from a typed value remains the separate +//! `IntoBytes::as_bytes` safety argument. These functions receive valid slice +//! references, so they need not reconstruct allocation lifetime or provenance. + +/// Writes the whole destination, rejecting unequal lengths without mutation. +/// +/// ```aeneas +/// spec write_exact_spec +/// ensures(raw) out => out.1 = decide (src.val.length = dst.val.length) ∧ +/// out.2.val = if src.val.length = dst.val.length then src.val else dst.val +/// ``` +#[inline] +pub(crate) fn exact(src: &[u8], dst: &mut [u8]) -> bool { + if dst.len() == src.len() { + // SAFETY: Equal lengths imply the helper's length requirement. The + // input references supply an initialized source and exclusive + // destination, and neither length changes before the copy. + unsafe { super::copy_unchecked(src, dst) }; + true + } else { + false + } +} + +/// Writes a fitting prefix, preserving the suffix and rejecting without mutation. +/// +/// ```aeneas +/// spec write_prefix_spec +/// ensures(raw) out => out.1 = decide (src.val.length ≤ dst.val.length) ∧ +/// out.2.val = if src.val.length ≤ dst.val.length +/// then src.val ++ dst.val.drop src.val.length else dst.val +/// ``` +#[inline] +pub(crate) fn prefix(src: &[u8], dst: &mut [u8]) -> bool { + if src.len() <= dst.len() { + // SAFETY: This branch establishes the helper's sole extra requirement. + // It copies only src.len() bytes, leaving the destination suffix alone. + unsafe { super::copy_unchecked(src, dst) }; + true + } else { + false + } +} + +/// Writes a fitting suffix, preserving the prefix and rejecting without mutation. +/// +/// ```aeneas +/// spec write_suffix_spec +/// ensures(raw) out => out.1 = decide (src.val.length ≤ dst.val.length) ∧ +/// out.2.val = if src.val.length ≤ dst.val.length +/// then dst.val.take (dst.val.length - src.val.length) ++ src.val else dst.val +/// ``` +#[inline] +pub(crate) fn suffix(src: &[u8], dst: &mut [u8]) -> bool { + let start = if let Some(start) = dst.len().checked_sub(src.len()) { + start + } else { + return false; + }; + // SAFETY: Successful subtraction gives start <= dst.len() and + // src.len() == dst.len() - start. The input references provide the source + // and destination access conditions required by copy_unchecked_at. + unsafe { super::copy_unchecked_at(src, dst, start) }; + true +} + +/// A concrete padding-free consumer: encode a big-endian word using the public +/// byteorder constructor/accessor, then run the production prefix writer. +/// The tests below compare this composition with `IntoBytes::write_to_prefix`. +/// +/// ```aeneas +/// spec write_be_word_prefix_spec +/// ensures(raw) out => out.1 = decide (2 ≤ dst.val.length) ∧ +/// out.2.val.map (fun byte => byte.bv) = if 2 ≤ dst.val.length +/// then Rust.Bytes.encodeBE 2 n.val ++ (dst.val.drop 2).map (fun byte => byte.bv) +/// else dst.val.map (fun byte => byte.bv) +/// ``` +#[allow(dead_code)] +fn be_word_prefix(n: u16, dst: &mut [u8]) -> bool { + let value = crate::byteorder::big_endian::U16::new(n); + prefix(&value.to_bytes(), dst) +} + +#[cfg(test)] +mod tests { + use crate::{byteorder::big_endian::U16, IntoBytes}; + + // These exercise the public methods, including their typed-to-byte bridge. + // Lean checks the shared selection/copying code; these regression tests + // additionally catch a public method wired to the wrong selection helper. + #[test] + fn public_writes() { + let value = U16::from_bytes([1, 2]); + for length in 0..=4 { + for mode in 0..3 { + let mut storage = [9, 8, 7, 6]; + let dst = &mut storage[..length]; + let accepted = match mode { + 0 => value.write_to(dst).is_ok(), + 1 => value.write_to_prefix(dst).is_ok(), + _ => value.write_to_suffix(dst).is_ok(), + }; + let fits = if mode == 0 { length == 2 } else { length >= 2 }; + assert_eq!(accepted, fits); + let mut expected = [9, 8, 7, 6]; + if fits { + let start = if mode == 2 { length - 2 } else { 0 }; + expected[start..start + 2].copy_from_slice(&[1, 2]); + } + assert_eq!(storage, expected); + } + } + } + + #[test] + fn empty_writes() { + let value: [u8; 0] = []; + let mut dst = [9; 3]; + value.write_to(&mut []).unwrap(); + value.write_to(&mut dst).unwrap_err(); + value.write_to_prefix(&mut dst).unwrap(); + value.write_to_suffix(&mut dst).unwrap(); + assert_eq!(dst, [9; 3]); + } + + #[test] + fn concrete_word_consumer() { + for n in [0, 1, 255, 256, u16::MAX] { + for length in 0..=4 { + let mut via_array = [9, 8, 7, 6]; + let mut via_into_bytes = via_array; + let accepted = super::be_word_prefix(n, &mut via_array[..length]); + let value = U16::new(n); + assert_eq!(accepted, value.write_to_prefix(&mut via_into_bytes[..length]).is_ok()); + assert_eq!(via_array, via_into_bytes); + } + } + } +} diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs index e9167686c1..f4c53b4428 100644 --- a/zerocopy/src/util/mod.rs +++ b/zerocopy/src/util/mod.rs @@ -14,6 +14,7 @@ pub(crate) mod macros; #[doc(hidden)] pub mod macro_util; +pub(crate) mod bytewrite; #[cfg(target_endian = "little")] #[allow(dead_code)] mod owned_transmute; @@ -327,6 +328,31 @@ pub(crate) unsafe fn copy_unchecked(src: &[u8], dst: &mut [u8]) { }; } +/// Copies `src` into `dst` beginning at byte `start`. +/// +/// This is a separate reviewed Aeneas boundary, using the same byte-copy +/// contract as `copy_unchecked`. The model checks the subslice bounds and +/// retains both untouched regions of the destination. +/// +/// # Safety +/// +/// The caller guarantees `start <= dst.len()` and +/// `src.len() <= dst.len() - start`. +#[inline(always)] +#[allow(clippy::indexing_slicing)] // The caller promises an in-bounds start. +pub(crate) unsafe fn copy_unchecked_at(src: &[u8], dst: &mut [u8], start: usize) { + let dst = &mut dst[start..]; + // Keep this trusted boundary self-contained: its body hash also covers the + // actual pointer operation, rather than hiding a mutable local dependency. + // SAFETY: The caller guarantees enough bytes in this subslice. The source + // reference supplies initialized readable bytes; the mutable destination + // supplies writable, disjoint bytes. Byte alignment is one, and subslicing + // retains the destination's allocation and exclusive access. + unsafe { + core::ptr::copy_nonoverlapping(src.as_ptr(), dst.as_mut_ptr(), src.len()); + }; +} + /// Unsafely transmutes the given `src` into a type `Dst`. /// /// Aeneas admits only the `u8` to `bool` instantiation as a trusted boundary