@@ -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
 
@@ -23,6 +23,7 @@
   {"rust": "core::option::{core::option::Option<T0>}::unwrap", "signature": {"unsafe": false, "inputs": ["core::option::Option<T0>"], "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"},
 
@@ -424,6 +424,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<O>}::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<O>}::new]:
     Source: 'src/util/macros.rs', lines 568:21-568:88
     Visibility: public -/
@@ -791,6 +798,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::_#1::{impl zerocopy::IntoBytes for i8}::only_derive_is_allowed_to_implement_this_trait]:
     Source: 'src/util/macros.rs', lines 165:8-165:62
     Visibility: public -/
@@ -1750,7 +1808,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
@@ -1766,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 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
@@ -1783,7 +1841,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)
@@ -1803,7 +1861,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)
 
@@ -58,11 +58,16 @@ 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 313:0-328:1 -/
+    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 340:0-351: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 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
 
@@ -178,7 +178,7 @@ structure byteorder.F64 (O : Type) where
   _1 : core.marker.PhantomData O
 
 /-- Trait declaration: [zerocopy::IntoBytes]
-    Source: 'src/lib.rs', lines 5941:0-6446:1
+    Source: 'src/lib.rs', lines 5941:0-6414:1
     Visibility: public -/
 structure IntoBytes (Self : Type) where
   only_derive_is_allowed_to_implement_this_trait : Result Unit
 
@@ -0,0 +1,51 @@
+/- 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
+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
@@ -0,0 +1,127 @@
+/- 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 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