diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 4bff328dc0..ad00a17773 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -56,6 +56,12 @@ allocator admission additionally needs the outer alignment and the signed metadata-size bound. Allocator behavior, zeroing, and `Box` validity remain separate Rust obligations. +Six concrete wrappers in [`lib.rs`](../../zerocopy/src/lib.rs) call the actual +`PointerMetadata` implementations for `()` and `usize`. Their contracts check +element-count conversion, layout-variant handling, and checked metadata sizing. +Using these results for an arbitrary `KnownLayout` implementation requires +separate layout correspondence. + 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. Every present specification must have its corresponding proof in both CI builds. diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index 8d224d798b..0a043cfe75 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -1298,8 +1298,96 @@ def layout.tail_checks.trailing_arithmetic_check else ok () else ok () +/-- [zerocopy::{impl zerocopy::PointerMetadata for ()}::from_elem_count]: + Source: 'src/lib.rs', lines 975:4-975:46 + Visibility: public -/ +def Tuple.Insts.ZerocopyPointerMetadata.from_elem_count + (_elems : Std.Usize) : Result Unit := do + ok () + +/-- [zerocopy::{impl zerocopy::PointerMetadata for ()}::to_elem_count]: + Source: 'src/lib.rs', lines 978:4-980:5 + Visibility: public -/ +def Tuple.Insts.ZerocopyPointerMetadata.to_elem_count + (_ : Unit) : Result Std.Usize := do + ok 0#usize + +/-- [zerocopy::{impl zerocopy::PointerMetadata for ()}::size_for_metadata]: + Source: 'src/lib.rs', lines 983:4-990:5 + Visibility: public -/ +def Tuple.Insts.ZerocopyPointerMetadata.size_for_metadata + (_ : Unit) (runtime_layout : layout.DstLayout) : + Result (Option Std.Usize) + := do + match runtime_layout.size_info with + | layout.SizeInfo.Sized size => ok (some size) + | layout.SizeInfo.SliceDst _ => ok none + +/-- [zerocopy::{impl zerocopy::PointerMetadata for usize}::from_elem_count]: + Source: 'src/lib.rs', lines 995:4-997:5 + Visibility: public -/ +def Usize.Insts.ZerocopyPointerMetadata.from_elem_count + (elems : Std.Usize) : Result Std.Usize := do + ok elems + +/-- [zerocopy::{impl zerocopy::PointerMetadata for usize}::to_elem_count]: + Source: 'src/lib.rs', lines 1000:4-1002:5 + Visibility: public -/ +def Usize.Insts.ZerocopyPointerMetadata.to_elem_count + (self : Std.Usize) : Result Std.Usize := do + ok self + +/-- [zerocopy::{impl zerocopy::PointerMetadata for usize}::size_for_metadata]: + Source: 'src/lib.rs', lines 1005:4-1012:5 + Visibility: public -/ +def Usize.Insts.ZerocopyPointerMetadata.size_for_metadata + (self : Std.Usize) (runtime_layout : layout.DstLayout) : + Result (Option Std.Usize) + := do + match runtime_layout.size_info with + | layout.SizeInfo.Sized _ => ok none + | layout.SizeInfo.SliceDst trailing => + layout.TrailingSliceLayoutUsize.size_for_elems trailing self + +/-- [zerocopy::pointer_metadata_unit_from_elem_count]: + Source: 'src/lib.rs', lines 1023:0-1025:1 -/ +def pointer_metadata_unit_from_elem_count + (elems : Std.Usize) : Result Unit := do + Tuple.Insts.ZerocopyPointerMetadata.from_elem_count elems + +/-- [zerocopy::pointer_metadata_unit_to_elem_count]: + Source: 'src/lib.rs', lines 1032:0-1034:1 -/ +def pointer_metadata_unit_to_elem_count : Result Std.Usize := do + Tuple.Insts.ZerocopyPointerMetadata.to_elem_count () + +/-- [zerocopy::pointer_metadata_unit_size_for_metadata]: + Source: 'src/lib.rs', lines 1043:0-1045:1 -/ +def pointer_metadata_unit_size_for_metadata + (runtime_layout : layout.DstLayout) : Result (Option Std.Usize) := do + Tuple.Insts.ZerocopyPointerMetadata.size_for_metadata () runtime_layout + +/-- [zerocopy::pointer_metadata_usize_from_elem_count]: + Source: 'src/lib.rs', lines 1052:0-1054:1 -/ +def pointer_metadata_usize_from_elem_count + (elems : Std.Usize) : Result Std.Usize := do + Usize.Insts.ZerocopyPointerMetadata.from_elem_count elems + +/-- [zerocopy::pointer_metadata_usize_to_elem_count]: + Source: 'src/lib.rs', lines 1061:0-1063:1 -/ +def pointer_metadata_usize_to_elem_count + (metadata : Std.Usize) : Result Std.Usize := do + Usize.Insts.ZerocopyPointerMetadata.to_elem_count metadata + +/-- [zerocopy::pointer_metadata_usize_size_for_metadata]: + Source: 'src/lib.rs', lines 1072:0-1077:1 -/ +def pointer_metadata_usize_size_for_metadata + (metadata : Std.Usize) (runtime_layout : layout.DstLayout) : + Result (Option Std.Usize) + := do + Usize.Insts.ZerocopyPointerMetadata.size_for_metadata metadata runtime_layout + /-- [zerocopy::FromZeros::new_zeroed]: - Source: 'src/lib.rs', lines 3827:4-3833:5 + Source: 'src/lib.rs', lines 3891:4-3897:5 Visibility: public -/ @[trait_default] native_models def FromZeros.new_zeroed.default (Self : Type) : Result Self := do diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index 29a81d0a03..034e0b4350 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -272,7 +272,7 @@ structure pointer.invariant.Alignment (Self : Type) where T /-- Trait declaration: [zerocopy::TryFromBytes] - Source: 'src/lib.rs', lines 1901:0-3451:1 + Source: 'src/lib.rs', lines 1965:0-3515:1 Visibility: public -/ structure TryFromBytes (Self : Type) where only_derive_is_allowed_to_implement_this_trait : Result Unit @@ -283,7 +283,7 @@ structure TryFromBytes (Self : Type) where pointer.invariant.Initialized → Result Bool /-- Trait declaration: [zerocopy::FromZeros] - Source: 'src/lib.rs', lines 3708:0-4074:1 + Source: 'src/lib.rs', lines 3772:0-4138:1 Visibility: public -/ structure FromZeros (Self : Type) where TryFromBytesInst : TryFromBytes Self @@ -291,20 +291,20 @@ structure FromZeros (Self : Type) where new_zeroed : Result Self /-- Trait declaration: [zerocopy::FromBytes] - Source: 'src/lib.rs', lines 4302:0-5714:1 + Source: 'src/lib.rs', lines 4366:0-5778:1 Visibility: public -/ structure FromBytes (Self : Type) where FromZerosInst : FromZeros Self only_derive_is_allowed_to_implement_this_trait : Result Unit /-- Trait declaration: [zerocopy::IntoBytes] - Source: 'src/lib.rs', lines 5953:0-6426:1 + Source: 'src/lib.rs', lines 6017:0-6490:1 Visibility: public -/ 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 + Source: 'src/lib.rs', lines 6628:0-6635:1 Visibility: public -/ structure Unaligned (Self : Type) where only_derive_is_allowed_to_implement_this_trait : Result Unit diff --git a/verification/aeneas/lean/Obligations/PointerMetadata.lean b/verification/aeneas/lean/Obligations/PointerMetadata.lean new file mode 100644 index 0000000000..105d09cb91 --- /dev/null +++ b/verification/aeneas/lean/Obligations/PointerMetadata.lean @@ -0,0 +1,66 @@ +/- 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 LayoutModel +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Obligations +open Zerocopy.Proofs +set_option linter.unusedVariables false + +/- Concrete wrappers call the actual trait implementations. These expectations +retain their complete raw domain and distinguish overflow from execution +failure, without using an extracted operation to define the expected result. -/ +def pointer_metadata_unit_from_elem_count_spec_contract (elems : Usize) + (run : Result Unit) : Prop := run ⦃ result => result = () ⦄ +def pointer_metadata_unit_from_elem_count_spec : Prop := ∀ elems, + pointer_metadata_unit_from_elem_count_spec_contract elems + (pointer_metadata_unit_from_elem_count elems) + +def pointer_metadata_unit_to_elem_count_spec_contract (run : Result Usize) : Prop := run ⦃ result => result.val = 0 ⦄ +def pointer_metadata_unit_to_elem_count_spec : Prop := + pointer_metadata_unit_to_elem_count_spec_contract pointer_metadata_unit_to_elem_count + +def pointer_metadata_usize_from_elem_count_spec_contract (elems : Usize) + (run : Result Usize) : Prop := run ⦃ result => result.val = elems.val ⦄ +def pointer_metadata_usize_from_elem_count_spec : Prop := ∀ elems, + pointer_metadata_usize_from_elem_count_spec_contract elems + (pointer_metadata_usize_from_elem_count elems) + +def pointer_metadata_usize_to_elem_count_spec_contract (metadata : Usize) + (run : Result Usize) : Prop := run ⦃ result => result.val = metadata.val ⦄ +def pointer_metadata_usize_to_elem_count_spec : Prop := ∀ metadata, + pointer_metadata_usize_to_elem_count_spec_contract metadata + (pointer_metadata_usize_to_elem_count metadata) + +def pointer_metadata_unit_size_for_metadata_spec_contract (runtime_layout : layout.DstLayout) (run : Result (Option Usize)) : Prop := + layoutValid runtime_layout → run ⦃ result => + match runtime_layout.size_info with + | .Sized bytes => ∃ size, result = some size ∧ size.val = bytes.val + | .SliceDst _ => result = none ⦄ +def pointer_metadata_unit_size_for_metadata_spec : Prop := ∀ runtime_layout, + pointer_metadata_unit_size_for_metadata_spec_contract runtime_layout + (pointer_metadata_unit_size_for_metadata runtime_layout) + +def pointer_metadata_usize_size_for_metadata_spec_contract (metadata : Usize) + (runtime_layout : layout.DstLayout) (run : Result (Option Usize)) : Prop := + layoutValid runtime_layout → run ⦃ result => + match runtime_layout.size_info with + | .Sized _ => result = none + | .SliceDst tail => match result with + | none => Usize.max < (trailingFormula tail).size metadata.val + | some size => size.val = (trailingFormula tail).size metadata.val ∧ + (trailingFormula tail).size metadata.val ≤ Usize.max ⦄ +def pointer_metadata_usize_size_for_metadata_spec : Prop := ∀ metadata runtime_layout, + pointer_metadata_usize_size_for_metadata_spec_contract metadata runtime_layout + (pointer_metadata_usize_size_for_metadata metadata runtime_layout) + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs/PointerMetadata.lean b/verification/aeneas/lean/Proofs/PointerMetadata.lean new file mode 100644 index 0000000000..cb1dc6c1a8 --- /dev/null +++ b/verification/aeneas/lean/Proofs/PointerMetadata.lean @@ -0,0 +1,121 @@ +/- 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 Proofs +public import RequiredModelContracts.PointerMetadata +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw.PointerMetadata + +/- The wrapper unfolds to the extracted concrete trait method. These proofs +retain that call, rather than substitute a second arithmetic implementation. -/ +theorem pointer_metadata_unit_from_elem_count_spec (elems : Usize) : + Zerocopy.pointer_metadata_unit_from_elem_count elems ⦃ result => result = () ⦄ := by + simp [Zerocopy.pointer_metadata_unit_from_elem_count, + Tuple.Insts.ZerocopyPointerMetadata.from_elem_count, WP.spec_ok] + +theorem pointer_metadata_unit_to_elem_count_spec : + Zerocopy.pointer_metadata_unit_to_elem_count ⦃ result => result.val = 0 ⦄ := by + simp [Zerocopy.pointer_metadata_unit_to_elem_count, + Tuple.Insts.ZerocopyPointerMetadata.to_elem_count, WP.spec_ok] + +theorem pointer_metadata_usize_from_elem_count_spec (elems : Usize) : + Zerocopy.pointer_metadata_usize_from_elem_count elems ⦃ result => result = elems ⦄ := by + simp [Zerocopy.pointer_metadata_usize_from_elem_count, + Usize.Insts.ZerocopyPointerMetadata.from_elem_count, WP.spec_ok] + +theorem pointer_metadata_usize_to_elem_count_spec (metadata : Usize) : + Zerocopy.pointer_metadata_usize_to_elem_count metadata ⦃ result => result = metadata ⦄ := by + simp [Zerocopy.pointer_metadata_usize_to_elem_count, + Usize.Insts.ZerocopyPointerMetadata.to_elem_count, WP.spec_ok] + +theorem pointer_metadata_unit_size_for_metadata_spec (runtime_layout : layout.DstLayout) : + Zerocopy.pointer_metadata_unit_size_for_metadata runtime_layout ⦃ result => + result = match runtime_layout.size_info with + | .Sized size => some size + | .SliceDst _ => none ⦄ := by + unfold Zerocopy.pointer_metadata_unit_size_for_metadata + Tuple.Insts.ZerocopyPointerMetadata.size_for_metadata + cases runtime_layout.size_info <;> simp [WP.spec_ok] + +theorem pointer_metadata_usize_size_for_metadata_spec (metadata : Usize) + (runtime_layout : layout.DstLayout) + (positive : match runtime_layout.size_info with + | .Sized _ => True + | .SliceDst tail => 0 < tail.size_rounding_align_and_phase._0.val.val) : + Zerocopy.pointer_metadata_usize_size_for_metadata metadata runtime_layout ⦃ result => + result.map UScalar.val = match runtime_layout.size_info with + | .Sized _ => none + | .SliceDst tail => (trailingFormula tail).checkedSize Usize.max metadata.val ⦄ := by + unfold Zerocopy.pointer_metadata_usize_size_for_metadata + Usize.Insts.ZerocopyPointerMetadata.size_for_metadata + cases info : runtime_layout.size_info with + | Sized size => simp [WP.spec_ok] + | SliceDst tail => + simp only [info] at positive + exact Zerocopy.Proofs.Raw.size_for_elems_spec tail metadata positive + +end Zerocopy.Proofs.Raw.PointerMetadata + +namespace Zerocopy.Proofs +open AeneasSpecs + +theorem pointer_metadata_unit_from_elem_count_spec : Specs.pointer_metadata_unit_from_elem_count_spec := by + unfold Specs.pointer_metadata_unit_from_elem_count_spec + representation_simps + intro elems + apply WP.spec_mono (Raw.PointerMetadata.pointer_metadata_unit_from_elem_count_spec elems) + intro result _facts + exact ⟨result, rfl⟩ +register_spec_step pointer_metadata_unit_from_elem_count_spec + +theorem pointer_metadata_unit_to_elem_count_spec : Specs.pointer_metadata_unit_to_elem_count_spec := by + unfold Specs.pointer_metadata_unit_to_elem_count_spec + representation_simps + exact Raw.PointerMetadata.pointer_metadata_unit_to_elem_count_spec +register_spec_step pointer_metadata_unit_to_elem_count_spec + +theorem pointer_metadata_usize_from_elem_count_spec : Specs.pointer_metadata_usize_from_elem_count_spec := by + unfold Specs.pointer_metadata_usize_from_elem_count_spec + representation_simps + intro elems + exact Raw.PointerMetadata.pointer_metadata_usize_from_elem_count_spec elems +register_spec_step pointer_metadata_usize_from_elem_count_spec + +theorem pointer_metadata_usize_to_elem_count_spec : Specs.pointer_metadata_usize_to_elem_count_spec := by + unfold Specs.pointer_metadata_usize_to_elem_count_spec + representation_simps + intro metadata + exact Raw.PointerMetadata.pointer_metadata_usize_to_elem_count_spec metadata +register_spec_step pointer_metadata_usize_to_elem_count_spec + +theorem pointer_metadata_unit_size_for_metadata_spec : Specs.pointer_metadata_unit_size_for_metadata_spec := by + unfold Specs.pointer_metadata_unit_size_for_metadata_spec + representation_simps + intro runtime_layout _valid + exact Raw.PointerMetadata.pointer_metadata_unit_size_for_metadata_spec runtime_layout +register_spec_step pointer_metadata_unit_size_for_metadata_spec + +theorem pointer_metadata_usize_size_for_metadata_spec : Specs.pointer_metadata_usize_size_for_metadata_spec := by + unfold Specs.pointer_metadata_usize_size_for_metadata_spec + representation_simps + intro metadata runtime_layout valid + have positive : match runtime_layout.size_info with + | .Sized _ => True + | .SliceDst tail => 0 < tail.size_rounding_align_and_phase._0.val.val := by + cases info : runtime_layout.size_info with + | Sized size => trivial + | SliceDst tail => simpa only [info] using valid.2 + exact Raw.PointerMetadata.pointer_metadata_usize_size_for_metadata_spec + metadata runtime_layout positive +register_spec_step pointer_metadata_usize_size_for_metadata_spec + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RequiredModelContracts/PointerMetadata.lean b/verification/aeneas/lean/RequiredModelContracts/PointerMetadata.lean new file mode 100644 index 0000000000..640bec3d15 --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/PointerMetadata.lean @@ -0,0 +1,86 @@ +/- 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 Obligations.PointerMetadata +public import RequiredModelContracts +@[expose] public section + +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +/- Every adapter consumes the supplied contract for the same arbitrary run. +No canonical implementation theorem is used to repair a weak specification. -/ +@[contract_simps] theorem required_pointer_metadata_unit_from_elem_count (elems : Usize) + (run : Result Unit) + (provided : Specs.pointer_metadata_unit_from_elem_count_spec_contract elems run) : + Obligations.pointer_metadata_unit_from_elem_count_spec_contract elems run := by + apply WP.spec_mono (provided (unsignedWord elems) rfl) + rintro result ⟨_value, _decoded, facts⟩ + exact facts + +@[contract_simps] theorem required_pointer_metadata_unit_to_elem_count (run : Result Usize) + (provided : Specs.pointer_metadata_unit_to_elem_count_spec_contract run) : + Obligations.pointer_metadata_unit_to_elem_count_spec_contract run := by + apply WP.spec_mono provided + rintro result ⟨_value, _decoded, facts⟩ + exact facts + +@[contract_simps] theorem required_pointer_metadata_usize_from_elem_count (elems : Usize) + (run : Result Usize) + (provided : Specs.pointer_metadata_usize_from_elem_count_spec_contract elems run) : + Obligations.pointer_metadata_usize_from_elem_count_spec_contract elems run := by + apply WP.spec_mono (provided (unsignedWord elems) rfl) + rintro result ⟨_value, _decoded, facts⟩ + exact congrArg UScalar.val facts + +@[contract_simps] theorem required_pointer_metadata_usize_to_elem_count (metadata : Usize) + (run : Result Usize) + (provided : Specs.pointer_metadata_usize_to_elem_count_spec_contract metadata run) : + Obligations.pointer_metadata_usize_to_elem_count_spec_contract metadata run := by + apply WP.spec_mono (provided (unsignedWord metadata) rfl) + rintro result ⟨_value, _decoded, facts⟩ + exact congrArg UScalar.val facts + +@[contract_simps] theorem required_pointer_metadata_unit_size_for_metadata (runtime_layout : layout.DstLayout) (run : Result (Option Usize)) + (provided : Specs.pointer_metadata_unit_size_for_metadata_spec_contract runtime_layout run) : + Obligations.pointer_metadata_unit_size_for_metadata_spec_contract runtime_layout run := by + intro valid + obtain ⟨value, decoded⟩ := (layout_valid_iff runtime_layout).mpr valid + apply WP.spec_mono (provided value decoded) + rintro result ⟨_value, _decoded, facts⟩ + cases info : runtime_layout.size_info with + | Sized bytes => + simp only [info] at facts ⊢ + exact ⟨bytes, facts, rfl⟩ + | SliceDst tail => simpa only [info] using facts + +@[contract_simps] theorem required_pointer_metadata_usize_size_for_metadata (metadata : Usize) + (runtime_layout : layout.DstLayout) (run : Result (Option Usize)) + (provided : Specs.pointer_metadata_usize_size_for_metadata_spec_contract metadata runtime_layout run) : + Obligations.pointer_metadata_usize_size_for_metadata_spec_contract metadata runtime_layout run := by + intro valid + obtain ⟨value, decoded⟩ := (layout_valid_iff runtime_layout).mpr valid + apply WP.spec_mono (provided (unsignedWord metadata) rfl value decoded) + rintro result ⟨_value, _decoded, facts⟩ + cases info : runtime_layout.size_info with + | Sized bytes => + simp only [info] at facts ⊢ + cases result <;> simp_all + | SliceDst tail => + simp only [info] at facts ⊢ + cases result with + | none => + simp only [Option.map_none, LayoutMath.Formula.checkedSize] at facts + split at facts <;> simp_all + | some size => + simp only [Option.map_some, LayoutMath.Formula.checkedSize] at facts + split at facts <;> simp_all + +end Zerocopy.Proofs diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index 63880497bc..b7282fb76c 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/verification/aeneas/projections/Specs.lean @@ -317,6 +317,58 @@ spec trailing_arithmetic_check_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.trailing_arithmetic_check_spec for Zerocopy.layout.tail_checks.trailing_arithmetic_check with 5 +check_model_inputs Zerocopy.pointer_metadata_unit_from_elem_count with 0 type parameters +aeneas_spec_begin +spec pointer_metadata_unit_from_elem_count_spec + for @Zerocopy.pointer_metadata_unit_from_elem_count with 0 type parameters + ensures(raw) result => result = () +aeneas_spec_end +check_spec_binding Zerocopy.Specs.pointer_metadata_unit_from_elem_count_spec for Zerocopy.pointer_metadata_unit_from_elem_count with 1 + +check_model_inputs Zerocopy.pointer_metadata_unit_to_elem_count with 0 type parameters +aeneas_spec_begin +spec pointer_metadata_unit_to_elem_count_spec + for @Zerocopy.pointer_metadata_unit_to_elem_count with 0 type parameters + ensures(raw) result => result.val = 0 +aeneas_spec_end +check_spec_binding Zerocopy.Specs.pointer_metadata_unit_to_elem_count_spec for Zerocopy.pointer_metadata_unit_to_elem_count with 0 + +check_model_inputs Zerocopy.pointer_metadata_unit_size_for_metadata with 0 type parameters +aeneas_spec_begin +spec pointer_metadata_unit_size_for_metadata_spec + for @Zerocopy.pointer_metadata_unit_size_for_metadata with 0 type parameters + ensures(raw) result => result = match runtime_layout.size_info with + | .Sized size => some size + | .SliceDst _ => none +aeneas_spec_end +check_spec_binding Zerocopy.Specs.pointer_metadata_unit_size_for_metadata_spec for Zerocopy.pointer_metadata_unit_size_for_metadata with 1 + +check_model_inputs Zerocopy.pointer_metadata_usize_from_elem_count with 0 type parameters +aeneas_spec_begin +spec pointer_metadata_usize_from_elem_count_spec + for @Zerocopy.pointer_metadata_usize_from_elem_count with 0 type parameters + ensures(raw) result => result = elems +aeneas_spec_end +check_spec_binding Zerocopy.Specs.pointer_metadata_usize_from_elem_count_spec for Zerocopy.pointer_metadata_usize_from_elem_count with 1 + +check_model_inputs Zerocopy.pointer_metadata_usize_to_elem_count with 0 type parameters +aeneas_spec_begin +spec pointer_metadata_usize_to_elem_count_spec + for @Zerocopy.pointer_metadata_usize_to_elem_count with 0 type parameters + ensures(raw) result => result = metadata +aeneas_spec_end +check_spec_binding Zerocopy.Specs.pointer_metadata_usize_to_elem_count_spec for Zerocopy.pointer_metadata_usize_to_elem_count with 1 + +check_model_inputs Zerocopy.pointer_metadata_usize_size_for_metadata with 0 type parameters +aeneas_spec_begin +spec pointer_metadata_usize_size_for_metadata_spec + for @Zerocopy.pointer_metadata_usize_size_for_metadata with 0 type parameters + ensures(raw) result => result.map UScalar.val = match runtime_layout.size_info with + | .Sized _ => none + | .SliceDst tail => (trailingFormula tail).checkedSize Usize.max metadata.val +aeneas_spec_end +check_spec_binding Zerocopy.Specs.pointer_metadata_usize_size_for_metadata_spec for Zerocopy.pointer_metadata_usize_size_for_metadata with 2 + default_trait_body Zerocopy.FromZeros.new_zeroed.default for Zerocopy.FromZeros with 1 type parameters check_model_inputs Zerocopy.FromZeros.new_zeroed.default with 1 type parameters aeneas_spec_begin diff --git a/zerocopy/src/lib.rs b/zerocopy/src/lib.rs index c3d3af1501..147d350695 100644 --- a/zerocopy/src/lib.rs +++ b/zerocopy/src/lib.rs @@ -980,8 +980,8 @@ impl PointerMetadata for () { } #[inline] - fn size_for_metadata(self, layout: DstLayout) -> Option { - match layout.size_info { + fn size_for_metadata(self, runtime_layout: DstLayout) -> Option { + match runtime_layout.size_info { SizeInfo::Sized { size } => Some(size), // NOTE: This branch is unreachable, but we return `None` rather // than `unreachable!()` to avoid generating panic paths. @@ -1002,8 +1002,8 @@ impl PointerMetadata for usize { } #[inline] - fn size_for_metadata(self, layout: DstLayout) -> Option { - match layout.size_info { + fn size_for_metadata(self, runtime_layout: DstLayout) -> Option { + match runtime_layout.size_info { SizeInfo::SliceDst(trailing) => trailing.size_for_elems(self), // NOTE: This branch is unreachable, but we return `None` rather // than `unreachable!()` to avoid generating panic paths. @@ -1012,6 +1012,70 @@ impl PointerMetadata for usize { } } +// The annotation frontend binds free roots, rather than trait impl methods. +// These concrete calls retain the production dictionaries and method bodies +// in extraction; they introduce no alternate implementation of metadata. +#[allow(dead_code)] +/// ```aeneas +/// spec pointer_metadata_unit_from_elem_count_spec +/// ensures(raw) result => result = () +/// ``` +pub(crate) fn pointer_metadata_unit_from_elem_count(elems: usize) { + <() as PointerMetadata>::from_elem_count(elems) +} + +#[allow(dead_code)] +/// ```aeneas +/// spec pointer_metadata_unit_to_elem_count_spec +/// ensures(raw) result => result.val = 0 +/// ``` +pub(crate) fn pointer_metadata_unit_to_elem_count() -> usize { + <() as PointerMetadata>::to_elem_count(()) +} + +#[allow(dead_code)] +/// ```aeneas +/// spec pointer_metadata_unit_size_for_metadata_spec +/// ensures(raw) result => result = match runtime_layout.size_info with +/// | .Sized size => some size +/// | .SliceDst _ => none +/// ``` +pub(crate) fn pointer_metadata_unit_size_for_metadata(runtime_layout: DstLayout) -> Option { + <() as PointerMetadata>::size_for_metadata((), runtime_layout) +} + +#[allow(dead_code)] +/// ```aeneas +/// spec pointer_metadata_usize_from_elem_count_spec +/// ensures(raw) result => result = elems +/// ``` +pub(crate) fn pointer_metadata_usize_from_elem_count(elems: usize) -> usize { + ::from_elem_count(elems) +} + +#[allow(dead_code)] +/// ```aeneas +/// spec pointer_metadata_usize_to_elem_count_spec +/// ensures(raw) result => result = metadata +/// ``` +pub(crate) fn pointer_metadata_usize_to_elem_count(metadata: usize) -> usize { + ::to_elem_count(metadata) +} + +#[allow(dead_code)] +/// ```aeneas +/// spec pointer_metadata_usize_size_for_metadata_spec +/// ensures(raw) result => result.map UScalar.val = match runtime_layout.size_info with +/// | .Sized _ => none +/// | .SliceDst tail => (trailingFormula tail).checkedSize Usize.max metadata.val +/// ``` +pub(crate) fn pointer_metadata_usize_size_for_metadata( + metadata: usize, + runtime_layout: DstLayout, +) -> Option { + ::size_for_metadata(metadata, runtime_layout) +} + // SAFETY: Delegates safety to `DstLayout::for_slice`. unsafe impl KnownLayout for [T] { #[allow(clippy::missing_inline_in_public_items, dead_code)]