Prove FromZeros::new_zeroed through its enclosing trait law

verification/aeneas/README.md

@@ -805,6 +805,14 @@ law. Negative Lean examples distinguish Boolean zero validity from Boolean
 validity for every byte, and reject zero construction of nonzero integers or a
 value rejected by its library decoder.
 
+The specification on the existing `FromZeros::new_zeroed` default method proves
+its actual body under the exact enclosing trait's law. Its stdlib boundary,
+`core::mem::zeroed`, decodes zero storage before returning a typed value;
+rejection is forbidden execution, even for a `True` postcondition. The compiled
+audit checks this complete definition, not just successful examples. An
+independent required contract states the physical and mathematical decoding
+facts without using the primitive's implementation.
+
 Aeneas normally has no model dictionary in the computation. The downstream
 `native_models` elaborator retains a provider only in generic definitions
 whose bodies need this boundary. Original Rust arguments remain in their exact
@@ -826,8 +834,8 @@ As with `IntoBytes`, applying these proofs to Rust assumes the physical decoder
 has the correct Rust width and language meaning. The primitive and array
 interpretations have explicit Reference premises; compiler assertions challenge
 the concrete widths. A generic provider is a supplied interpretation, not a
-proof of an arbitrary downstream type's representation. These construction laws
-cover the selected impls; they do not certify pointer access, external-state
+proof of an arbitrary downstream type's representation. This example covers
+resource-free owned zero construction, not pointer access, external-state
 invariants, destructors, or every `FromBytes`/`FromZeros` impl.
 
 ## Native Lean proofs and independent checks

verification/aeneas/control_runner.py

@@ -29,7 +29,7 @@
 FAMILIES = ('producers', 'authoring', 'trait-rounding', 'unsafe', 'coverage', 'abi',
             'contracts', 'dependencies', 'admission', 'semantics', 'owned-std')
 MODELS = ('golden-verification', 'verification')
-FIXTURES = ('StdTransmuteAuditProbe.lean', 'NegativeControl.lean', 'WeakOutcome.lean',
+FIXTURES = ('StdTransmuteAuditProbe.lean', 'ZeroedAuditProbe.lean', 'NegativeControl.lean', 'WeakOutcome.lean',
             'RoundingConstructorControl.lean', 'RoundingDomainControl.lean',
             'Zerocopy/ScopeControl.lean', 'Zerocopy/ShapeControl.lean',
             'Zerocopy/ModelControl.lean', 'Proofs/WitnessOwnerControl.lean',

verification/aeneas/golden/Funs.lean

@@ -644,7 +644,7 @@ def byteorder.verification.set_u32_be
   byteorder.U32.get byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder value1
 
 /-- [zerocopy::FromZeros::new_zeroed]:
-    Source: 'src/lib.rs', lines 3823:4-3829:5
+    Source: 'src/lib.rs', lines 3827:4-3833:5
     Visibility: public -/
 @[trait_default]
 native_models def FromZeros.new_zeroed.default (Self : Type) : Result Self := do

verification/aeneas/golden/Types.lean

@@ -246,22 +246,22 @@ structure TryFromBytes (Self : Type) where
     pointer.invariant.Initialized → Result Bool
 
 /-- Trait declaration: [zerocopy::FromZeros]
-    Source: 'src/lib.rs', lines 3708:0-4070:1
+    Source: 'src/lib.rs', lines 3708:0-4074:1
     Visibility: public -/
 structure FromZeros (Self : Type) where
   TryFromBytesInst : TryFromBytes Self
   only_derive_is_allowed_to_implement_this_trait : Result Unit
   new_zeroed : Result Self
 
 /-- Trait declaration: [zerocopy::FromBytes]
-    Source: 'src/lib.rs', lines 4298:0-5710:1
+    Source: 'src/lib.rs', lines 4302:0-5714:1
     Visibility: public -/
 structure FromBytes (Self : Type) where
   FromZerosInst : FromZeros Self
   only_derive_is_allowed_to_implement_this_trait : Result Unit
 
 /-- Trait declaration: [zerocopy::IntoBytes]
-    Source: 'src/lib.rs', lines 5949:0-6454:1
+    Source: 'src/lib.rs', lines 5953:0-6458:1
     Visibility: public -/
 structure IntoBytes (Self : Type) where
   only_derive_is_allowed_to_implement_this_trait : Result Unit

verification/aeneas/lean/Obligations/Zeroed.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 TraitLaws
+public import RustRepresentation
+@[expose] public section
+
+/-!
+The independent outcome family requires successful execution, an available
+physical decoder accepting the initialized all-zero representation, and an
+accepted mathematical value through the retained provider. It does not define
+the expected outcome in terms of the extracted default method or its guarded
+implementation. The concrete proposition specializes the same family to that
+method only after the arbitrary-outcome expectation has been stated.
+-/
+
+open Aeneas Aeneas.Std AeneasSpecs
+namespace Zerocopy.Obligations
+
+def new_zeroed_spec_contract (Self : Type) (meaning : RustModel Self)
+    (run : Result Self) : Prop :=
+  ∀ (dictionary : FromZeros Self) [_law : @TraitLaws.from_zeros_valid Self dictionary meaning],
+    ∃ raw value decoder, run = .ok raw ∧ meaning.representation = some decoder ∧
+      decoder.run (List.replicate decoder.byteSize (Rust.Storage.AMByte.init 0)) = some raw ∧
+      meaning.decode raw = some value
+
+def new_zeroed_spec : Prop :=
+  ∀ (Self : Type) [_meaning : RustModel Self],
+    new_zeroed_spec_contract Self _meaning (FromZeros.new_zeroed.default Self)
+
+end Zerocopy.Obligations

verification/aeneas/lean/Proofs/Zeroed.lean

@@ -0,0 +1,33 @@
+/- 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 RustRepresentation
+@[expose] public section
+
+/-!
+The production default method calls the guarded zero constructor with its
+retained semantic provider. Its enclosing FromZeros dictionary supplies zero
+admission; the returned raw value must also decode through that same provider.
+This proof does not infer that a moved raw value retains initialized padding.
+-/
+
+open Aeneas Aeneas.Std AeneasSpecs
+namespace Zerocopy.Proofs
+
+theorem new_zeroed_spec : Specs.new_zeroed_spec := by
+  intro Self meaning dictionary law
+  obtain ⟨raw, value, constructed, decoded⟩ := meaning.zeroedResult_admitted
+    (@TraitLaws.from_zeros_valid.holds Self dictionary meaning law)
+  change meaning.zeroedResult ⦃ output =>
+    ∃ mathematical, meaning.decode output = some mathematical ∧ meaning.zeroedResult = .ok output ⦄
+  rw [constructed]
+  exact ⟨value, decoded, rfl⟩
+
+end Zerocopy.Proofs

verification/aeneas/lean/RequiredModelContracts/Zeroed.lean

@@ -0,0 +1,30 @@
+/- 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 Obligations.Zeroed
+public import RequiredContracts
+@[expose] public section
+open Aeneas Aeneas.Std AeneasSpecs
+namespace Zerocopy.Proofs
+
+-- Compare arbitrary outcomes without assuming the function's own correctness.
+-- The expectation states each decoding stage instead of repeating zeroedValue.
+@[contract_simps] theorem required_new_zeroed (Self : Type) [meaning : RustModel Self]
+    (run : Result Self) (provided : Specs.new_zeroed_spec_contract Self run) :
+    Obligations.new_zeroed_spec_contract Self meaning run := by
+  intro dictionary law
+  obtain ⟨raw, executed, mathematical, decoded, zeroed⟩ :=
+    (WP.spec_equiv_exists run _).mp (provided dictionary)
+  obtain ⟨decoder, available, physical, _⟩ :=
+    (meaning.zeroedResult_eq_ok_iff raw).mp zeroed
+  exact ⟨raw, mathematical, decoder, executed, available, physical, decoded⟩
+
+
+end Zerocopy.Proofs

verification/aeneas/lean/ZeroedContractTests.lean

@@ -0,0 +1,45 @@
+/- 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 Proofs.Zeroed
+public import Proofs.FromBytes
+public import RequiredModelContracts.Zeroed
+@[expose] public section
+open Aeneas Aeneas.Std AeneasSpecs
+namespace Zerocopy.Proofs
+
+-- The independent expectation rejects failure, divergence, and a valid Boolean
+-- with the wrong value. These are model tests, not executions of invalid Rust.
+example : Obligations.new_zeroed_spec := by
+  intro Self meaning
+  exact required_new_zeroed Self (FromZeros.new_zeroed.default Self)
+    (new_zeroed_spec Self)
+
+example : ¬ @Obligations.new_zeroed_spec_contract Bool modelBool (.fail .undef) := by
+  intro expected
+  obtain ⟨raw, _, _, executed, _⟩ := expected Bool.Insts.ZerocopyFromZeros
+  simp at executed
+
+example : ¬ @Obligations.new_zeroed_spec_contract Bool modelBool .div := by
+  intro expected
+  obtain ⟨raw, _, _, executed, _⟩ := expected Bool.Insts.ZerocopyFromZeros
+  simp at executed
+
+example : ¬ @Obligations.new_zeroed_spec_contract Bool modelBool (.ok true) := by
+  intro expected
+  obtain ⟨raw, _, decoder, executed, available, physical, _⟩ :=
+    expected Bool.Insts.ZerocopyFromZeros
+  have same : raw = true := by simpa using executed.symm
+  subst raw
+  change some Rust.Storage.boolDecoder = some decoder at available
+  cases Option.some.inj available
+  change some false = some true at physical
+  contradiction
+
+end Zerocopy.Proofs

verification/aeneas/negative-control-family.sh

@@ -24,7 +24,7 @@ echo "Testing failure controls in $1"
 # suite starts and is removed on exit. Use the same roster for both decisions
 # so cleanup cannot delete a source that belonged to an earlier editor session.
 control_files=(
-    StdTransmuteAuditProbe.lean NegativeControl.lean WeakOutcome.lean
+    StdTransmuteAuditProbe.lean ZeroedAuditProbe.lean NegativeControl.lean WeakOutcome.lean
     RoundingConstructorControl.lean RoundingDomainControl.lean
     Zerocopy/ScopeControl.lean Zerocopy/ShapeControl.lean Zerocopy/ModelControl.lean
     Proofs/WitnessOwnerControl.lean Proofs/PaddingDependencyControl.lean
@@ -310,6 +310,12 @@ restore_build() {
 }
 
 if [[ $AENEAS_CONTROL_FAMILY == unsafe ]]; then
+# Exercise the new constructor's execution guard and exact retained decoder,
+# separately from its proof on valid inputs and its enclosing trait premise.
+if has_model FromZeros.new_zeroed.default; then
+    python3 -B "$repo/verification/aeneas/tests/zeroed_audit_controls.py" \
+        --work "$PWD" --runtime "$tools_dir" --evidence "$backup/zeroed"
+fi
 # Successful-input proofs cannot detect changing UB into an ordinary panic.
 # Check the independent primitive interpretation, then directly compile the
 # rejection examples so --old cannot replay a test from the unchanged model.

verification/aeneas/projections/Specs.lean

@@ -122,6 +122,15 @@ spec set_u32_be_spec
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.set_u32_be_spec for Zerocopy.byteorder.verification.set_u32_be with 2
 
+default_trait_body Zerocopy.FromZeros.new_zeroed.default for Zerocopy.FromZeros with 1 type parameters
+check_model_inputs Zerocopy.FromZeros.new_zeroed.default with 1 type parameters
+aeneas_spec_begin
+spec new_zeroed_spec
+  for @Zerocopy.FromZeros.new_zeroed.default with 1 type parameters
+  ensures(raw) r => AeneasSpecs.RustModel.zeroedValue r
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.new_zeroed_spec for Zerocopy.FromZeros.new_zeroed.default with 1
+
 check_model_inputs Zerocopy.trait_checks.byte_codec_roundtrip with 1 type parameters
 aeneas_spec_begin
 spec byte_codec_roundtrip_spec

verification/aeneas/projections/TraitLaws.lean

@@ -26,16 +26,16 @@ trait_dictionary @Zerocopy.FromZeros
 trait_dictionary @Zerocopy.FromBytes
 trait_dictionary @Zerocopy.IntoBytes
 trait_dictionary @Zerocopy.trait_checks.ByteCodec
+trait_invariant from_zeros_valid for @Zerocopy.FromZeros with 1 type parameters where self =>
+  AeneasSpecs.RustModel.zeroRepresentation Self
+
 trait_invariant byte_roundtrip for @Zerocopy.trait_checks.ByteCodec with 1 type parameters where self =>
   ∀ byte, (do let encoded ← self.encode byte; self.decode encoded)
       ⦃ result => result = byte ⦄
 
 trait_invariant into_bytes_initialized for @Zerocopy.IntoBytes with 1 type parameters where self =>
   AeneasSpecs.RustModel.initializedRepresentation Self
 
-trait_invariant from_zeros_valid for @Zerocopy.FromZeros with 1 type parameters where self =>
-  AeneasSpecs.RustModel.zeroRepresentation Self
-
 trait_invariant from_bytes_valid for @Zerocopy.FromBytes with 1 type parameters where self =>
   AeneasSpecs.RustModel.completeRepresentation Self