From 6afb0119a19d2177e6548fa749fd72d3237ba94f Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 15 Oct 2026 18:05:48 -0400 Subject: [PATCH] Bound pointer projections even for empty referents Byte-set inclusion puts no bound on an empty destination's address. State Project's postcondition with a nonnegative bounded offset, carry that contract through HasField, and use it in the NonNull and transitive projection safety arguments. Add shared mathematical Projection, Cast, and CastExact laws for explicit extents and opaque provenance. Prove composition, empty and one-past bounds, non-null propagation, slice splitting, and no-wrap consequences under explicit word bounds. Keep native pointer carriers rejected: the unchanged Aeneas pin does not retain their geometry. Exercise that boundary with well-formed native pointer shapes. Audit every imported shared Rust module and test root, including referent laws, so adding a library module cannot silently omit its assumptions. gherrit-pr-id: Gsul3w4vydc4wowguwwscielqttbpeytg Agent-authored-by: AI agent acting on joshlf's behalf --- anneal/lean/README.md | 11 +- anneal/lean/Rust.lean | 1 + anneal/lean/Rust/Pointer/Geometry.lean | 285 ++++++++++++++++++++ anneal/lean/Rust/Pointer/GeometryTests.lean | 180 +++++++++++++ anneal/lean/RustPointerTests.lean | 1 + anneal/lean/RustTests.lean | 23 +- verification/aeneas/LOWERING_AUDIT.md | 17 ++ verification/aeneas/tests/test_admission.py | 38 ++- zerocopy/src/lib.rs | 4 +- zerocopy/src/pointer/inner.rs | 7 +- zerocopy/src/pointer/mod.rs | 47 ++-- 11 files changed, 579 insertions(+), 35 deletions(-) create mode 100644 anneal/lean/Rust/Pointer/Geometry.lean create mode 100644 anneal/lean/Rust/Pointer/GeometryTests.lean diff --git a/anneal/lean/README.md b/anneal/lean/README.md index 0fce80a921..93b6189a49 100644 --- a/anneal/lean/README.md +++ b/anneal/lean/README.md @@ -15,6 +15,12 @@ pins. optional provenance, and unit or count metadata. Its casts preserve exact provenance; non-nullness and provenance presence confer no access permission. It has no pointer byte encoding or dereference operation. +- `Rust.Pointer.Geometry` relates pointer values by byte-range projection, + address-preserving cast, and equal-extent cast. Metadata may change, and the + consumer supplies the corresponding byte extents. Empty destinations have + bounded starts, including one-past endpoints; target-word no-wrap conclusions + require explicit numerical bounds. These predicates confer no permissions or + referent validity and do not implement Rust pointer operations. - `Rust.Bytes` gives positional little- and big-endian integer encodings, including exact-length, bound, truncation, and round-trip theorems. - `Rust.Storage` distinguishes initialized bytes from uninitialized bytes and @@ -77,7 +83,10 @@ lake env lean -DwarningAsError=true RustTests.lean `RustTests`, `RustBytesTests`, `RustStorageTests`, and `RustPointerTests` check concrete boundary cases and use the universal theorems independently of any frontend. `RustTests` also audits every compiled library declaration, including -unused helpers, and rejects assumptions beyond Lean's standard logical axioms. +unused helpers, plus declarations in the imported shared test modules, and +rejects assumptions beyond Lean's standard logical axioms. It selects every +imported `Rust` submodule by its defining module, so adding an import does not +require extending a manual audit roster. The second command reruns that audit even when Lake can reuse its compiled test module. diff --git a/anneal/lean/Rust.lean b/anneal/lean/Rust.lean index 9199e7b863..1cb5a8d4c2 100644 --- a/anneal/lean/Rust.lean +++ b/anneal/lean/Rust.lean @@ -9,6 +9,7 @@ those terms. -/ import Rust.Layout import Rust.Memory import Rust.Pointer +import Rust.Pointer.Geometry import Rust.Bytes import Rust.Storage import Rust.Referent diff --git a/anneal/lean/Rust/Pointer/Geometry.lean b/anneal/lean/Rust/Pointer/Geometry.lean new file mode 100644 index 0000000000..57cc6365ff --- /dev/null +++ b/anneal/lean/Rust/Pointer/Geometry.lean @@ -0,0 +1,285 @@ +/- 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. -/ + +import Rust.Pointer +import Std.Tactic + +/-! +Numerical byte-range relations between raw pointer values. Source and destination +metadata may have different types or values. The caller supplies their byte +extents separately; an extent is not a slice element count. Connecting an extent +to a Rust type's metadata and layout remains the consumer's obligation. + +`Projection` places the destination's entire byte interval within the source's +interval and preserves the exact optional provenance. Empty destinations still +have a bounded start, including the source's one-past endpoint. `Cast` adds an +equal start address; `CastExact` also requires equal byte extents. These are +predicates on modeled values, not implementations of Rust operations. An +arbitrary Rust raw pointer cast need not satisfy these additional extent bounds. + +Addresses and extents are unbounded naturals. Word-size conclusions below require +explicit bounds, including representability of an empty destination's start. +None of these relations establishes allocation, permissions, alignment, +initialization, referent validity, liveness, or a right to dereference. The +resource-free carrier and its consumer correspondence obligations are described +in `Rust.Pointer`; no Rust execution semantics or axioms are added here. +-/ + +namespace Rust.Pointer + +/-- A forward subrange with the same opaque provenance, including its absence. -/ +def Projection (source : Value Provenance SourceMetadata) + (destination : Value Provenance DestinationMetadata) + (sourceExtent destinationExtent : Nat) : Prop := + ∃ offset : Nat, + destination.address = source.address + offset ∧ + offset + destinationExtent ≤ sourceExtent ∧ + PreservesProvenance source destination + +/-- A projection that retains the start address, while metadata may change. -/ +def Cast (source : Value Provenance SourceMetadata) + (destination : Value Provenance DestinationMetadata) + (sourceExtent destinationExtent : Nat) : Prop := + Projection source destination sourceExtent destinationExtent ∧ + destination.address = source.address + +/-- A cast that also retains the byte extent, independently of metadata equality. -/ +def CastExact (source : Value Provenance SourceMetadata) + (destination : Value Provenance DestinationMetadata) + (sourceExtent destinationExtent : Nat) : Prop := + Cast source destination sourceExtent destinationExtent ∧ + destinationExtent = sourceExtent + +variable {p : Value P M} {q : Value P N} {r : Value P O} + {sourceExtent middleExtent destinationExtent : Nat} + +theorem projection_refl (p : Value P M) (extent : Nat) : + Projection p p extent extent := + ⟨0, by simp, by simp, rfl⟩ + +/-- Both premises use the same intermediate pointer, including its exact metadata, +and the same intermediate byte extent. -/ +theorem projection_trans + (first : Projection p q sourceExtent middleExtent) + (second : Projection q r middleExtent destinationExtent) : + Projection p r sourceExtent destinationExtent := by + obtain ⟨a, ha, hba, hpa⟩ := first + obtain ⟨b, hb, hbb, hpb⟩ := second + refine ⟨a + b, by omega, by omega, ?_⟩ + exact hpb.trans hpa + +theorem projection_preservesProvenance + (h : Projection p q sourceExtent destinationExtent) : + PreservesProvenance p q := by + obtain ⟨_, _, _, provenance⟩ := h + exact provenance + +/-- The exact token is preserved without requiring decidable provenance equality. -/ +theorem projection_carries + (h : Projection p q sourceExtent destinationExtent) (token : P) + (carried : Carries p token) : Carries q token := + (projection_preservesProvenance h).trans carried + +theorem projection_hasProvenance + (h : Projection p q sourceExtent destinationExtent) : + hasProvenance q ↔ hasProvenance p := by + unfold hasProvenance + rw [projection_preservesProvenance h] + +theorem projection_address_le + (h : Projection p q sourceExtent destinationExtent) : + p.address ≤ q.address := by + obtain ⟨offset, address, _, _⟩ := h + omega + +theorem projection_extent_le + (h : Projection p q sourceExtent destinationExtent) : + destinationExtent ≤ sourceExtent := by + obtain ⟨offset, _, bound, _⟩ := h + omega + +theorem projection_end_le + (h : Projection p q sourceExtent destinationExtent) : + q.address + destinationExtent ≤ p.address + sourceExtent := by + obtain ⟨offset, address, bound, _⟩ := h + omega + +/-- This endpoint characterization includes empty intervals; byte-set inclusion +alone would not bound the start of an empty destination. -/ +theorem projection_iff_bounds : + Projection p q sourceExtent destinationExtent ↔ + p.address ≤ q.address ∧ + q.address + destinationExtent ≤ p.address + sourceExtent ∧ + PreservesProvenance p q := by + constructor + · intro h + exact ⟨projection_address_le h, projection_end_le h, + projection_preservesProvenance h⟩ + · rintro ⟨start, finish, provenance⟩ + exact ⟨q.address - p.address, by omega, by omega, provenance⟩ + +theorem projection_empty_iff : + Projection p q sourceExtent 0 ↔ + p.address ≤ q.address ∧ q.address ≤ p.address + sourceExtent ∧ + PreservesProvenance p q := by + simpa using (projection_iff_bounds (p := p) (q := q) + (sourceExtent := sourceExtent) (destinationExtent := 0)) + +/-- Every byte in the destination's half-open interval lies in the source's. -/ +theorem projection_byte_bounds + (h : Projection p q sourceExtent destinationExtent) (address : Nat) + (inside : q.address ≤ address ∧ address < q.address + destinationExtent) : + p.address ≤ address ∧ address < p.address + sourceExtent := by + have := projection_address_le h + have := projection_end_le h + omega + +theorem projection_start_lt_end + (h : Projection p q sourceExtent destinationExtent) + (nonempty : 0 < destinationExtent) : + q.address < p.address + sourceExtent := by + have := projection_end_le h + omega + +/-- Forward natural-number offsets preserve nonzero starts. -/ +theorem projection_nonzero + (h : Projection p q sourceExtent destinationExtent) + (nonzero : p.address ≠ 0) : q.address ≠ 0 := by + have := projection_address_le h + omega + +theorem projection_nonNull + (h : Projection p q sourceExtent destinationExtent) + (nonzero : p.address ≠ 0) : ∃ result, nonNull q = some result := by + let result : NonNull P N := ⟨q, projection_nonzero h nonzero⟩ + exact ⟨result, (nonNull_eq_some_iff q result).mpr rfl⟩ + +/-- A source end at most the word limit bounds destination ends as naturals. +An empty destination at the limit still needs a strict representability check. -/ +theorem projection_word_end_le + (h : Projection p q sourceExtent destinationExtent) (wordBits : Nat) + (sourceBound : p.address + sourceExtent ≤ 2 ^ wordBits) : + q.address + destinationExtent ≤ 2 ^ wordBits := + Nat.le_trans (projection_end_le h) sourceBound + +/-- A representable source end makes both destination endpoints representable, +including the start of an empty destination at the source's one-past endpoint. -/ +theorem projection_word_bounds + (h : Projection p q sourceExtent destinationExtent) (wordBits : Nat) + (sourceBound : p.address + sourceExtent < 2 ^ wordBits) : + q.address < 2 ^ wordBits ∧ q.address + destinationExtent < 2 ^ wordBits := by + have := projection_end_le h + omega + +/-- With the strict source-end premise, reducing either destination endpoint +modulo the target word modulus does not wrap it. -/ +theorem projection_word_noWrap + (h : Projection p q sourceExtent destinationExtent) (wordBits : Nat) + (sourceBound : p.address + sourceExtent < 2 ^ wordBits) : + q.address % (2 ^ wordBits) = q.address ∧ + (q.address + destinationExtent) % (2 ^ wordBits) = + q.address + destinationExtent := by + have bounds := projection_word_bounds h wordBits sourceBound + exact ⟨Nat.mod_eq_of_lt bounds.1, Nat.mod_eq_of_lt bounds.2⟩ + +/-- The projection's actual offset addition also agrees with word reduction. -/ +theorem projection_offset_noWrap + (h : Projection p q sourceExtent destinationExtent) (wordBits : Nat) + (sourceBound : p.address + sourceExtent < 2 ^ wordBits) : + ∃ offset : Nat, offset + destinationExtent ≤ sourceExtent ∧ + p.address + offset = q.address ∧ + (p.address + offset) % (2 ^ wordBits) = q.address := by + have noWrap := (projection_word_noWrap h wordBits sourceBound).1 + obtain ⟨offset, address, bound, _⟩ := h + exact ⟨offset, bound, address.symm, by simpa only [← address] using noWrap⟩ + +theorem cast_refl (p : Value P M) (extent : Nat) : Cast p p extent extent := + ⟨projection_refl p extent, rfl⟩ + +theorem cast_trans + (first : Cast p q sourceExtent middleExtent) + (second : Cast q r middleExtent destinationExtent) : + Cast p r sourceExtent destinationExtent := + ⟨projection_trans first.1 second.1, second.2.trans first.2⟩ + +/-- Equal starts reduce containment to an extent comparison and provenance. -/ +theorem cast_iff : + Cast p q sourceExtent destinationExtent ↔ + q.address = p.address ∧ destinationExtent ≤ sourceExtent ∧ + PreservesProvenance p q := by + constructor + · intro h + exact ⟨h.2, projection_extent_le h.1, projection_preservesProvenance h.1⟩ + · rintro ⟨address, bound, provenance⟩ + exact ⟨⟨0, by simpa using address, by simpa using bound, provenance⟩, address⟩ + +theorem castExact_refl (p : Value P M) (extent : Nat) : CastExact p p extent extent := + ⟨cast_refl p extent, rfl⟩ + +theorem castExact_trans + (first : CastExact p q sourceExtent middleExtent) + (second : CastExact q r middleExtent destinationExtent) : + CastExact p r sourceExtent destinationExtent := + ⟨cast_trans first.1 second.1, second.2.trans first.2⟩ + +theorem castExact_iff : + CastExact p q sourceExtent destinationExtent ↔ + q.address = p.address ∧ destinationExtent = sourceExtent ∧ + PreservesProvenance p q := by + constructor + · intro h + exact ⟨h.1.2, h.2, projection_preservesProvenance h.1.1⟩ + · rintro ⟨address, extent, provenance⟩ + exact ⟨cast_iff.mpr ⟨address, by omega, provenance⟩, extent⟩ + +/-- Reinterpreting a pointer preserves its numeric geometry when the requested +extent fits. This is a value theorem, not an interpretation of native casts. -/ +theorem cast_shrink (pointer : Value P M) (sourceExtent destinationExtent : Nat) + (fits : destinationExtent ≤ sourceExtent) : + Cast pointer (cast pointer) sourceExtent destinationExtent := + cast_iff.mpr ⟨rfl, fits, rfl⟩ + +/-- Forgetting metadata can describe a zero-byte destination at the same start. -/ +theorem cast_to_unit (pointer : Value P M) (sourceExtent : Nat) : + Cast pointer (dataPointer pointer) sourceExtent 0 := + cast_iff.mpr ⟨rfl, Nat.zero_le _, rfl⟩ + +/-- Metadata assembly keeps the address and provenance; containment still needs +an explicit comparison of the actual source and destination extents. -/ +theorem withMetadata_cast (pointer : Thin P) (metadata : M) + (sourceExtent destinationExtent : Nat) (fits : destinationExtent ≤ sourceExtent) : + Cast pointer (withMetadata pointer metadata) sourceExtent destinationExtent := + cast_iff.mpr ⟨rfl, fits, rfl⟩ + +/-- A byte-slice view uses a byte count. A bare slice-pointer cast would retain +an element count instead. Native usize representability is a separate premise. -/ +theorem slice_as_bytes (pointer : Slice P) (stride : Nat) : + CastExact pointer (withMetadata (dataPointer pointer) (pointer.metadata * stride)) + (pointer.metadata * stride) (pointer.metadata * stride) := + castExact_iff.mpr ⟨rfl, rfl, rfl⟩ + +/-- The two numeric subregions meet at exactly the split count, even when every +element occupies zero bytes. This theorem constructs no Rust pointer and needs +no access permission; native pointer arithmetic needs its own interpretation. -/ +theorem slice_split (pointer : Slice P) (stride count : Nat) + (within : count ≤ pointer.metadata) : + Projection pointer (withMetadata (dataPointer pointer) count) + (pointer.metadata * stride) (count * stride) ∧ + Projection pointer + (⟨pointer.address + count * stride, pointer.provenance, + pointer.metadata - count⟩ : Slice P) + (pointer.metadata * stride) ((pointer.metadata - count) * stride) := by + constructor + · exact ⟨0, by simp [withMetadata, dataPointer], by + simpa using Nat.mul_le_mul_right stride within, rfl⟩ + · refine ⟨count * stride, rfl, ?_, rfl⟩ + have sum : count + (pointer.metadata - count) = pointer.metadata := by omega + rw [← Nat.add_mul, sum] + exact Nat.le_refl _ + +end Rust.Pointer diff --git a/anneal/lean/Rust/Pointer/GeometryTests.lean b/anneal/lean/Rust/Pointer/GeometryTests.lean new file mode 100644 index 0000000000..ba26208bbc --- /dev/null +++ b/anneal/lean/Rust/Pointer/GeometryTests.lean @@ -0,0 +1,180 @@ +/- 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. -/ + +import Rust.Pointer.Geometry + +/-! +Boundary examples for the resource-free geometry. Byte extents are explicit, +including when slice counts differ. These are Lean theorems about the model; +they do not establish that an extracted Rust operation implements a relation. +`RustTests` imports these declarations through `RustPointerTests` and audits +all their transitive axioms with the shared library's allowlist. +-/ + +namespace Rust.Pointer.GeometryTests + +-- No decidable equality instance is needed for the opaque provenance parameter. +theorem opaque_identity {P M : Type} (p : Value P M) (extent : Nat) : + Projection p p extent extent ∧ Cast p p extent extent ∧ + CastExact p p extent extent := + ⟨projection_refl p extent, cast_refl p extent, castExact_refl p extent⟩ + +-- Composition uses the same exact middle value, with its metadata and extent. +theorem heterogeneous_composition {P M N O : Type} + (p : Value P M) (q : Value P N) (r : Value P O) (a b c : Nat) + (first : Projection p q a b) (second : Projection q r b c) : + Projection p r a c := projection_trans first second + +theorem cast_composition {P M N O : Type} + (p : Value P M) (q : Value P N) (r : Value P O) (a b c : Nat) + (first : Cast p q a b) (second : Cast q r b c) : + Cast p r a c := cast_trans first second + +theorem exact_cast_composition {P M N O : Type} + (p : Value P M) (q : Value P N) (r : Value P O) (a b c : Nat) + (first : CastExact p q a b) (second : CastExact q r b c) : + CastExact p r a c := castExact_trans first second + +theorem metadata_changing_projection_chain : + Projection (⟨100, some 7, ()⟩ : Thin Nat) + (⟨105, some 7, true⟩ : Value Nat Bool) 8 1 := + projection_trans (q := (⟨102, some 7, 2⟩ : Slice Nat)) (middleExtent := 4) + ⟨2, rfl, by decide, rfl⟩ ⟨3, rfl, by decide, rfl⟩ + +theorem exact_token_preserved {P M N : Type} + (p : Value P M) (q : Value P N) (a b : Nat) (token : P) + (h : Projection p q a b) (carried : Carries p token) : Carries q token := + projection_carries h token carried + +theorem nonNull_preserved {P M N : Type} + (p : Value P M) (q : Value P N) (a b : Nat) + (h : Projection p q a b) (nonzero : p.address ≠ 0) : + ∃ result, nonNull q = some result := projection_nonNull h nonzero + +-- An interior destination and one at the source's end are both bounded. +theorem empty_inside : + Projection (⟨100, some 7, 4⟩ : Slice Nat) (⟨103, some 7, ()⟩ : Thin Nat) 8 0 := + ⟨3, rfl, by decide, rfl⟩ + +theorem empty_one_past : + Projection (⟨100, some 7, 4⟩ : Slice Nat) (⟨108, some 7, ()⟩ : Thin Nat) 8 0 := + ⟨8, rfl, by decide, rfl⟩ + +theorem empty_before_source_rejected : + ¬Projection (⟨100, some 7, ()⟩ : Thin Nat) ⟨99, some 7, ()⟩ 8 0 := by + intro h + have := projection_address_le h + contradiction + +theorem empty_beyond_source_rejected : + ¬Projection (⟨100, some 7, ()⟩ : Thin Nat) ⟨109, some 7, ()⟩ 8 0 := by + intro h + have := projection_end_le h + contradiction + +theorem positive_at_one_past_rejected : + ¬Projection (⟨100, some 7, ()⟩ : Thin Nat) ⟨108, some 7, ()⟩ 8 1 := by + intro h + have := projection_end_le h + contradiction + +-- An 8-bit wrapping addition from 250 to 2 is not a natural-number projection. +theorem wrapping_destination_rejected : + (250 + 8) % (2 ^ 8) = 2 ∧ + ¬Projection (⟨250, some 7, ()⟩ : Thin Nat) ⟨2, some 7, ()⟩ 16 1 := by + refine ⟨by decide, ?_⟩ + intro h + have := projection_address_le h + contradiction + +theorem different_provenance_rejected : + ¬Projection (⟨100, some 1, ()⟩ : Thin Nat) ⟨100, some 2, ()⟩ 8 8 := by + intro h + have impossible : (some 2 : Option Nat) = some 1 := projection_preservesProvenance h + contradiction + +-- Absence is preserved exactly; geometry does not require a provenance token. +theorem absent_provenance : + CastExact (⟨100, none, ()⟩ : Thin Nat) (⟨100, none, 0⟩ : Slice Nat) 0 0 := + ⟨⟨⟨0, rfl, by decide, rfl⟩, rfl⟩, rfl⟩ + +-- The counts describe different element layouts: 3 two-byte elements and 6 +-- one-byte elements have equal byte extent. Count equality is not a cast premise. +theorem different_counts_equal_extent : + CastExact (⟨100, some 7, 3⟩ : Slice Nat) ⟨100, some 7, 6⟩ (3 * 2) (6 * 1) := + ⟨⟨⟨0, rfl, by decide, rfl⟩, rfl⟩, rfl⟩ + +-- Distinct zero-sized slice counts also retain their distinct metadata. +theorem zero_sized_counts : + CastExact (⟨100, some 7, 3⟩ : Slice Nat) ⟨100, some 7, 9⟩ (3 * 0) (9 * 0) ∧ + ¬equal (⟨100, some 7, 3⟩ : Slice Nat) ⟨100, some 7, 9⟩ := + ⟨⟨⟨⟨0, rfl, by decide, rfl⟩, rfl⟩, rfl⟩, by decide⟩ + +theorem shifted_projection_is_not_cast : + Projection (⟨100, some 7, ()⟩ : Thin Nat) ⟨102, some 7, ()⟩ 8 4 ∧ + ¬Cast (⟨100, some 7, ()⟩ : Thin Nat) ⟨102, some 7, ()⟩ 8 4 := by + refine ⟨⟨2, rfl, by decide, rfl⟩, ?_⟩ + intro h + have := h.2 + contradiction + +theorem smaller_cast_is_not_exact : + Cast (⟨100, some 7, 4⟩ : Slice Nat) ⟨100, some 7, 2⟩ 8 4 ∧ + ¬CastExact (⟨100, some 7, 4⟩ : Slice Nat) ⟨100, some 7, 2⟩ 8 4 := by + refine ⟨⟨⟨0, rfl, by decide, rfl⟩, rfl⟩, ?_⟩ + intro h + have := h.2 + contradiction + +theorem larger_extent_rejected : + ¬Projection (⟨100, some 7, 4⟩ : Slice Nat) ⟨100, some 7, 5⟩ 8 10 := by + intro h + have := projection_extent_le h + contradiction + +-- Merely identifying middle addresses cannot replace the exact middle pointer +-- and byte extent: these two slice metadata choices describe different ranges. +theorem intermediate_extent_is_necessary : + Projection (⟨10, some 7, ()⟩ : Thin Nat) (⟨10, some 7, 0⟩ : Slice Nat) 1 0 ∧ + Projection (⟨10, some 7, 2⟩ : Slice Nat) (⟨11, some 7, ()⟩ : Thin Nat) 2 1 ∧ + ¬Projection (⟨10, some 7, ()⟩ : Thin Nat) ⟨11, some 7, ()⟩ 1 1 := by + refine ⟨⟨0, rfl, by decide, rfl⟩, ⟨1, rfl, by decide, rfl⟩, ?_⟩ + intro h + have := projection_end_le h + contradiction + +theorem bounded_noWrap : + (108 : Nat) % (2 ^ 8) = 108 ∧ (108 + 0) % (2 ^ 8) = 108 + 0 := + projection_word_noWrap empty_one_past 8 (by decide) + +-- A non-strict end bound allows an unrepresentable empty start at the modulus. +-- This is why the no-wrap theorem requires a strict bound even for zero extent. +theorem strict_word_bound_is_necessary : + Projection (⟨250, some 7, ()⟩ : Thin Nat) ⟨256, some 7, ()⟩ 6 0 ∧ + 250 + 6 ≤ 2 ^ 8 ∧ (256 : Nat) % (2 ^ 8) ≠ 256 := + ⟨⟨6, rfl, by decide, rfl⟩, by decide, by decide⟩ + +end Rust.Pointer.GeometryTests + +-- These constructions describe the arithmetic used by familiar cast/project +-- operations without assigning native pointer execution semantics. +example (pointer : Rust.Pointer.Slice P) (stride : Nat) : + Rust.Pointer.CastExact pointer + (Rust.Pointer.withMetadata (Rust.Pointer.dataPointer pointer) (pointer.metadata * stride)) + (pointer.metadata * stride) (pointer.metadata * stride) := + Rust.Pointer.slice_as_bytes pointer stride + +example (pointer : Rust.Pointer.Slice P) (count : Nat) (within : count ≤ pointer.metadata) : + Rust.Pointer.Projection pointer + (⟨pointer.address, pointer.provenance, count⟩ : Rust.Pointer.Slice P) 0 0 := by + simpa [Rust.Pointer.withMetadata, Rust.Pointer.dataPointer] using + (Rust.Pointer.slice_split pointer 0 count within).1 + +example (pointer : Rust.Pointer.Value P M) : + Rust.Pointer.Cast pointer (Rust.Pointer.dataPointer pointer) 0 0 := + Rust.Pointer.cast_to_unit pointer 0 diff --git a/anneal/lean/RustPointerTests.lean b/anneal/lean/RustPointerTests.lean index f3ae2ca6d9..9c81030377 100644 --- a/anneal/lean/RustPointerTests.lean +++ b/anneal/lean/RustPointerTests.lean @@ -7,6 +7,7 @@ This file may not be copied, modified, or distributed except according to those terms. -/ import Rust.Pointer +import Rust.Pointer.GeometryTests open Rust.Pointer diff --git a/anneal/lean/RustTests.lean b/anneal/lean/RustTests.lean index cf3ca1739e..f41bc741c1 100644 --- a/anneal/lean/RustTests.lean +++ b/anneal/lean/RustTests.lean @@ -7,6 +7,9 @@ This file may not be copied, modified, or distributed except according to those terms. -/ import Rust +import RustBytesTests +import RustStorageTests +import RustPointerTests import Lean.Util.CollectAxioms import Lean.Elab.Command @@ -17,7 +20,8 @@ check that callers can use the universal lemmas without reproducing their proofs Lean checks each `example` as a theorem. `by decide` computes the small concrete proposition and supplies a proof; it is not an unchecked runtime assertion. -The final command audits the assumptions of every compiled library declaration. +The final command audits the assumptions of every compiled library declaration +and of the imported shared test modules. An abstract mathematical library should not acquire a Rust correspondence axiom merely because one frontend needs that premise for its own operations. -/ @@ -59,12 +63,17 @@ end Compatibility -- a previously compiled test module. run_cmd do let env ← Lean.getEnv - -- Select declarations by the module that defined them, not by namespace. - -- A helper outside `Rust` still belongs to this library. Keep this roster in - -- step with the library modules, and reject a missing import rather than - -- accidentally auditing only part of the package. - let libraryModules := #[`Rust, `Rust.Layout, `Rust.Memory, `Rust.Pointer, `Rust.Bytes, `Rust.Storage, `Rust.Arithmetic] - let owners ← libraryModules.mapM fun moduleName => do + -- Select declarations by their defining module, not their namespace. The + -- hierarchical `Rust` prefix includes every imported library submodule, even + -- when its declarations use other namespaces; it does not match `RustAeneas`. + -- The three test roots live outside that hierarchy and are selected explicitly. + let testModules := #[`RustBytesTests, `RustStorageTests, `RustPointerTests] + for required in #[`Rust] ++ testModules do + unless (env.getModuleIdx? required).isSome do + throwError "Shared library or test root was not imported: {required}" + let auditedModules := env.header.moduleNames.filter fun moduleName => + (`Rust).isPrefixOf moduleName || testModules.contains moduleName + let owners ← auditedModules.mapM fun moduleName => do let some owner := env.getModuleIdx? moduleName | throwError "Shared library module was not imported: {moduleName}" pure owner diff --git a/verification/aeneas/LOWERING_AUDIT.md b/verification/aeneas/LOWERING_AUDIT.md index 70bd350674..c6d425327c 100644 --- a/verification/aeneas/LOWERING_AUDIT.md +++ b/verification/aeneas/LOWERING_AUDIT.md @@ -538,3 +538,20 @@ golden/proof checks provide such a certificate. [duplicate-call elimination]: https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/src/pure/PureMicroPassesGeneral.ml#L607 [builtin replacements]: https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/src/extract/ExtractBuiltin.ml#L507 [borrow-calculus soundness paper]: https://arxiv.org/html/2404.02680v1 + +## Pointer geometry and its current extraction boundary + +`Rust.Pointer.Geometry` states bounded subranges, unchanged-address casts, and +unchanged-size casts. Bounds constrain even empty destinations: their start must +lie between the source start and its end, inclusive. The `Project` Rust contract +states the same requirement; a subset of an empty byte set alone supplies no +address bound. Composition retains the exact intermediate pointer and extent. +The mathematical no-wrap lemmas require an explicit target address bound. + +These theorems do not interpret native pointer operations. In the unchanged pin, +Aeneas's `RawPtr` carrier stores a typed value, without an address, metadata, or +provenance field. It cannot faithfully carry these geometric observations. +Admission continues to reject raw-pointer carriers, including when nested under +references, slices, and arrays. The regression inputs use actual native type +shapes, rather than malformed pointer syntax. No local zerocopy pointer body is +made opaque to substitute an assumed geometry theorem for its implementation. diff --git a/verification/aeneas/tests/test_admission.py b/verification/aeneas/tests/test_admission.py index 90db01c45b..eb4358938f 100644 --- a/verification/aeneas/tests/test_admission.py +++ b/verification/aeneas/tests/test_admission.py @@ -208,11 +208,39 @@ def test_new_operations_attributes_and_configuration_fail_closed(self): with self.assertRaises(ValueError): self.check() - def test_padding_and_raw_storage_cannot_be_logical_values(self): - self.data['translated']['fun_decls'][0]['body']['Unstructured']['locals']['locals'][0]['ty'] = { - 'Untagged': {'RawPtr': []}} - with self.assertRaisesRegex(ValueError, 'raw pointers and storage'): - self.check() + def test_native_raw_pointer_carriers_cannot_be_logical_values(self): + # These shapes occur in the preserved raw-pointers capability probe's + # cast, with_len and nonnull signatures, before and after lowering. + u8 = {'Untagged': {'Scalar': {'Integer': {'Unsigned': 'U8'}}}} + u32 = {'Untagged': {'Scalar': {'Integer': {'Unsigned': 'U32'}}}} + pointers = [ + {'Untagged': {'RawPtr': [u32, 'Shared']}}, + {'Untagged': {'RawPtr': [u8, 'Shared']}}, + {'Untagged': {'RawPtr': [u8, 'Mut']}}, + {'Untagged': {'RawPtr': [ + {'Untagged': {'Slice': [u8, None]}}, 'Shared']}}, + ] + length = {'Untagged': [ + {'Integer': {'Unsigned': ['Usize', '1']}}, + {'Untagged': {'Scalar': {'Integer': {'Unsigned': 'Usize'}}}}]} + original = copy.deepcopy(self.data) + for pointer in pointers: + for carrier in (pointer, {'Untagged': {'Slice': [pointer, None]}}, + {'Untagged': {'Array': [pointer, length, None]}}, + {'Untagged': {'Ref': [{'Body': 1}, pointer, 'Shared']}}, + {'Untagged': {'Ref': [{'Body': 1}, pointer, 'Mut']}}): + for site in ('local', 'input', 'output'): + with self.subTest(pointer=pointer, carrier=carrier, site=site): + self.data = copy.deepcopy(original) + function = self.data['translated']['fun_decls'][0] + if site == 'local': + function['body']['Unstructured']['locals']['locals'][0]['ty'] = carrier + elif site == 'input': + function['signature']['inputs'][0] = carrier + else: + function['signature']['output'] = carrier + with self.assertRaisesRegex(ValueError, 'raw pointers and storage'): + self.check() def test_bit_invalid_production_cannot_be_an_infallible_cast(self): self.body()[0]['statements'].append({ diff --git a/zerocopy/src/lib.rs b/zerocopy/src/lib.rs index 58adfe171c..f121697c57 100644 --- a/zerocopy/src/lib.rs +++ b/zerocopy/src/lib.rs @@ -1390,8 +1390,8 @@ pub unsafe trait HasField) -> *mut Self::Type; } diff --git a/zerocopy/src/pointer/inner.rs b/zerocopy/src/pointer/inner.rs index eeef49f948..edb5559134 100644 --- a/zerocopy/src/pointer/inner.rs +++ b/zerocopy/src/pointer/inner.rs @@ -193,9 +193,10 @@ impl<'a, T: ?Sized> PtrInner<'a, T> { // contained in it or one-past-the-end of it are null. // // By invariant on `C: Project`, `C::project` is a provenance-preserving - // projection which preserves or shrinks the set of referent bytes, so - // `projected_raw` references a subset of `self`'s referent, and so it - // cannot be null. + // projection whose starting address is within `self`'s referent or + // one-past-the-end, including when the destination is empty. Thus its + // starting address cannot be null. For an empty destination, byte-set + // inclusion alone would not establish this address bound. // // [1] https://doc.rust-lang.org/1.92.0/std/ptr/index.html#allocation let projected_non_null = unsafe { NonNull::new_unchecked(projected_raw) }; diff --git a/zerocopy/src/pointer/mod.rs b/zerocopy/src/pointer/mod.rs index 4759396748..d8e409dc2d 100644 --- a/zerocopy/src/pointer/mod.rs +++ b/zerocopy/src/pointer/mod.rs @@ -66,8 +66,16 @@ pub mod cast { /// /// # Safety /// - /// The returned pointer refers to a non-strict subset of the bytes of - /// `src`'s referent, and has the same provenance as `src`. + /// The returned pointer must have the same provenance as `src`. There + /// must be a nonnegative byte offset `offset` such that its address is + /// the source address plus `offset`, without wrapping, and + /// `offset + destination_size <= source_size`. Each size is the + /// referent's actual byte size at that pointer's metadata. + /// + /// This includes empty referents: an empty destination may start at + /// any offset through one-past-the-end of the source, but not outside + /// that range. Byte-set inclusion alone would not constrain an empty + /// destination's address. fn project(src: PtrInner<'_, Src>) -> *mut Dst; } @@ -84,7 +92,8 @@ pub mod cast { /// /// # Safety /// - /// A `CastExact` projection must preserve the set of referent bytes. + /// A `CastExact` projection must preserve the referent's byte size. Since + /// `Cast` already preserves its start, it preserves the same byte range. pub unsafe trait CastExact: Cast {} /// A no-op pointer cast. @@ -92,9 +101,9 @@ pub mod cast { #[allow(missing_debug_implementations)] pub struct IdCast; - // SAFETY: `project` returns its argument unchanged, and so it is a - // provenance-preserving projection which preserves the set of referent - // bytes. + // SAFETY: `project` returns its argument unchanged. Its offset is zero, + // its referent size is unchanged, and it preserves provenance. These facts + // satisfy the bounded-range requirement even for an empty referent. unsafe impl Project for IdCast { #[inline(always)] fn project(src: PtrInner<'_, T>) -> *mut T { @@ -120,9 +129,9 @@ pub mod cast { #[allow(missing_debug_implementations, missing_copy_implementations)] pub enum CastSized {} - // SAFETY: By the `static_assert!`, `Dst` is no larger than `Src`, - // and so all casts preserve or shrink the set of referent bytes. All - // operations preserve provenance. + // SAFETY: The cast preserves address and provenance. The `static_assert!` + // guarantees that `Dst` is no larger than `Src`, so offset zero satisfies + // the bounded-range requirement, including for zero-sized referents. unsafe impl Project for CastSized { #[inline(always)] fn project(src: PtrInner<'_, Src>) -> *mut Dst { @@ -147,9 +156,9 @@ pub mod cast { #[allow(missing_debug_implementations, missing_copy_implementations)] pub enum CastSizedExact {} - // SAFETY: By the `static_assert!`, `Dst` has the same size as `Src`, - // and so all casts preserve the set of referent bytes. All operations - // preserve provenance. + // SAFETY: The cast preserves address and provenance. The `static_assert!` + // guarantees equal referent sizes, so offset zero satisfies the range + // requirement without changing either endpoint, including at size zero. unsafe impl Project for CastSizedExact { #[inline(always)] fn project(src: PtrInner<'_, Src>) -> *mut Dst { @@ -455,9 +464,13 @@ pub mod cast { _u: PhantomData, } - // SAFETY: Since `TU::project` and `UV::project` are each - // provenance-preserving operations which preserve or shrink the set of - // referent bytes, so is their composition. + // SAFETY: Let the two projections have offsets `a` and `b`, and let + // their referents' actual sizes be `t`, `u`, and `v`. Their contracts give + // `a + u <= t` and `b + v <= u`, so `(a + b) + v <= t`. Their addresses + // therefore compose at the bounded offset `a + b`, including for empty + // referents. Both operations preserve the same provenance. The intermediate + // pointer and its metadata are exactly the ones returned by the first + // projection and passed to the second. unsafe impl Project for TransitiveProject where T: ?Sized, @@ -536,8 +549,8 @@ pub mod cast { #[allow(missing_copy_implementations, missing_debug_implementations)] pub struct CastToUnit; - // SAFETY: The `project` implementation projects to a subset of its - // argument's referent using provenance-preserving operations. + // SAFETY: The cast keeps the address and provenance. Its zero-sized + // destination fits at offset zero, even when the source is also empty. unsafe impl Project for CastToUnit { #[inline(always)] fn project(src: PtrInner<'_, T>) -> *mut () {