diff --git a/verification/aeneas/DESIGN.md b/verification/aeneas/DESIGN.md index ebd0bc2064..778afc2095 100644 --- a/verification/aeneas/DESIGN.md +++ b/verification/aeneas/DESIGN.md @@ -519,6 +519,8 @@ completeness remains an explicit `StorageDecoder.CompleteWith` proof. Extending those native laws requires carrying the `Sized`-related premises needed by owned-value methods, rather than silently guessing metadata for them. +Content transfer and pointer geometry are separate reusable statements. An +indexed content transfer names the actual source/destination metadata pair. Geometric projection requires a bounded forward offset and unchanged opaque provenance. `Cast` additionally retains the start; `CastExact` retains the size. The shared library proves identity, composition, slice splitting, byte-count diff --git a/verification/aeneas/LOWERING_AUDIT.md b/verification/aeneas/LOWERING_AUDIT.md index a585dc23a7..e64a3e5e1b 100644 --- a/verification/aeneas/LOWERING_AUDIT.md +++ b/verification/aeneas/LOWERING_AUDIT.md @@ -559,3 +559,10 @@ 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. + +`IndexedReferent.StorageView` independently supports content implications at an +explicit source/destination metadata pair. Both decoders come from their exact +retained providers. Composition uses the same intermediate view and metadata; +equal byte widths cannot substitute a different zero-sized slice count. These +laws do not change the existing native `TransmuteFrom` contract, choose cast +metadata, or prove access, provenance, liveness, aliasing, or a Rust ABI identity. diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 8f3f9b1a31..bda8988248 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -67,6 +67,8 @@ The shared `Rust.Pointer.Geometry` library proves bounded projections and cast composition, including empty destinations and slice splitting. These are mathematical foundations. Native pointer operations remain rejected by admission because the unchanged Aeneas pointer carrier cannot preserve their geometry. +`IndexedReferent` similarly provides content laws at an explicit metadata pair; +it does not prove native pointer execution or resource permissions. These harnesses use the same annotation and proof rules as every other function. There is no root marker or separately maintained list of required functions. diff --git a/verification/aeneas/lean/IndexedReferent.lean b/verification/aeneas/lean/IndexedReferent.lean new file mode 100644 index 0000000000..9526a3f341 --- /dev/null +++ b/verification/aeneas/lean/IndexedReferent.lean @@ -0,0 +1,154 @@ +/- 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 RustModel +public import Rust.Referent +@[expose] public section + +/-! +This adapter compares byte domains at two explicit metadata values. Each view +retains the provider's sole installed physical profile; its metadata type, +equality test and decoder are projections of that profile. Width equality does +not identify metadata, even for zero-sized referents. + +These are numeric storage implications. They do not interpret native pointer +execution and do not replace the existing type-level TransmuteFrom contract. +-/ + +open Rust.Storage +namespace AeneasSpecs +namespace PhysicalStorage + +def Metadata : PhysicalStorage Raw → Type + | .fixed _ => Unit + | .indexed metadata _ _ => metadata + +def metadataEquality : (physical : PhysicalStorage Raw) → DecidableEq physical.Metadata + | .fixed _ => by change DecidableEq Unit; infer_instance + | .indexed _ equality _ => equality + +def decoder : (physical : PhysicalStorage Raw) → StorageDecoder physical.Metadata Raw + | .fixed decoder => decoder.asStorageDecoder + | .indexed _ _ decoder => decoder + +/-- Mapping a wrapper preserves the child's metadata type and values. -/ +def mapMetadata (physical : PhysicalStorage A) (wrap : A → B) (unwrap : B → A) + (inverse : ∀ raw, unwrap (wrap raw) = raw) : + physical.Metadata → (physical.map wrap unwrap inverse).Metadata := by + cases physical <;> exact id + +theorem map_metadata (physical : PhysicalStorage A) (wrap : A → B) (unwrap : B → A) + (inverse : ∀ raw, unwrap (wrap raw) = raw) (raw : A) : + (physical.map wrap unwrap inverse).decoder.metadata (wrap raw) = + physical.mapMetadata wrap unwrap inverse (physical.decoder.metadata raw) := by + cases physical with + | fixed decoder => rfl + | indexed metadata equality decoder => + change decoder.metadata (unwrap (wrap raw)) = decoder.metadata raw + rw [inverse] + +theorem map_width (physical : PhysicalStorage A) (wrap : A → B) (unwrap : B → A) + (inverse : ∀ raw, unwrap (wrap raw) = raw) (metadata : physical.Metadata) : + (physical.map wrap unwrap inverse).decoder.byteSize + (physical.mapMetadata wrap unwrap inverse metadata) = physical.decoder.byteSize metadata := by + cases physical <;> rfl + +end PhysicalStorage + +namespace IndexedReferent + +/-- Naming storage requires evidence that this exact provider installed it. -/ +structure StorageView {Raw : Type u} (meaning : RustModel Raw) where + physical : PhysicalStorage Raw + installed : meaning.storage = some physical + +namespace StorageView + +abbrev Metadata {meaning : RustModel Raw} (view : StorageView meaning) := + view.physical.Metadata + +instance {meaning : RustModel Raw} (view : StorageView meaning) : DecidableEq view.Metadata := + view.physical.metadataEquality + +def decoder {meaning : RustModel Raw} (view : StorageView meaning) : + StorageDecoder view.Metadata Raw := view.physical.decoder + +theorem initialized {meaning : RustModel Raw} (view : StorageView meaning) + (law : @RustModel.initializedRepresentation Raw meaning) : view.decoder.Initialized := by + rcases view with ⟨physical, installed⟩ + have physicalLaw : physical.Initialized := by + simpa only [RustModel.initializedRepresentation, installed] using law + cases physical with + | fixed decoder => + exact decoder.asStorageDecoder_initialized physicalLaw + | indexed metadata equality decoder => exact physicalLaw + +/-- Unsupported storage cannot be repaired by choosing a decoder in a view. -/ +theorem absent {meaning : RustModel Raw} (missing : meaning.storage = none) : + ¬ Nonempty (StorageView meaning) := by + rintro ⟨view⟩ + have installed := view.installed + rw [missing] at installed + contradiction + +end StorageView + +def safeAt {meaning : RustModel Raw} (view : StorageView meaning) + (metadata : view.Metadata) (bytes : List AMByte) : Prop := + Rust.Referent.Safe view.decoder meaning.decode metadata bytes + +def transferAt {source : RustModel Src} {destination : RustModel Dst} + (sourceView : StorageView source) (sourceMetadata : sourceView.Metadata) + (destinationView : StorageView destination) (destinationMetadata : destinationView.Metadata) + (sourceState destinationState : Rust.Referent.State) : Prop := + Rust.Referent.Transfer (sourceView.decoder.byteSize sourceMetadata) + (safeAt sourceView sourceMetadata) sourceState + (destinationView.decoder.byteSize destinationMetadata) + (safeAt destinationView destinationMetadata) destinationState + +theorem safe_to_initialized {source : RustModel Src} {destination : RustModel Dst} + (sourceView : StorageView source) (sm : sourceView.Metadata) + (destinationView : StorageView destination) (dm : destinationView.Metadata) + (law : sourceView.decoder.Initialized) : + transferAt sourceView sm destinationView dm .safe .initialized := + Rust.Referent.safe_to_initialized _ source.decode law sm _ _ + +theorem initialized_to_safe {source : RustModel Src} {destination : RustModel Dst} + (sourceView : StorageView source) (sm : sourceView.Metadata) + (destinationView : StorageView destination) (dm : destinationView.Metadata) + (law : destinationView.decoder.CompleteWith destination.decode) : + transferAt sourceView sm destinationView dm .initialized .safe := + Rust.Referent.initialized_to_safe _ destination.decode law dm _ _ + +/-- A local completeness proof need cover only this destination metadata. -/ +theorem initialized_to_safe_at {source : RustModel Src} {destination : RustModel Dst} + (sourceView : StorageView source) (sm : sourceView.Metadata) + (destinationView : StorageView destination) (dm : destinationView.Metadata) + (law : ∀ bytes, bytes.length = destinationView.decoder.byteSize dm → + Rust.Storage.Initialized bytes → safeAt destinationView dm bytes) : + transferAt sourceView sm destinationView dm .initialized .safe := by + intro width bytes admitted + exact ⟨admitted.1.trans width, law bytes (admitted.1.trans width) admitted.2⟩ + +/-- The same middle view and metadata occur in both premises. A width guard +cannot silently substitute a different zero-sized referent count. -/ +theorem transfer_trans {source : RustModel Src} {middle : RustModel Mid} + {destination : RustModel Dst} + (sourceView : StorageView source) (sm : sourceView.Metadata) + (middleView : StorageView middle) (mm : middleView.Metadata) + (destinationView : StorageView destination) (dm : destinationView.Metadata) + (firstState middleState lastState : Rust.Referent.State) + (first : transferAt sourceView sm middleView mm firstState middleState) + (second : transferAt middleView mm destinationView dm middleState lastState) + (width : sourceView.decoder.byteSize sm = middleView.decoder.byteSize mm) : + transferAt sourceView sm destinationView dm firstState lastState := + Rust.Referent.transfer_trans _ _ _ _ _ _ _ _ _ first second width + +end IndexedReferent +end AeneasSpecs diff --git a/verification/aeneas/lean/IndexedReferentTests.lean b/verification/aeneas/lean/IndexedReferentTests.lean new file mode 100644 index 0000000000..97323dfae0 --- /dev/null +++ b/verification/aeneas/lean/IndexedReferentTests.lean @@ -0,0 +1,157 @@ +/- 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 +import all IndexedReferent +import all RustModel + +/-! +These examples check retained numeric byte domains and metadata. They do not +execute native pointer operations or prove Rust layout correspondence. +-/ + +open Aeneas Aeneas.Std AeneasSpecs Rust.Storage AeneasSpecs.IndexedReferent +namespace IndexedReferentTests + +def unitView : StorageView modelUnit := ⟨.fixed unitDecoder, rfl⟩ + +example : unitView.Metadata = Unit := rfl +example : unitView.decoder.Initialized := unitView.initialized unitDecoder_initialized + +theorem unit_complete : unitView.decoder.CompleteWith modelUnit.decode := by + intro metadata bytes width _ + cases metadata + have empty : bytes = [] := List.length_eq_zero_iff.mp width + subst bytes + exact ⟨(), rfl⟩ + +example : transferAt unitView () unitView () .initialized .safe := + initialized_to_safe unitView () unitView () unit_complete + +def unitSliceView : StorageView (modelSlice (α := Unit)) := + ⟨PhysicalStorage.slice (.fixed unitDecoder), rfl⟩ + +example : unitSliceView.Metadata = Usize := rfl + +example : unitSliceView.decoder.byteSize (0#usize) = + unitSliceView.decoder.byteSize (1#usize) := rfl + +theorem unit_slice_safe (count : Usize) : safeAt unitSliceView count [] := by + obtain ⟨values, accepted⟩ := arrayDecoder_complete unitDecoder + (fun bytes width _ => ⟨(), emptyDecoder_complete () bytes width⟩) count.val [] + (by simp [unitDecoder, emptyDecoder]) initialized_nil + have physical : unitSliceView.decoder.run count [] = + some (Slice.from values.val (by rw [values.property]; scalar_tac)) := by + change (RustModel.sliceStorageDecoder unitDecoder).run count [] = _ + rw [RustModel.sliceStorageDecoder_run, accepted] + rfl + refine ⟨_, ⟨values.val, by rw [values.property]; scalar_tac⟩, physical, ?_⟩ + have decode_some (raws : List Unit) : decodeList (some : Unit → Option Unit) raws = some raws := by + induction raws with + | nil => rfl + | cons raw raws ih => simp [decodeList, ih] + change (@modelSlice Unit modelUnit).decode _ = _ + simp only [RustModel.decode] + have decoded : decodeList (some : Unit → Option Unit) + (Slice.from values.val (by rw [values.property]; scalar_tac)).val = some values.val := by + rw [Slice.from_val] + exact decode_some _ + split + · rename_i rejected + have impossible := rejected.symm.trans decoded + contradiction + · rename_i output acceptedModel + have same : output = values.val := Option.some.inj (acceptedModel.symm.trans decoded) + subst output + rfl + +-- Two distinct counts have equal width. Transfer uses the explicit pair, +-- rather than concluding that their metadata or decoded values are equal. +theorem unit_slice_transfer (sourceCount destinationCount : Usize) : + transferAt unitSliceView sourceCount unitSliceView destinationCount .safe .safe := by + intro _ bytes admitted + have zero : unitSliceView.decoder.byteSize sourceCount = 0 := by + change sourceCount.val * 0 = 0 + exact Nat.mul_zero _ + have empty : bytes = [] := List.length_eq_zero_iff.mp (admitted.1.trans zero) + subst bytes + refine ⟨?_, unit_slice_safe destinationCount⟩ + change 0 = destinationCount.val * 0 + simp + +example : transferAt unitSliceView (0#usize) unitSliceView (1#usize) .safe .initialized := + safe_to_initialized unitSliceView (0#usize) unitSliceView (1#usize) + (RustModel.sliceStorageDecoder_initialized _ unitDecoder_initialized) + +example : transferAt unitSliceView (0#usize) unitSliceView (2#usize) .safe .safe := + transfer_trans unitSliceView (0#usize) unitSliceView (1#usize) unitSliceView (2#usize) + .safe .safe .safe (unit_slice_transfer _ _) (unit_slice_transfer _ _) rfl + +example (count : Usize) : transferAt unitView () unitSliceView count .initialized .safe := by + apply initialized_to_safe_at + intro bytes width _ + have zero : unitSliceView.decoder.byteSize count = 0 := by + change count.val * 0 = 0 + exact Nat.mul_zero _ + have empty : bytes = [] := List.length_eq_zero_iff.mp (width.trans zero) + subst bytes + exact unit_slice_safe count + +example (raw : Slice Unit) : + (unitSliceView.physical.map (fun value => (value, ())) Prod.fst (fun _ => rfl)).decoder.metadata + (raw, ()) = unitSliceView.physical.mapMetadata (fun value => (value, ())) Prod.fst + (fun _ => rfl) (unitSliceView.physical.decoder.metadata raw) := + unitSliceView.physical.map_metadata _ _ _ raw + +def emptyBits : BitDecoder Empty where + byteSize := 0 + decode _ := none + +@[reducible] def emptyMeaning : RustModel Empty where + Model := Empty + decode raw := nomatch raw + storage := some (.fixed emptyBits) + +@[reducible] def emptySliceMeaning : RustModel (Slice Empty) := @modelSlice Empty emptyMeaning + +def emptySliceView : StorageView emptySliceMeaning := + ⟨PhysicalStorage.slice (.fixed emptyBits), rfl⟩ + +theorem empty_zero_safe : safeAt emptySliceView (0#usize) [] := by + refine ⟨Slice.from [] (by scalar_tac), ⟨[], by scalar_tac⟩, ?_, rfl⟩ + rfl + +theorem empty_one_unsafe : ¬ safeAt emptySliceView (1#usize) [] := by + rintro ⟨raw, _, accepted, _⟩ + have metadata := emptySliceView.decoder.run_metadata (1#usize) [] raw accepted + change raw.len = (1#usize) at metadata + have empty : raw.val = [] := by + cases elements : raw.val with + | nil => rfl + | cons value _ => nomatch value + have length := congrArg UScalar.val metadata + simp [empty] at length + +-- Both widths are zero, but count one requires an Empty inhabitant. +example : ¬ transferAt emptySliceView (0#usize) emptySliceView (1#usize) .safe .safe := by + intro transfer + exact empty_one_unsafe (transfer rfl [] ⟨rfl, empty_zero_safe⟩).2 + +example : ¬ Nonempty (StorageView modelNat) := StorageView.absent rfl + +-- Existing computation contracts retain forbidden execution even for a +-- vacuous postcondition. A metadata-indexed referent view does not alter them. +example : ¬ WP.spec (.fail .undef : Result Unit) (fun _ => True) := by simp +example : ¬ WP.dspec (.fail .undef : Result Unit) (fun _ => True) := by simp + +#print axioms safe_to_initialized +#print axioms initialized_to_safe +#print axioms transfer_trans +#print axioms empty_one_unsafe + +end IndexedReferentTests