From b0f71c3923d6b366074f3f2398313f7676b96cf2 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Tue, 13 Oct 2026 17:12:37 -0400 Subject: [PATCH] Prove and consume the Unaligned alignment law Declare Unaligned's alignment-one promise in its Rust documentation. Prove the extracted built-in u8 implementation and exercise generic callers, callee-proof reuse, a concrete caller, and an unused bound whose law must remain in the theorem domain. Use that law to prove a zero-free unsafe NonZeroUsize construction followed by ordinary division. The guarded standard-library interpretation rejects zero as forbidden execution, even when a caller discards the result or subsequently diverges. The concrete byte caller discharges the selected implementation's law. Interpret the byte carrier's ABI alignment explicitly as one, checked by the native compile-time layout fixture. Other carriers retain the abstract alignment data input. The compiled audit checks that complete interpretation, so the byte theorem cannot silently constrain every generic alignment. Agent-authored-by: AI agent acting on joshlf's behalf gherrit-pr-id: Gw5blxfy2ukqgizynv5tybeaa67xgzkmj --- verification/aeneas/ADMISSION_DESIGN.md | 10 ++ verification/aeneas/DESIGN.md | 3 +- verification/aeneas/SEMANTICS.md | 9 +- verification/aeneas/external.json | 1 + verification/aeneas/golden/Funs.lean | 83 +++++++++++++-- .../aeneas/golden/FunsExternal_Template.lean | 11 ++ verification/aeneas/golden/Types.lean | 12 ++- .../aeneas/lean/NonZeroSafetyTests.lean | 70 ++++++++++++ .../aeneas/lean/Obligations/TraitChecks.lean | 46 ++++++++ .../aeneas/lean/Proofs/TraitChecks.lean | 100 ++++++++++++++---- .../RequiredModelContracts/TraitChecks.lean | 66 ++++++++++++ .../aeneas/lean/Zerocopy/FunsExternal.lean | 12 +++ .../aeneas/negative-control-extraction.sh | 4 + verification/aeneas/projections/Specs.lean | 48 +++++++++ .../aeneas/projections/TraitLaws.lean | 4 + .../tests/nonzero_instantiation_controls.py | 83 +++++++++++++++ zerocopy/src/lib.rs | 3 + zerocopy/src/trait_checks.rs | 80 +++++++++++++- 18 files changed, 608 insertions(+), 37 deletions(-) create mode 100644 verification/aeneas/lean/NonZeroSafetyTests.lean create mode 100644 verification/aeneas/tests/nonzero_instantiation_controls.py diff --git a/verification/aeneas/ADMISSION_DESIGN.md b/verification/aeneas/ADMISSION_DESIGN.md index 22755945b3..bb01b1d5df 100644 --- a/verification/aeneas/ADMISSION_DESIGN.md +++ b/verification/aeneas/ADMISSION_DESIGN.md @@ -46,6 +46,16 @@ 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 `Unaligned` trial admits only the standard-library `NonZeroUsize` +constructor boundary. Before and after lowering, admission checks its exact +unsafe signature and original `usize` instantiation. The native model guards +zero before constructing a wrapper and leaves it forbidden even if discarded. +The generic caller's extracted alignment read and both checked divisions remain +visible; its exact trait law establishes alignment one and the nonzero argument. +Kernel controls reject zero under total and partial `True` contracts and show +that an alignment-two model cannot establish either execution contract without +the law. No body of the new Rust caller is made opaque. + 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 diff --git a/verification/aeneas/DESIGN.md b/verification/aeneas/DESIGN.md index d46af833b1..b9aa5b58cf 100644 --- a/verification/aeneas/DESIGN.md +++ b/verification/aeneas/DESIGN.md @@ -329,7 +329,8 @@ the library already models every part of Rust's abstract machine. const generics, associated-type trait laws, higher-ranked bounds, bounded nominal models, and escaping borrow reconstruction remain unsupported with explicit errors. The first trait-law bridge supports `Self`-only traits and - simple generic bounds, with a total byte codec as a checked example. Add semantics and admission checks before accepting + simple generic bounds, with `Unaligned` and a total byte codec as checked + examples. Add semantics and admission checks before accepting them. Stateful or nondeterministic APIs may need observable traces and effects, rather than only result contracts. - **Abstract storage and bit validity.** Check byte-to-value production before diff --git a/verification/aeneas/SEMANTICS.md b/verification/aeneas/SEMANTICS.md index b831de5c9d..7ea7cde080 100644 --- a/verification/aeneas/SEMANTICS.md +++ b/verification/aeneas/SEMANTICS.md @@ -82,9 +82,14 @@ not to replace the universal algebra proof. ## External inputs and trust Aeneas erases ABI layout information from generic Rust type parameters. -`Zerocopy.RustLayout.size` and `Zerocopy.RustLayout.align` are therefore +`Zerocopy.RustLayout.size` and `Zerocopy.RustLayout.alignInput` are uninterpreted **data inputs**, each of type `Type → Usize`. No proposition -about their values is an axiom. The constructors' contracts explicitly +about their values is an axiom. `RustLayout.align` uses alignment one for the +concrete byte carrier `U8` and the abstract alignment input for every other +carrier. That byte interpretation is an explicit compiler-correspondence +premise, checked by a Rust compile-time assertion. It allows the concrete +`u8: Unaligned` dictionary to discharge its trait law without assuming that +all types have alignment one. The constructors' contracts explicitly require the relevant primitive reads and alignment properties. The audit admits exactly these two names and verifies their signatures. Changing an input to a proposition, or adding another axiom, fails the audit. diff --git a/verification/aeneas/external.json b/verification/aeneas/external.json index 4b04e20b84..f94eec62ef 100644 --- a/verification/aeneas/external.json +++ b/verification/aeneas/external.json @@ -5,6 +5,7 @@ {"rust": "core::num::{usize}::checked_mul", "signature": {"unsafe": false, "inputs": ["usize", "usize"], "output": "core::option::Option", "types": 0, "consts": 0}, "lean": "Usize.checked_mul"}, {"rust": "core::num::nonzero::{core::num::nonzero::NonZero}::get", "signature": {"unsafe": false, "inputs": ["core::num::nonzero::NonZero"], "output": "T0", "types": 2, "consts": 0}, "lean": "core.num.nonzero.NonZero.get", "before": {"rust": "core::num::nonzero::{core::num::nonzero::NonZero}::get", "signature": {"unsafe": false, "inputs": ["core::num::nonzero::NonZero"], "output": "T0", "types": 1, "consts": 0}}}, {"rust": "core::num::nonzero::{core::num::nonzero::NonZero}::new", "signature": {"unsafe": false, "inputs": ["T0"], "output": "core::option::Option>", "types": 2, "consts": 0}, "lean": "core.num.nonzero.NonZero.new", "before": {"rust": "core::num::nonzero::{core::num::nonzero::NonZero}::new", "signature": {"unsafe": false, "inputs": ["T0"], "output": "core::option::Option>", "types": 1, "consts": 0}}}, + {"rust": "core::num::nonzero::{core::num::nonzero::NonZero}::new_unchecked", "signature": {"unsafe": true, "inputs": ["T0"], "output": "core::num::nonzero::NonZero", "types": 2, "consts": 0}, "lean": "core.num.nonzero.NonZero.new_unchecked", "before": {"rust": "core::num::nonzero::{core::num::nonzero::NonZero}::new_unchecked", "signature": {"unsafe": true, "inputs": ["T0"], "output": "core::num::nonzero::NonZero", "types": 1, "consts": 0}}}, {"rust": "core::num::{usize}::checked_sub", "signature": {"unsafe": false, "inputs": ["usize", "usize"], "output": "core::option::Option", "types": 0, "consts": 0}, "lean": "Usize.checked_sub"}, {"rust": "core::fmt::{core::fmt::Arguments}::from_str", "signature": {"unsafe": false, "inputs": ["&str"], "output": "core::fmt::Arguments", "types": 0, "consts": 0}, "lean": "core.fmt.Arguments.from_str"}, {"rust": "core::slice::{[T0]}::len", "signature": {"unsafe": false, "inputs": ["&[T0]"], "output": "usize", "types": 1, "consts": 0}, "lean": "Slice.len"}, diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index 8ebf01c851..81d1617df7 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -1077,20 +1077,83 @@ def layout.primitive_checks.check_empty_layout native_models def FromZeros.new_zeroed.default (Self : Type) : Result Self := do core.mem.zeroed Self +/-- [zerocopy::trait_checks::unaligned_alignment]: + Source: 'src/trait_checks.rs', lines 25:0-27:1 -/ +def trait_checks.unaligned_alignment + {T : Type} (UnalignedInst : Unaligned T) : Result Std.Usize := do + core.mem.align_of T + +/-- [zerocopy::trait_checks::check_unaligned]: + Source: 'src/trait_checks.rs', lines 35:0-37:1 -/ +def trait_checks.check_unaligned + {T : Type} (UnalignedInst : Unaligned T) : Result Unit := do + let i ← trait_checks.unaligned_alignment UnalignedInst + massert (i = 1#usize) + +/-- [zerocopy::trait_checks::unused_unaligned_bound]: + Source: 'src/trait_checks.rs', lines 48:0-50:1 -/ +def trait_checks.unused_unaligned_bound + {T : Type} (UnalignedInst : Unaligned T) (value : Std.Usize) : + Result Std.Usize + := do + ok value + +/-- [zerocopy::impls::_#1::{impl zerocopy::Unaligned for u8}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def U8.Insts.ZerocopyUnaligned.only_derive_is_allowed_to_implement_this_trait + : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#1::{impl zerocopy::Unaligned for u8}] + Source: 'src/util/macros.rs', lines 30:8-32:9 -/ +@[reducible] +def U8.Insts.ZerocopyUnaligned : Unaligned Std.U8 := { + only_derive_is_allowed_to_implement_this_trait := + U8.Insts.ZerocopyUnaligned.only_derive_is_allowed_to_implement_this_trait +} + +/-- [zerocopy::trait_checks::check_byte_unaligned]: + Source: 'src/trait_checks.rs', lines 58:0-60:1 -/ +def trait_checks.check_byte_unaligned : Result Unit := do + trait_checks.check_unaligned U8.Insts.ZerocopyUnaligned + +/-- [zerocopy::trait_checks::divide_by_unaligned]: + Source: 'src/trait_checks.rs', lines 71:0-78:1 -/ +def trait_checks.divide_by_unaligned + {T : Type} (UnalignedInst : Unaligned T) (x : Std.Usize) : + Result Std.Usize + := do + let i ← core.mem.align_of T + let divisor ← 1#usize / i + let divisor1 ← + core.num.nonzero.NonZero.new_unchecked + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner divisor + let i1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner divisor1 + x / i1 + +/-- [zerocopy::trait_checks::divide_by_byte_alignment]: + Source: 'src/trait_checks.rs', lines 86:0-88:1 -/ +def trait_checks.divide_by_byte_alignment + (x : Std.Usize) : Result Std.Usize := do + trait_checks.divide_by_unaligned U8.Insts.ZerocopyUnaligned x + /-- [zerocopy::trait_checks::{impl zerocopy::trait_checks::ByteCodec for zerocopy::trait_checks::XorCodec}::decode]: - Source: 'src/trait_checks.rs', lines 41:4-43:5 -/ + Source: 'src/trait_checks.rs', lines 112:4-114:5 -/ def trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec.decode (byte : Std.U8) : Result Std.U8 := do ok (byte ^^^ 170#u8) /-- [zerocopy::trait_checks::{impl zerocopy::trait_checks::ByteCodec for zerocopy::trait_checks::XorCodec}::encode]: - Source: 'src/trait_checks.rs', lines 37:4-39:5 -/ + Source: 'src/trait_checks.rs', lines 108:4-110:5 -/ def trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec.encode (byte : Std.U8) : Result Std.U8 := do ok (byte ^^^ 170#u8) /-- Trait implementation: [zerocopy::trait_checks::{impl zerocopy::trait_checks::ByteCodec for zerocopy::trait_checks::XorCodec}] - Source: 'src/trait_checks.rs', lines 36:0-44:1 -/ + Source: 'src/trait_checks.rs', lines 107:0-115:1 -/ @[reducible] def trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec : trait_checks.ByteCodec trait_checks.XorCodec := { @@ -1099,7 +1162,7 @@ def trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec : } /-- [zerocopy::trait_checks::{impl zerocopy::trait_checks::ByteCodec for zerocopy::trait_checks::Forward}::decode]: - Source: 'src/trait_checks.rs', lines 54:4-56:5 -/ + Source: 'src/trait_checks.rs', lines 125:4-127:5 -/ def trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec.decode {C : Type} (ByteCodecInst : trait_checks.ByteCodec C) (byte : Std.U8) : Result Std.U8 @@ -1107,7 +1170,7 @@ def trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec.decode ByteCodecInst.decode byte /-- [zerocopy::trait_checks::{impl zerocopy::trait_checks::ByteCodec for zerocopy::trait_checks::Forward}::encode]: - Source: 'src/trait_checks.rs', lines 50:4-52:5 -/ + Source: 'src/trait_checks.rs', lines 121:4-123:5 -/ def trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec.encode {C : Type} (ByteCodecInst : trait_checks.ByteCodec C) (byte : Std.U8) : Result Std.U8 @@ -1115,7 +1178,7 @@ def trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec.encode ByteCodecInst.encode byte /-- Trait implementation: [zerocopy::trait_checks::{impl zerocopy::trait_checks::ByteCodec for zerocopy::trait_checks::Forward}] - Source: 'src/trait_checks.rs', lines 49:0-57:1 -/ + Source: 'src/trait_checks.rs', lines 120:0-128:1 -/ @[reducible] def trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec {C : Type} (ByteCodecInst : trait_checks.ByteCodec C) : trait_checks.ByteCodec @@ -1127,7 +1190,7 @@ def trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec {C : Type} } /-- [zerocopy::trait_checks::byte_codec_roundtrip]: - Source: 'src/trait_checks.rs', lines 63:0-65:1 -/ + Source: 'src/trait_checks.rs', lines 134:0-136:1 -/ def trait_checks.byte_codec_roundtrip {C : Type} (ByteCodecInst : trait_checks.ByteCodec C) (byte : Std.U8) : Result Std.U8 @@ -1136,14 +1199,14 @@ def trait_checks.byte_codec_roundtrip ByteCodecInst.decode i /-- [zerocopy::trait_checks::forwarded_byte_codec]: - Source: 'src/trait_checks.rs', lines 73:0-75:1 -/ + Source: 'src/trait_checks.rs', lines 144:0-146:1 -/ def trait_checks.forwarded_byte_codec (byte : Std.U8) : Result Std.U8 := do trait_checks.byte_codec_roundtrip (trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec) byte /-- [zerocopy::trait_checks::require_into_bytes]: - Source: 'src/trait_checks.rs', lines 77:0-77:47 -/ + Source: 'src/trait_checks.rs', lines 148:0-148:47 -/ def trait_checks.require_into_bytes {T : Type} (IntoBytesInst : IntoBytes T) : Result Unit := do ok () @@ -1213,7 +1276,7 @@ def Tuple.Insts.ZerocopyIntoBytes : IntoBytes Unit := { } /-- [zerocopy::trait_checks::check_array_into_bytes]: - Source: 'src/trait_checks.rs', lines 92:0-98:1 -/ + Source: 'src/trait_checks.rs', lines 163:0-169:1 -/ def trait_checks.check_array_into_bytes : Result Unit := do trait_checks.require_into_bytes (Array.Insts.ZerocopyIntoBytes 3#usize Bool.Insts.ZerocopyIntoBytes) diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean index 76ecc41466..3fbb32bf45 100644 --- a/verification/aeneas/golden/FunsExternal_Template.lean +++ b/verification/aeneas/golden/FunsExternal_Template.lean @@ -77,6 +77,17 @@ axiom core.num.nonzero.NonZero.new core.num.nonzero.ZeroablePrimitive T Clause0_NonZeroInner) : T → Result (Option (core.num.nonzero.NonZero T Clause0_NonZeroInner)) +/-- [core::num::nonzero::{core::num::nonzero::NonZero}::new_unchecked]: + Source: '/rustc/library/core/src/num/nonzero.rs', lines 405:4-405:51 + Name pattern: [core::num::nonzero::{core::num::nonzero::NonZero<@T, @Clause0_NonZeroInner>}::new_unchecked] + Visibility: public -/ +@[rust_fun + "core::num::nonzero::{core::num::nonzero::NonZero<@T, @Clause0_NonZeroInner>}::new_unchecked"] +axiom core.num.nonzero.NonZero.new_unchecked + {T : Type} {Clause0_NonZeroInner : Type} (ZeroablePrimitiveInst : + core.num.nonzero.ZeroablePrimitive T Clause0_NonZeroInner) : + T → Result (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] diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index a702da6d51..682dce8ab5 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -303,18 +303,24 @@ structure FromBytes (Self : Type) where structure IntoBytes (Self : Type) where only_derive_is_allowed_to_implement_this_trait : Result Unit +/-- Trait declaration: [zerocopy::Unaligned] + Source: 'src/lib.rs', lines 6564:0-6571:1 + Visibility: public -/ +structure Unaligned (Self : Type) where + only_derive_is_allowed_to_implement_this_trait : Result Unit + /-- Trait declaration: [zerocopy::trait_checks::ByteCodec] - Source: 'src/trait_checks.rs', lines 26:0-29:1 -/ + Source: 'src/trait_checks.rs', lines 97:0-100:1 -/ structure trait_checks.ByteCodec (Self : Type) where encode : Std.U8 → Result Std.U8 decode : Std.U8 → Result Std.U8 /-- [zerocopy::trait_checks::XorCodec] - Source: 'src/trait_checks.rs', lines 31:0-31:16 -/ + Source: 'src/trait_checks.rs', lines 102:0-102:16 -/ structure trait_checks.XorCodec where /-- [zerocopy::trait_checks::Forward] - Source: 'src/trait_checks.rs', lines 47:0-47:34 -/ + Source: 'src/trait_checks.rs', lines 118:0-118:34 -/ structure trait_checks.Forward (C : Type) where _0 : core.marker.PhantomData C diff --git a/verification/aeneas/lean/NonZeroSafetyTests.lean b/verification/aeneas/lean/NonZeroSafetyTests.lean new file mode 100644 index 0000000000..a351d2824b --- /dev/null +++ b/verification/aeneas/lean/NonZeroSafetyTests.lean @@ -0,0 +1,70 @@ +/- 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 SpecsSyntax +public import Zerocopy.Funs +@[expose] public section +open Aeneas Aeneas.Std AeneasSpecs Zerocopy +namespace NonZeroSafetyTests + +-- These are model executions, not attempts to execute undefined Rust. +noncomputable def zeroConstructor := + core.num.nonzero.NonZero.new_unchecked + Zerocopy.Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner (0#usize) + +theorem zero_forbidden : zeroConstructor = .fail .undef := by + simp [zeroConstructor, core.num.nonzero.NonZero.new_unchecked, + Zerocopy.forbiddenExecution] + +example : ¬ WP.spec zeroConstructor (fun _ => True) := by simp [zero_forbidden] +example : ¬ WP.dspec zeroConstructor (fun _ => True) := by simp [zero_forbidden] + +noncomputable def discardZero : Result Unit := do let _ ← zeroConstructor; .ok () +noncomputable def zeroBeforeDivergence : Result Unit := do let _ ← zeroConstructor; .div +spec discarded for discardZero with 0 type parameters + ensures _ => True +partial spec beforeDivergence for zeroBeforeDivergence with 0 type parameters + ensures _ => True + +example : ¬discarded := by simp [discarded, discardZero, zero_forbidden] +example : ¬beforeDivergence := by + simp [beforeDivergence, zeroBeforeDivergence, zero_forbidden] + +theorem unsupported_carrier_forbidden {T Inner : Type} + (inst : core.num.nonzero.ZeroablePrimitive T Inner) (x : T) (unsupported : T ≠ Usize) : + core.num.nonzero.NonZero.new_unchecked inst x = .fail .undef := by + simp [core.num.nonzero.NonZero.new_unchecked, unsupported, Zerocopy.forbiddenExecution] + +-- A native dictionary alone supplies no alignment proposition. Without its +-- law, an alignment-two model reaches a forbidden zero constructor. The +-- premise here is a counterfactual model value, not an extra Rust assumption. +theorem missing_law_forbidden (T : Type) (dictionary : Zerocopy.Unaligned T) (x : Usize) + (alignment : Zerocopy.RustLayout.align T = 2#usize) : + Zerocopy.trait_checks.divide_by_unaligned dictionary x = .fail .undef := by + have half : (1#usize / 2#usize : Result Usize) = .ok (0#usize) := by + obtain ⟨result, call, numeric⟩ := + UScalar.div_spec (1#usize) (y := 2#usize) (by scalar_tac) + have zero : result = 0#usize := by + apply UScalar.eq_of_val_eq + simpa using numeric + simpa only [zero] using call + simp [Zerocopy.trait_checks.divide_by_unaligned, core.mem.align_of, alignment, + half, core.num.nonzero.NonZero.new_unchecked, Zerocopy.forbiddenExecution] + +example (T : Type) (dictionary : Zerocopy.Unaligned T) (x : Usize) + (alignment : Zerocopy.RustLayout.align T = 2#usize) : + ¬ WP.spec (Zerocopy.trait_checks.divide_by_unaligned dictionary x) (fun _ => True) := by + simp [missing_law_forbidden T dictionary x alignment] + +example (T : Type) (dictionary : Zerocopy.Unaligned T) (x : Usize) + (alignment : Zerocopy.RustLayout.align T = 2#usize) : + ¬ WP.dspec (Zerocopy.trait_checks.divide_by_unaligned dictionary x) (fun _ => True) := by + simp [missing_law_forbidden T dictionary x alignment] + +end NonZeroSafetyTests diff --git a/verification/aeneas/lean/Obligations/TraitChecks.lean b/verification/aeneas/lean/Obligations/TraitChecks.lean index 0261867c00..78612aaab1 100644 --- a/verification/aeneas/lean/Obligations/TraitChecks.lean +++ b/verification/aeneas/lean/Obligations/TraitChecks.lean @@ -42,6 +42,52 @@ def array_into_bytes_spec_contract (run : Result Unit) : Prop := def array_into_bytes_spec : Prop := array_into_bytes_spec_contract trait_checks.check_array_into_bytes +def unaligned_alignment_spec_contract (T : Type) (dictionary : Unaligned T) + (run : Result Usize) : Prop := + TraitLaws.unaligned T dictionary → run ⦃ alignment => alignment = 1#usize ⦄ + +def unaligned_alignment_spec : Prop := + ∀ (T : Type) (dictionary : Unaligned T), + unaligned_alignment_spec_contract T dictionary (trait_checks.unaligned_alignment dictionary) + +def unaligned_check_spec_contract (T : Type) (dictionary : Unaligned T) + (run : Result Unit) : Prop := + TraitLaws.unaligned T dictionary → run ⦃ _ => True ⦄ + +def unaligned_check_spec : Prop := + ∀ (T : Type) (dictionary : Unaligned T), + unaligned_check_spec_contract T dictionary (trait_checks.check_unaligned dictionary) + +def unused_unaligned_bound_spec_contract (T : Type) (dictionary : Unaligned T) + (value : Usize) (run : Result Usize) : Prop := + TraitLaws.unaligned T dictionary → run ⦃ result => result = value ⦄ + +def unused_unaligned_bound_spec : Prop := + ∀ (T : Type) (dictionary : Unaligned T) (value : Usize), + unused_unaligned_bound_spec_contract T dictionary value + (trait_checks.unused_unaligned_bound dictionary value) + +def concrete_unaligned_check_spec_contract (run : Result Unit) : Prop := + run ⦃ _ => True ⦄ + +def concrete_unaligned_check_spec : Prop := + concrete_unaligned_check_spec_contract trait_checks.check_byte_unaligned + +def divide_by_unaligned_spec_contract (T : Type) (dictionary : Unaligned T) + (x : Usize) (run : Result Usize) : Prop := + TraitLaws.unaligned T dictionary → run ⦃ result => result = x ⦄ + +def divide_by_unaligned_spec : Prop := + ∀ (T : Type) (dictionary : Unaligned T) (x : Usize), + divide_by_unaligned_spec_contract T dictionary x + (trait_checks.divide_by_unaligned dictionary x) + +def divide_by_byte_alignment_spec_contract (x : Usize) (run : Result Usize) : Prop := + run ⦃ result => result = x ⦄ + +def divide_by_byte_alignment_spec : Prop := + ∀ (x : Usize), divide_by_byte_alignment_spec_contract x + (trait_checks.divide_by_byte_alignment x) def byte_codec_roundtrip_spec_contract (C : Type) (dictionary : trait_checks.ByteCodec C) (byte : U8) (run : Result U8) : Prop := diff --git a/verification/aeneas/lean/Proofs/TraitChecks.lean b/verification/aeneas/lean/Proofs/TraitChecks.lean index f2f2bb9085..e70eca529f 100644 --- a/verification/aeneas/lean/Proofs/TraitChecks.lean +++ b/verification/aeneas/lean/Proofs/TraitChecks.lean @@ -19,6 +19,32 @@ proves a total codec, and forwarding preserves only the supplied codec's law. open Aeneas Aeneas.Std AeneasSpecs namespace Zerocopy.Proofs +@[instance] theorem U8.Insts.ZerocopyUnaligned_law : + TraitLaws.unaligned Aeneas.Std.U8 Zerocopy.U8.Insts.ZerocopyUnaligned := + ⟨RustLayout.align_u8⟩ + +@[instance] theorem trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec_law : + TraitLaws.byte_roundtrip Zerocopy.trait_checks.XorCodec + Zerocopy.trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec := by + constructor + intro byte + simp only [Zerocopy.trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec.encode, + Zerocopy.trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec.decode, + bind_ok, WP.spec_ok] + apply UScalar.eq_of_val_eq + simp [UScalar.val_xor] + +@[instance] theorem trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec_law + {C : Type} (dictionary : Zerocopy.trait_checks.ByteCodec C) + [law : TraitLaws.byte_roundtrip C dictionary] : + TraitLaws.byte_roundtrip (Zerocopy.trait_checks.Forward C) + (Zerocopy.trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec dictionary) := by + constructor + simpa only [Zerocopy.trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec, + Zerocopy.trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec.encode, + Zerocopy.trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec.decode] + using (@TraitLaws.byte_roundtrip.holds C dictionary law) + -- These primitive byte interpretations follow Rust's validity and layout -- rules. The array law below uses those interpretations, not the optional -- library decoder's (possibly smaller) admission domain. @@ -68,28 +94,62 @@ theorem array_into_bytes_spec : Specs.array_into_bytes_spec := by (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Bool.Insts.ZerocopyIntoBytes)) _ inferInstance) +theorem unaligned_alignment_spec : Specs.unaligned_alignment_spec := by + intro T dictionary _ law + simp only [Zerocopy.trait_checks.unaligned_alignment, core.mem.align_of, WP.spec_ok] + refine ⟨unsignedWord (RustLayout.align T), rfl, ?_⟩ + rw [@TraitLaws.unaligned.holds T dictionary law] + simp [unsignedWord, UScalar.val] -@[instance] theorem trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec_law : - TraitLaws.byte_roundtrip Zerocopy.trait_checks.XorCodec - Zerocopy.trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec := by - constructor - intro byte - simp only [Zerocopy.trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec.encode, - Zerocopy.trait_checks.XorCodec.Insts.ZerocopyTrait_checksByteCodec.decode, - bind_ok, WP.spec_ok] - apply UScalar.eq_of_val_eq - simp [UScalar.val_xor] +theorem unaligned_check_spec : Specs.unaligned_check_spec := by + intro T dictionary _ law + unfold Zerocopy.trait_checks.check_unaligned + step with unaligned_alignment_spec T dictionary as ⟨alignment, mathematical, decoded, one⟩ + have same : alignment = 1#usize := by + apply UScalar.eq_of_val_eq + have numeric := (decodeUScalar_iff alignment _).mp decoded + change alignment.val = 1 + exact numeric.trans one + simp only [same, massert, ↓reduceIte, WP.spec_ok] + exact ⟨(), rfl⟩ -@[instance] theorem trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec_law - {C : Type} (dictionary : Zerocopy.trait_checks.ByteCodec C) - [law : TraitLaws.byte_roundtrip C dictionary] : - TraitLaws.byte_roundtrip (Zerocopy.trait_checks.Forward C) - (Zerocopy.trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec dictionary) := by - constructor - simpa only [Zerocopy.trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec, - Zerocopy.trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec.encode, - Zerocopy.trait_checks.Forward.Insts.ZerocopyTrait_checksByteCodec.decode] - using (@TraitLaws.byte_roundtrip.holds C dictionary law) +theorem unused_unaligned_bound_spec : Specs.unused_unaligned_bound_spec := by + intro T dictionary value _ law mathematical decoded + simp only [Zerocopy.trait_checks.unused_unaligned_bound, WP.spec_ok] + exact ⟨mathematical, decoded, rfl⟩ + +theorem concrete_unaligned_check_spec : Specs.concrete_unaligned_check_spec := by + simpa only [Specs.concrete_unaligned_check_spec, Zerocopy.trait_checks.check_byte_unaligned] + using (unaligned_check_spec Aeneas.Std.U8 Zerocopy.U8.Insts.ZerocopyUnaligned) + +-- Derive the computation from the backend's checked division theorem; no +-- constructor validity or trait fact is assumed by this arithmetic helper. +theorem usize_div_one (x : Usize) : (x / 1#usize : Result Usize) = .ok x := by + obtain ⟨result, call, numeric⟩ := UScalar.div_spec x (y := 1#usize) (by scalar_tac) + have same : result = x := by + apply UScalar.eq_of_val_eq + simpa using numeric + simpa only [same] using call + +@[step] theorem nonzero_usize_new_unchecked_spec (x : Usize) (nonzero : x ≠ 0#usize) : + core.num.nonzero.NonZero.new_unchecked + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner x + ⦃ result => result.val = x ⦄ := by + simp [core.num.nonzero.NonZero.new_unchecked, nonzero] + +theorem divide_by_unaligned_spec : Specs.divide_by_unaligned_spec := by + intro T dictionary x _ law mathematical decoded + simp only [Zerocopy.trait_checks.divide_by_unaligned, core.mem.align_of, bind_ok, + @TraitLaws.unaligned.holds T dictionary law, usize_div_one] + step with nonzero_usize_new_unchecked_spec (1#usize) (by scalar_tac) + as ⟨divisor, stored⟩ + simp only [core.num.nonzero.NonZero.get, bind_ok, stored, usize_div_one, WP.spec_ok] + exact decoded + +theorem divide_by_byte_alignment_spec : Specs.divide_by_byte_alignment_spec := by + intro x mathematical decoded + exact divide_by_unaligned_spec Aeneas.Std.U8 Zerocopy.U8.Insts.ZerocopyUnaligned + x mathematical decoded theorem byte_codec_roundtrip_spec : Specs.byte_codec_roundtrip_spec := by intro C dictionary byte _ law mathematical decoded diff --git a/verification/aeneas/lean/RequiredModelContracts/TraitChecks.lean b/verification/aeneas/lean/RequiredModelContracts/TraitChecks.lean index 2bd4230751..3dc1ee91bf 100644 --- a/verification/aeneas/lean/RequiredModelContracts/TraitChecks.lean +++ b/verification/aeneas/lean/RequiredModelContracts/TraitChecks.lean @@ -29,6 +29,49 @@ namespace Zerocopy.Proofs rintro _ ⟨_, _, boolean, byte, unit, empty, nested⟩ exact ⟨boolean, byte, unit, empty, nested⟩ +@[contract_simps] theorem required_unaligned_alignment (T : Type) (dictionary : Unaligned T) + (run : Result Usize) + (provided : Specs.unaligned_alignment_spec_contract T dictionary run) : + Obligations.unaligned_alignment_spec_contract T dictionary run := by + intro law + letI : RustModel T := { Model := T, «decode» := some } + letI := law + apply WP.spec_mono provided + rintro alignment ⟨mathematical, decoded, one⟩ + apply UScalar.eq_of_val_eq + have numeric := (decodeUScalar_iff alignment mathematical).mp decoded + change alignment.val = 1 + exact numeric.trans one + +@[contract_simps] theorem required_unaligned_check (T : Type) (dictionary : Unaligned T) + (run : Result Unit) (provided : Specs.unaligned_check_spec_contract T dictionary run) : + Obligations.unaligned_check_spec_contract T dictionary run := by + intro law + letI : RustModel T := { Model := T, «decode» := some } + letI := law + apply WP.spec_mono provided + intro _ _ + trivial + +@[contract_simps] theorem required_unused_unaligned_bound (T : Type) + (dictionary : Unaligned T) (value : Usize) (run : Result Usize) + (provided : Specs.unused_unaligned_bound_spec_contract T dictionary value run) : + Obligations.unused_unaligned_bound_spec_contract T dictionary value run := by + intro law + letI : RustModel T := { Model := T, «decode» := some } + letI := law + apply WP.spec_mono (provided (unsignedWord value) rfl) + rintro result ⟨mathematical, decoded, same⟩ + apply UScalar.eq_of_val_eq + exact ((decodeUScalar_iff result mathematical).mp decoded).trans + (congrArg UnsignedWord.value same) + +@[contract_simps] theorem required_concrete_unaligned_check (run : Result Unit) + (provided : Specs.concrete_unaligned_check_spec_contract run) : + Obligations.concrete_unaligned_check_spec_contract run := by + apply WP.spec_mono provided + intro _ _ + trivial @[contract_simps] theorem required_byte_codec_roundtrip (C : Type) (dictionary : trait_checks.ByteCodec C) (byte : U8) (run : Result U8) @@ -43,6 +86,29 @@ namespace Zerocopy.Proofs exact ((decodeUScalar_iff result mathematical).mp decoded).trans (congrArg UnsignedWord.value same) +@[contract_simps] theorem required_divide_by_unaligned (T : Type) + (dictionary : Unaligned T) (x : Usize) (run : Result Usize) + (provided : Specs.divide_by_unaligned_spec_contract T dictionary x run) : + Obligations.divide_by_unaligned_spec_contract T dictionary x run := by + intro law + letI : RustModel T := { Model := T, «decode» := some } + letI := law + apply WP.spec_mono (provided (unsignedWord x) rfl) + rintro result ⟨mathematical, decoded, same⟩ + apply UScalar.eq_of_val_eq + exact ((decodeUScalar_iff result mathematical).mp decoded).trans + (congrArg UnsignedWord.value same) + +@[contract_simps] theorem required_divide_by_byte_alignment (x : Usize) + (run : Result Usize) + (provided : Specs.divide_by_byte_alignment_spec_contract x run) : + Obligations.divide_by_byte_alignment_spec_contract x run := by + apply WP.spec_mono (provided (unsignedWord x) rfl) + rintro result ⟨mathematical, decoded, same⟩ + apply UScalar.eq_of_val_eq + exact ((decodeUScalar_iff result mathematical).mp decoded).trans + (congrArg UnsignedWord.value same) + @[contract_simps] theorem required_forwarded_byte_codec (byte : U8) (run : Result U8) (provided : Specs.forwarded_byte_codec_spec_contract byte run) : Obligations.forwarded_byte_codec_spec_contract byte run := by diff --git a/verification/aeneas/lean/Zerocopy/FunsExternal.lean b/verification/aeneas/lean/Zerocopy/FunsExternal.lean index d0de054abe..d2bbae06de 100644 --- a/verification/aeneas/lean/Zerocopy/FunsExternal.lean +++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean @@ -197,3 +197,15 @@ noncomputable def Zerocopy.RustLayout.align (T : Type) : Usize := by exact if h : T = Usize then if (cast h x : Usize) = 0#usize then .ok none else .ok (some ⟨x⟩) else forbiddenExecution + +-- The pinned std contract requires a nonzero argument. Guard the execution +-- before producing even a raw wrapper: zero is forbidden, including when a +-- caller discards the result. Only Usize is reviewed, and admission checks its +-- original Rust type and lifted NonZeroUsizeInner argument independently. +@[simp] noncomputable def core.num.nonzero.NonZero.new_unchecked + {T Inner : Type} (_inst : core.num.nonzero.ZeroablePrimitive T Inner) + (x : T) : Result (core.num.nonzero.NonZero T Inner) := by + classical + exact if h : T = Usize then + if (cast h x : Usize) = 0#usize then forbiddenExecution else .ok ⟨x⟩ + else forbiddenExecution diff --git a/verification/aeneas/negative-control-extraction.sh b/verification/aeneas/negative-control-extraction.sh index f0929e8e33..7078aea61a 100644 --- a/verification/aeneas/negative-control-extraction.sh +++ b/verification/aeneas/negative-control-extraction.sh @@ -33,6 +33,7 @@ manifest = json.loads(Path(sys.argv[1]).read_text()) if manifest.get('version') != 3 or manifest.get('mode') != 'verified-live': raise SystemExit('Invalid verified bindings for extraction controls') functions = {row['raw'] for row in manifest['bindings'].values() if row['kind'] == 'function'} +print('nonzero' if 'Zerocopy.trait_checks.divide_by_unaligned' in functions else '') print('storage' if 'Zerocopy.util.safety_checks.checked_bool' in functions else '') print('into-bytes' if any(row['rust'] == 'zerocopy::IntoBytes' for row in manifest['trait_laws']) else '') image = manifest.get('type_image') @@ -42,6 +43,9 @@ if not isinstance(image, list) or not all( print('unemitted' if any(row['category'] == 'unemitted-uninhabited' for row in image) else '') PY ) +if [[ $capabilities == *nonzero* ]]; then + run python3 -B verification/aeneas/tests/nonzero_instantiation_controls.py "$project" +fi if [[ $capabilities == *into-bytes* ]]; then run python3 -B verification/aeneas/tests/trait_const_binding_controls.py "$project" fi diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index ac4f3295d1..4f8e6712e9 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/verification/aeneas/projections/Specs.lean @@ -283,6 +283,54 @@ spec new_zeroed_spec 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.unaligned_alignment with 1 type parameters +aeneas_spec_begin +spec unaligned_alignment_spec + for @Zerocopy.trait_checks.unaligned_alignment with 1 type parameters + ensures alignment => (alignment : Nat) = 1 +aeneas_spec_end +check_spec_binding Zerocopy.Specs.unaligned_alignment_spec for Zerocopy.trait_checks.unaligned_alignment with 2 + +check_model_inputs Zerocopy.trait_checks.check_unaligned with 1 type parameters +aeneas_spec_begin +spec unaligned_check_spec + for @Zerocopy.trait_checks.check_unaligned with 1 type parameters + ensures _ => True +aeneas_spec_end +check_spec_binding Zerocopy.Specs.unaligned_check_spec for Zerocopy.trait_checks.check_unaligned with 2 + +check_model_inputs Zerocopy.trait_checks.unused_unaligned_bound with 1 type parameters +aeneas_spec_begin +spec unused_unaligned_bound_spec + for @Zerocopy.trait_checks.unused_unaligned_bound with 1 type parameters + ensures result => result = value +aeneas_spec_end +check_spec_binding Zerocopy.Specs.unused_unaligned_bound_spec for Zerocopy.trait_checks.unused_unaligned_bound with 3 + +check_model_inputs Zerocopy.trait_checks.check_byte_unaligned with 0 type parameters +aeneas_spec_begin +spec concrete_unaligned_check_spec + for @Zerocopy.trait_checks.check_byte_unaligned with 0 type parameters + ensures _ => True +aeneas_spec_end +check_spec_binding Zerocopy.Specs.concrete_unaligned_check_spec for Zerocopy.trait_checks.check_byte_unaligned with 0 + +check_model_inputs Zerocopy.trait_checks.divide_by_unaligned with 1 type parameters +aeneas_spec_begin +spec divide_by_unaligned_spec + for @Zerocopy.trait_checks.divide_by_unaligned with 1 type parameters + ensures result => result = x +aeneas_spec_end +check_spec_binding Zerocopy.Specs.divide_by_unaligned_spec for Zerocopy.trait_checks.divide_by_unaligned with 3 + +check_model_inputs Zerocopy.trait_checks.divide_by_byte_alignment with 0 type parameters +aeneas_spec_begin +spec divide_by_byte_alignment_spec + for @Zerocopy.trait_checks.divide_by_byte_alignment with 0 type parameters + ensures result => result = x +aeneas_spec_end +check_spec_binding Zerocopy.Specs.divide_by_byte_alignment_spec for Zerocopy.trait_checks.divide_by_byte_alignment with 1 + check_model_inputs Zerocopy.trait_checks.byte_codec_roundtrip with 1 type parameters aeneas_spec_begin spec byte_codec_roundtrip_spec diff --git a/verification/aeneas/projections/TraitLaws.lean b/verification/aeneas/projections/TraitLaws.lean index 5bdff2c8c2..152ded5181 100644 --- a/verification/aeneas/projections/TraitLaws.lean +++ b/verification/aeneas/projections/TraitLaws.lean @@ -26,10 +26,14 @@ trait_dictionary @Zerocopy.TryFromBytes trait_dictionary @Zerocopy.FromZeros trait_dictionary @Zerocopy.FromBytes trait_dictionary @Zerocopy.IntoBytes +trait_dictionary @Zerocopy.Unaligned 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 unaligned for @Zerocopy.Unaligned with 1 type parameters where self => + Zerocopy.RustLayout.align Self = 1#usize + 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 ⦄ diff --git a/verification/aeneas/tests/nonzero_instantiation_controls.py b/verification/aeneas/tests/nonzero_instantiation_controls.py new file mode 100644 index 0000000000..12b3452a0b --- /dev/null +++ b/verification/aeneas/tests/nonzero_instantiation_controls.py @@ -0,0 +1,83 @@ +# 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. + +"""Challenge the original Rust identities in a real pinned extraction. + +The lifted inner carrier is an alias in Lean. Changing its Rust identity must +still reject admission, independently of the model's native T = Usize guard. +Mutations stay in memory and never execute invalid Rust or rewrite snapshots. +""" +import copy +import json +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parents[3] +sys.path.insert(0, str(ROOT / 'verification/aeneas')) +import admission + + +def dictionaries(value): + if isinstance(value, dict): + yield value + for child in value.values(): + yield from dictionaries(child) + elif isinstance(value, list): + for child in value: + yield from dictionaries(child) + + +def main(work): + registry = json.loads((ROOT / 'verification/aeneas/external.json').read_text()) + manifest = json.loads((work / 'bindings.json').read_text()) + laws = [row['rust'] for row in manifest['trait_laws']] + root = 'zerocopy::trait_checks::divide_by_unaligned' + for stage, filename in [('before', 'zerocopy.before.ullbc'), ('llbc', 'zerocopy.llbc')]: + data = json.loads((work / filename).read_text()) + baseline = admission.Admission(data, registry, laws) + baseline.audit([root]) + # Match compiler paths without interpreting unrelated signature-only + # carriers. The positive root audit already checks its actual callee. + constructors = {index for index, function in baseline.functions.items() + if function['item_meta']['name'][-1] == {'Ident': ['new_unchecked', 0]}} + owner = next(function for function in baseline.functions.values() + if function['item_meta']['name'] == [{'Ident': [part, 0]} for part in root.split('::')]) + calls = [] + for node in dictionaries(owner['body']): + function = node.get('func', {}).get('Regular', {}) + if function.get('kind', {}).get('Fun') in constructors: + calls.append(function) + if len(calls) != 1: + raise ValueError(f'{stage}: expected exactly one actual constructor call') + original = calls[0]['generics']['types'] + original_values = copy.deepcopy(original) + expected_count = 1 if stage == 'before' else 2 + if len(original) != expected_count: + raise ValueError(f'{stage}: constructor generic prefix changed') + mutations = [('integer identity', 0, {'Untagged': {'Scalar': { + 'Integer': {'Unsigned': 'U8'}}}})] + if stage == 'llbc': + # Both carriers lower to Usize, but their original Rust identities + # differ. The guarded native definition cannot detect this change. + mutations.append(('lifted inner identity', 1, copy.deepcopy(original[0]))) + for label, index, replacement in mutations: + original[index] = replacement + try: + admission.Admission(data, registry, laws).audit([root]) + except ValueError as error: + if 'Unsupported NonZero::new_unchecked instantiation' not in str(error): + raise ValueError(f'{stage}: {label} failed outside its intended guard') from error + print(f'Confirmed: {stage} rejects changed {label}') + else: + raise ValueError(f'{stage}: accepted changed {label}') + finally: + original[index] = copy.deepcopy(original_values[index]) + + +if __name__ == '__main__': + main(Path(sys.argv[1]).resolve()) diff --git a/zerocopy/src/lib.rs b/zerocopy/src/lib.rs index 6fb83f7a1a..c3d3af1501 100644 --- a/zerocopy/src/lib.rs +++ b/zerocopy/src/lib.rs @@ -6558,6 +6558,9 @@ pub use zerocopy_derive::Unaligned; not(no_zerocopy_diagnostic_on_unimplemented_1_78_0), diagnostic::on_unimplemented(note = "Consider adding `#[derive(Unaligned)]` to `{Self}`") )] +/// ```aeneas +/// invariant unaligned for self => Zerocopy.RustLayout.align Self = 1#usize +/// ``` pub unsafe trait Unaligned { // The `Self: Sized` bound makes it so that `Unaligned` is still object // safe. diff --git a/zerocopy/src/trait_checks.rs b/zerocopy/src/trait_checks.rs index ed16535077..c44519b254 100644 --- a/zerocopy/src/trait_checks.rs +++ b/zerocopy/src/trait_checks.rs @@ -14,7 +14,78 @@ //! the law of its exact Rust dictionary. A concrete caller must discharge that //! law for the selected implementation before reusing the consumer. -use core::marker::PhantomData; +use core::{marker::PhantomData, mem, num::NonZeroUsize}; + +use crate::Unaligned; + +/// ```aeneas +/// spec unaligned_alignment_spec +/// ensures alignment => (alignment : Nat) = 1 +/// ``` +fn unaligned_alignment() -> usize { + mem::align_of::() +} + +/// The assertion consumes the callee's checked contract. +/// +/// ```aeneas +/// spec unaligned_check_spec +/// ensures _ => True +/// ``` +fn check_unaligned() { + assert!(unaligned_alignment::() == 1); +} + +/// An unused trait bound must still contribute its invariant. +/// +/// ```aeneas +/// spec unused_unaligned_bound_spec +/// ensures result => result = value +/// ``` +// Keep T unused so extraction must preserve the bound's law independently +// of runtime arguments or method calls. +#[allow(clippy::extra_unused_type_parameters)] +fn unused_unaligned_bound(value: usize) -> usize { + value +} + +/// This call also checks the concrete built-in `u8` implementation's law. +/// +/// ```aeneas +/// spec concrete_unaligned_check_spec +/// ensures _ => True +/// ``` +fn check_byte_unaligned() { + check_unaligned::(); +} + +/// Trait evidence establishes the unsafe constructor's precondition. +/// +/// ```aeneas +/// spec divide_by_unaligned_spec +/// ensures result => result = x +/// ``` +// Both divisions have divisor one by the Unaligned contract. +// Keep get explicit so extraction checks both standard-library boundaries. +#[allow(clippy::arithmetic_side_effects, clippy::needless_nonzero_get)] +fn divide_by_unaligned(x: usize) -> usize { + let divisor = 1 / mem::align_of::(); + // SAFETY: Unaligned requires T to have alignment one, so the preceding + // division computes 1 / 1 = 1. NonZeroUsize::new_unchecked requires a + // nonzero argument, which divisor = 1 satisfies. + let divisor = unsafe { NonZeroUsize::new_unchecked(divisor) }; + x / divisor.get() +} + +/// The concrete call discharges the actual built-in u8 dictionary's law. +/// +/// ```aeneas +/// spec divide_by_byte_alignment_spec +/// ensures result => result = x +/// ``` +fn divide_by_byte_alignment(x: usize) -> usize { + divide_by_unaligned::(x) +} /// Encoding and decoding form one total round trip on every byte. /// @@ -103,6 +174,13 @@ mod tests { #[test] fn trait_law_examples() { + check_byte_unaligned(); + assert_eq!(unaligned_alignment::(), 1); + assert_eq!(unused_unaligned_bound::(37), 37); + for value in [0, 1, 2, 37, usize::MAX - 1, usize::MAX].iter().copied() { + assert_eq!(divide_by_unaligned::(value), value); + assert_eq!(divide_by_byte_alignment(value), value); + } for byte in 0..=u8::MAX { assert_eq!(forwarded_byte_codec(byte), byte); }