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 () {