Prove guarded Boolean conversion and byte copying

tools/aeneas-inline/src/main.rs

@@ -129,7 +129,8 @@ impl Functions<'_> {
                     supported &= receiver.reference.is_none() || receiver.mutability.is_none();
                 }
                 syn::FnArg::Typed(input) => {
-                    supported &= !unsupported_borrow(&input.ty, true);
+                    supported &=
+                        !unsupported_borrow(&input.ty, true) || mutable_byte_slice(&input.ty);
                     match input.pat.as_ref() {
                         syn::Pat::Ident(pattern)
                             if pattern.by_ref.is_none() && pattern.subpat.is_none() =>
@@ -298,6 +299,17 @@ fn unsupported_borrow(ty: &syn::Type, allow_shared: bool) -> bool {
     visitor.found
 }
 
+// Aeneas returns this mutable input as ordinary updated byte-slice state.
+// This narrow shape has no nested loans, stored references, or escaping borrow
+// transformer. Other mutable inputs remain unsupported until their returned
+// state and reconstruction semantics have an explicit audit.
+fn mutable_byte_slice(ty: &syn::Type) -> bool {
+    let syn::Type::Reference(reference) = ty else { return false };
+    let syn::Type::Slice(slice) = reference.elem.as_ref() else { return false };
+    let syn::Type::Path(element) = slice.elem.as_ref() else { return false };
+    reference.mutability.is_some() && element.qself.is_none() && element.path.is_ident("u8")
+}
+
 fn has_borrowed_fields(fields: &Value) -> bool {
     // Struct fields and enum variants share the report's recursive container
     // shape. A borrowed field in any variant makes the nominal owner unsupported.

verification/aeneas/README.md

@@ -168,6 +168,31 @@ builtin correspondence also remains part of the pinned translator's trust
 boundary. See [ADMISSION_DESIGN.md](ADMISSION_DESIGN.md) for the implemented
 fragment and [LOWERING_AUDIT.md](LOWERING_AUDIT.md) for the erasure inventory.
 
+The first storage examples are in
+[`util/safety_checks/mod.rs`](../../zerocopy/src/util/safety_checks/mod.rs):
+
+- `checked_bool` accepts exactly byte encodings 0 and 1 and rejects all others.
+- `checked_copy` copies a fitting prefix, preserves the suffix, and leaves the
+  entire destination unchanged when the source is too long. Its model returns
+  the updated mutable slice explicitly.
+
+The existing production `add_scaled_metadata` exercises guarded unchecked
+addition and multiplication. Each of these four primitive definitions has an
+independent complete-definition check, including its forbidden branch. Kernel
+controls prove rejection even if an invalid result is discarded or followed by
+divergence. Extraction controls check actual generated callers that discard an
+invalid Boolean or reach it before a loop. Mutation controls also challenge the
+failure tag and helper guards.
+
+Incoming references must already denote valid Rust allocations with the
+necessary exclusivity and initializedness. Logical byte lists do not establish
+provenance, allocation lifetime, or reference validity. Both storage examples
+use padding-free `u8`/`bool`; general padding and typed-copy effects remain
+unsupported. No panic-catching, thread, callback, or failure-recovery model is
+admitted. Both today's total and partial contracts reject *every* execution
+failure, including source UB aborts whose tag the pinned importer merges with
+panic. Supporting a recovery handler would require preserving that distinction.
+
 The binding manifest records both inspected snapshots, their dependency
 closures, exact registry identity, sources, compiler configuration, and patched
 runtime. Inputs are captured before compilation and checked again during binding

verification/aeneas/control_runner.py

@@ -26,7 +26,7 @@
 import tempfile
 import time
 
-FAMILIES = ('authoring', 'trait-rounding', 'unsafe', 'coverage', 'abi',
+FAMILIES = ('producers', 'authoring', 'trait-rounding', 'unsafe', 'coverage', 'abi',
             'contracts', 'dependencies', 'admission', 'semantics')
 MODELS = ('golden-verification', 'verification')
 FIXTURES = ('NegativeControl.lean', 'WeakOutcome.lean',

verification/aeneas/golden/Funs.lean

@@ -65,7 +65,7 @@ def Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner :
 }
 
 /-- [zerocopy::util::padding_needed_for]:
-    Source: 'src/util/mod.rs', lines 161:0-221:1 -/
+    Source: 'src/util/mod.rs', lines 163:0-223:1 -/
 def util.padding_needed_for
   (len : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -81,7 +81,7 @@ def util.padding_needed_for
   ok (i2 &&& mask)
 
 /-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
-    Source: 'src/util/mod.rs', lines 248:0-266:1 -/
+    Source: 'src/util/mod.rs', lines 250:0-268:1 -/
 def util.round_down_to_next_multiple_of_alignment
   (n : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -98,7 +98,7 @@ def util.round_down_to_next_multiple_of_alignment
   ok (n &&& mask)
 
 /-- [zerocopy::util::max]:
-    Source: 'src/util/mod.rs', lines 275:0-281:1 -/
+    Source: 'src/util/mod.rs', lines 277:0-283:1 -/
 def util.max
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -118,7 +118,7 @@ def util.max
   else ok a
 
 /-- [zerocopy::util::min]:
-    Source: 'src/util/mod.rs', lines 290:0-296:1 -/
+    Source: 'src/util/mod.rs', lines 292:0-298:1 -/
 def util.min
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -137,4 +137,26 @@ def util.min
   then ok b
   else ok a
 
+/-- [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)
+  else ok none
+
+/-- [zerocopy::util::safety_checks::checked_copy]:
+    Source: 'src/util/safety_checks/mod.rs', lines 51:0-61:1 -/
+def util.safety_checks.checked_copy
+  (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)
+
 end Zerocopy

verification/aeneas/golden/FunsExternal_Template.lean

@@ -50,3 +50,12 @@ 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 310:0-325: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 337:0-366:1 -/
+axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst
+

verification/aeneas/lean/Check.lean

@@ -63,6 +63,31 @@ run_elab do
       throwError "Missing external size read"
     unless ← Meta.isDefEq (mkConst `core.mem.size_of) sizeRead do
       throwError "External size read changed its data-input interpretation"
+  if env.contains `util.transmute_unchecked then
+    let expected ← Term.elabTerm (← `(fun {Src : Type} (Dst : Type) (src : Src) => by
+      classical
+      exact if hs : Src = Aeneas.Std.U8 then
+        if hd : Dst = Bool then
+          let byte := cast hs src
+          if byte.val < 2 then Aeneas.Std.Result.ok (cast hd.symm (decide (byte.val = 1)))
+          else Aeneas.Std.Result.fail Aeneas.Std.Error.undef
+        else Aeneas.Std.Result.fail Aeneas.Std.Error.undef
+      else Aeneas.Std.Result.fail Aeneas.Std.Error.undef)) none
+    Term.synthesizeSyntheticMVarsNoPostponing
+    unless ← Meta.isDefEq (mkConst `util.transmute_unchecked) (← instantiateMVars expected) do
+      throwError "External Boolean conversion changed its complete interpretation"
+  if env.contains `util.copy_unchecked then
+    let expected ← Term.elabTerm (← `(fun (src dst : Aeneas.Std.Slice Aeneas.Std.U8) =>
+      if h : src.val.length ≤ dst.val.length then
+        Aeneas.Std.Result.ok (Aeneas.Std.Slice.from
+          (src.val ++ dst.val.drop src.val.length) (by
+            have := dst.property
+            simp only [List.length_append, List.length_drop]
+            omega))
+      else Aeneas.Std.Result.fail Aeneas.Std.Error.undef)) none
+    Term.synthesizeSyntheticMVarsNoPostponing
+    unless ← Meta.isDefEq (mkConst `util.copy_unchecked) (← instantiateMVars expected) do
+      throwError "External byte copy changed its complete interpretation"
   -- Module indices identify declarations by compiled ownership. A matching
   -- namespace is insufficient: a generated or unrelated module could otherwise
   -- install a theorem under a handwritten proof's expected name.

verification/aeneas/lean/Obligations/SafetyChecks.lean

@@ -0,0 +1,32 @@
+/- Copyright 2026 The Fuchsia Authors
+
+Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+<LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+This file may not be copied, modified, or distributed except according to
+those terms. -/
+
+module
+public import Zerocopy
+@[expose] public section
+open Aeneas Aeneas.Std
+namespace Zerocopy.Obligations
+
+-- The independent expectations describe all inputs, including rejected bytes
+-- and insufficient destinations. They are propositions, not trusted axioms.
+def checked_bool_spec_contract (byte : U8) (run : Result (Option Bool)) : Prop :=
+  run ⦃ out => out = if byte.val < 2 then some (decide (byte.val = 1)) else none ⦄
+
+def checked_bool_spec : Prop :=
+  ∀ byte, checked_bool_spec_contract byte (util.safety_checks.checked_bool byte)
+
+def checked_copy_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 checked_copy_spec : Prop :=
+  ∀ src dst, checked_copy_spec_contract src dst (util.safety_checks.checked_copy src dst)
+
+end Zerocopy.Obligations

verification/aeneas/lean/Proofs/SafetyChecks.lean

@@ -0,0 +1,80 @@
+/- 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 ModelLemmas
+@[expose] public section
+
+/-!
+The callers establish the guards of the trusted conversion and copying helpers.
+These are proofs of composition, not proofs of the opaque Rust helper bodies.
+The result witnesses additionally check that the actual returned representation,
+including the updated mutable slice, decodes successfully.
+-/
+open Aeneas Aeneas.Std AeneasSpecs
+namespace Zerocopy.Proofs
+
+private theorem decode_bool_option (value : Option Bool) :
+    (inferInstance : RustModel (Option Bool)).decode value = some value := by
+  cases value <;> rfl
+
+private theorem decode_unsigned_list (values : List U8) :
+    decodeList (modelUScalar .U8).decode values = some (values.map unsignedWord) := by
+  induction values with
+  | nil => rfl
+  | cons head tail ih => simp [decodeList, ih]
+
+def byteSlice (raw : Slice U8) : SliceValue (UnsignedWord .U8) :=
+  ⟨raw.val.map unsignedWord, by simpa only [List.length_map] using raw.property⟩
+
+theorem decode_byte_slice (raw : Slice U8) :
+    (modelSlice (α := U8)).decode raw = some (byteSlice raw) := by
+  apply (decodeSlice_iff (modelUScalar .U8) raw (byteSlice raw)).mpr
+  exact decode_unsigned_list raw.val
+
+private theorem decode_copy_result (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 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,
+      UScalar.ofNatCore_val_eq, util.transmute_unchecked, valid, bind_ok]
+  · simp [util.safety_checks.checked_bool, UScalar.lt_equiv,
+      UScalar.ofNatCore_val_eq, valid]
+
+theorem checked_bool_spec : Specs.checked_bool_spec := by
+  intro byte _ _
+  apply WP.spec_mono (checked_bool_raw byte)
+  intro result same
+  exact ⟨result, decode_bool_option result, same⟩
+
+theorem checked_copy_raw (src dst : Slice U8) :
+    util.safety_checks.checked_copy 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.safety_checks.checked_copy, Slice.len, UScalar.le_equiv,
+      util.copy_unchecked, fits, bind_ok]
+  · simp [util.safety_checks.checked_copy, Slice.len, UScalar.le_equiv,
+      fits]
+
+theorem checked_copy_spec : Specs.checked_copy_spec := by
+  intro src dst _ _ _ _
+  apply WP.spec_mono (checked_copy_raw src dst)
+  intro result facts
+  exact ⟨(result.1, byteSlice result.2), decode_copy_result result, facts⟩
+
+end Zerocopy.Proofs

verification/aeneas/lean/RequiredModelContracts/SafetyChecks.lean

@@ -0,0 +1,37 @@
+/- 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 RequiredContracts
+public import Specs
+public import Proofs.SafetyChecks
+public import Obligations.SafetyChecks
+@[expose] public section
+open Aeneas Aeneas.Std AeneasSpecs
+namespace Zerocopy.Proofs
+
+-- These implications quantify over an arbitrary execution. They do not use
+-- the successful behavior of the extracted caller to strengthen its contract.
+@[contract_simps] theorem required_checked_bool (byte : U8)
+    (run : Result (Option Bool))
+    (provided : Specs.checked_bool_spec_contract byte run) :
+    Obligations.checked_bool_spec_contract byte run := by
+  apply WP.spec_mono (provided (unsignedWord byte) rfl)
+  rintro output ⟨_, _, facts⟩
+  exact facts
+
+@[contract_simps] theorem required_checked_copy (src dst : Slice U8)
+    (run : Result (Bool × Slice U8))
+    (provided : Specs.checked_copy_spec_contract src dst run) :
+    Obligations.checked_copy_spec_contract src dst run := by
+  apply WP.spec_mono (provided (byteSlice src) (decode_byte_slice src)
+    (byteSlice dst) (decode_byte_slice dst))
+  rintro output ⟨_, _, facts⟩
+  exact facts
+
+end Zerocopy.Proofs

verification/aeneas/lean/SafetyTests.lean

@@ -0,0 +1,58 @@
+/- 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 SpecsSyntax
+public import Zerocopy.Funs
+@[expose] public section
+open Aeneas Aeneas.Std AeneasSpecs
+namespace SafetyTests
+
+-- Sequencing cannot convert forbidden execution into either a value or
+-- divergence. In particular, discarding a callee's result is still sequencing.
+theorem forbidden_bind {α β : Type} (next : α → Result β) :
+    (Result.fail .undef >>= next) = Result.fail .undef := bind_fail .undef next
+
+theorem total_rejects_forbidden {α : Type} (post : α → Prop) :
+    ¬ WP.spec (.fail .undef) post := by simp
+
+theorem partial_rejects_forbidden {α : Type} (post : α → Prop) :
+    ¬ WP.dspec (.fail .undef) post := by simp
+
+-- Every oversized copy is forbidden, rather than success with truncated
+-- output or a recoverable None. The caller proves this branch unreachable.
+theorem copy_rejects_oversize (src dst : Slice U8)
+    (oversize : dst.val.length < src.val.length) :
+    util.copy_unchecked src dst = .fail .undef := by
+  simp [util.copy_unchecked, Zerocopy.forbiddenExecution, 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)
+
+theorem bad_bool_forbidden : badBool = .fail .undef := by
+  simp [badBool, util.transmute_unchecked, Zerocopy.forbiddenExecution, UScalar.val]
+
+noncomputable def discardCall : Result Unit := do let _ ← badBool; Result.ok ()
+noncomputable def failThenDiverge : Result Unit := do let _ ← badBool; Result.div
+def diverge : Result Unit := .div
+spec discarded for discardCall with 0 type parameters
+  ensures _ => True
+partial spec beforeDivergence for failThenDiverge with 0 type parameters
+  ensures _ => True
+
+example : ¬discarded := by simp [discarded, discardCall, bad_bool_forbidden]
+example : ¬beforeDivergence := by simp [beforeDivergence, failThenDiverge, bad_bool_forbidden]
+
+-- Even a contract that says nothing about the output must prove its execution
+-- judgment. Partial contracts permit divergence, but never preceding UB.
+partial spec diverges for diverge with 0 type parameters
+  ensures _ => True
+example : diverges := WP.dspec.div _
+
+end SafetyTests