From 000a31f86ce9129c6c4c02f660612d2da8e37f25 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Mon, 5 Oct 2026 13:08:01 -0400 Subject: [PATCH] Prove numerical cast plan selection and metadata conversion Accepted plans preserve complete rounded sizes for every natural element count and retain the destination alignment requirement. Prove both selection paths, then prove the unchecked metadata implementation returns its exact affine map whenever its product and sum fit. Rejected plans remain conservative. Extract the actual numerical functions, retain independent arbitrary-outcome contract checks, and document the restricted external correspondence for unchecked integer operations. Pointer construction is outside these claims. Validation: fresh extraction, required proofs and axiom audit; MSRV, stable, nightly and workspace Clippy checks. Agent-authored-by: AI agent acting on joshlf's behalf gherrit-pr-id: Gdbl6xaqz63ttxnug4rlquswinz6f64o6 --- verification/aeneas/README.md | 4 + verification/aeneas/SEMANTICS.md | 8 + verification/aeneas/golden/Funs.lean | 2006 +++++++++-------- .../aeneas/golden/FunsExternal_Template.lean | 16 + verification/aeneas/golden/Types.lean | 78 +- verification/aeneas/lean/CastMath.lean | 44 + verification/aeneas/lean/LayoutModel.lean | 34 + .../aeneas/lean/Obligations/CastPlan.lean | 78 + .../aeneas/lean/Proofs/CastArithmetic.lean | 65 + .../aeneas/lean/Proofs/CastSelection.lean | 221 ++ .../aeneas/lean/Proofs/CastSequence.lean | 72 + .../lean/RequiredModelContracts/CastPlan.lean | 71 + .../aeneas/lean/Zerocopy/FunsExternal.lean | 7 + zerocopy/src/layout/cast_from.rs | 22 +- zerocopy/src/layout/mod.rs | 6 + 15 files changed, 1767 insertions(+), 965 deletions(-) create mode 100644 verification/aeneas/lean/CastMath.lean create mode 100644 verification/aeneas/lean/Obligations/CastPlan.lean create mode 100644 verification/aeneas/lean/Proofs/CastArithmetic.lean create mode 100644 verification/aeneas/lean/Proofs/CastSelection.lean create mode 100644 verification/aeneas/lean/Proofs/CastSequence.lean create mode 100644 verification/aeneas/lean/RequiredModelContracts/CastPlan.lean diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 7494d3f4cc..8f3f164ba5 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -778,6 +778,10 @@ records but does not formally prove: Rust values by admitting zero; the generated conditional contracts assume successful recursive decoding of inputs and prove it for returned values. This introduces no axiom asserting that every modeled wrapper is nonzero. +- The external `usize::unchecked_mul` and `usize::unchecked_add` models + return the exact product and sum on non-overflowing inputs. Their Lean + definitions use checked arithmetic, and every use proves both results fit. + They claim no Rust behavior outside that domain. - Lean's kernel, its standard logic axioms, and the imported proof artifacts check the encoded propositions correctly. Release checksums establish artifact identity, not a proof of compiler or model correctness. diff --git a/verification/aeneas/SEMANTICS.md b/verification/aeneas/SEMANTICS.md index 2a89db4cd0..cbfcd427de 100644 --- a/verification/aeneas/SEMANTICS.md +++ b/verification/aeneas/SEMANTICS.md @@ -108,6 +108,14 @@ it into a power-of-two alignment and bounded phase; structural layout models reuse that shared pair. This admission law has an ordinary Lean proof and does not change the extracted raw implementation. +The extracted cast metadata helper uses Rust's unsafe `usize::unchecked_mul` +and `usize::unchecked_add`. Their handwritten external models use Aeneas's +checked multiplication and addition. The correspondence premise is restricted +to non-overflowing inputs: each call returns the exact natural-number result. +No correspondence is claimed for overflowing inputs, where Rust's unchecked +operations have undefined behavior. The arithmetic contracts prove both +intermediate results fit. + The remaining trusted boundary is the pinned Rust-to-LLBC-to-Lean translation, its builtin arithmetic and control-flow models, the external primitive correspondences above, the Lean kernel, and specification adequacy. Both diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index 9bb9209aa1..daeba92e69 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -642,907 +642,1149 @@ def byteorder.verification.set_u32_be value n byteorder.U32.get byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder value1 -/-- [zerocopy::layout::composition_checks::matches_reference]: - Source: 'src/layout/composition_checks.rs', lines 57:0-75:1 -/ -def layout.composition_checks.matches_reference - (runtime_layout : layout.DstLayout) - (reference : layout.composition_checks.ReferenceLayout) : - Result Bool +/-- [zerocopy::util::round_down_to_next_multiple_of_alignment]: + Source: 'src/util/mod.rs', lines 262:0-280:1 -/ +def util.round_down_to_next_multiple_of_alignment + (n : Std.Usize) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) : + Result Std.Usize + := do + let align1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + let b ← core.num.Usize.is_power_of_two align1 + massert b + let i ← align1 - 1#usize + let mask ← lift (~~~ i) + ok (n &&& mask) + +/-- [zerocopy::layout::POINTER_WIDTH_BITS] + Source: 'src/layout/mod.rs', lines 32:0-32:62 -/ +@[global_simps, irreducible] +def layout.POINTER_WIDTH_BITS : Result Std.Usize := do + let i ← core.mem.size_of Std.Usize + i * 8#usize + +/-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::components]: + Source: 'src/layout/mod.rs', lines 145:4-172:5 -/ +def layout.RoundingAlignAndPhase.components + (self : layout.RoundingAlignAndPhase) : + Result ((core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) × Std.Usize) + := do + let i ← layout.POINTER_WIDTH_BITS + let i1 ← i - 1#usize + let i2 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner self._0 + let i3 ← lift (core.num.Usize.leading_zeros i2) + let i4 ← lift (UScalar.cast .Usize i3) + let shift ← i1 - i4 + let align ← 1#usize <<< shift + let o ← + core.num.nonzero.NonZero.new + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + match o with + | none => fail panic + | some align1 => + let i5 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align1 + let phase ← lift (i2 ^^^ i5) + ok (align1, phase) + +/-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::new]: + Source: 'src/layout/mod.rs', lines 112:4-131:5 -/ +def layout.RoundingAlignAndPhase.new + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) : + Result layout.RoundingAlignAndPhase := do let i ← core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner - runtime_layout.align - if i = reference.align - then - if runtime_layout.statically_shallow_unpadded = reference.unpadded - then - match runtime_layout.size_info with - | layout.SizeInfo.Sized size => - match reference.size with - | layout.composition_checks.ReferenceSize.Fixed expected => - ok (size = expected) - | layout.composition_checks.ReferenceSize.Tail _ => ok false - | layout.SizeInfo.SliceDst actual => - match reference.size with - | layout.composition_checks.ReferenceSize.Fixed _ => ok false - | layout.composition_checks.ReferenceSize.Tail expected => - let b ← core.num.Usize.is_power_of_two expected.round_align - if b - then - if expected.phase < expected.round_align - then - if actual.offset = expected.offset - then - if actual.elem_size = expected.elem_size - then - if actual.size_base = expected.base - then - let o ← - lift (Usize.checked_add expected.round_align - expected.phase) - match o with - | none => ok false - | some encoded => - let i1 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner - actual.size_rounding_align_and_phase._0 - ok (i1 = encoded) - else ok false - else ok false - else ok false - else ok false - else ok false - else ok false - else ok false + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + let b ← core.num.Usize.is_power_of_two i + massert b + massert (phase < i) + let encoded ← lift (i ||| phase) + let o ← + core.num.nonzero.NonZero.new + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner encoded + match o with + | none => fail panic + | some encoded1 => ok { _0 := encoded1 } -/-- [zerocopy::layout::composition_checks::reference_round_up]: - Source: 'src/layout/composition_checks.rs', lines 78:0-84:1 -/ -def layout.composition_checks.reference_round_up - (bytes : Std.Usize) (align : Std.Usize) : Result (Option Std.Usize) := do - if align = 0#usize +/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::advance]: + Source: 'src/layout/mod.rs', lines 706:4-802:5 -/ +def layout.TrailingSliceLayoutUsize.advance + (self : layout.TrailingSliceLayout Std.Usize) (bytes : Std.Usize) + (elem_size : Std.Usize) : + Result (Option (layout.TrailingSliceLayout Std.Usize)) + := do + let (size_align, size_phase) ← + layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner size_align + let align_mask ← i - 1#usize + let i1 ← core.num.Usize.MAX - self.size_base + let phase_capacity ← lift (i1 ||| align_mask) + let max_advance ← phase_capacity - size_phase + if bytes > max_advance then ok none else - let i ← bytes % align - let i1 ← align - i - let padding ← i1 % align - ok (Usize.checked_add bytes padding) - -/-- [zerocopy::layout::composition_checks::extension_alignment]: - Source: 'src/layout/composition_checks.rs', lines 87:0-89:1 -/ -def layout.composition_checks.extension_alignment - (align : Std.Usize) : Result Bool := do - let b ← core.num.Usize.is_power_of_two align - if b - then let i ← 1#usize <<< 29#i32 - ok (align <= i) - else ok false + let advanced_phase ← size_phase + bytes + let normalized_phase ← lift (advanced_phase &&& align_mask) + let whole_bytes ← + util.round_down_to_next_multiple_of_alignment advanced_phase size_align + let size_base ← self.size_base + whole_bytes + let raap ← layout.RoundingAlignAndPhase.new size_align normalized_phase + ok (some + { self with elem_size, size_base, size_rounding_align_and_phase := raap }) -/-- [zerocopy::layout::composition_checks::reference_extend_at]: - Source: 'src/layout/composition_checks.rs', lines 121:0-156:1 -/ -def layout.composition_checks.reference_extend_at - (preceding : layout.composition_checks.ReferenceLayout) - (field : layout.composition_checks.ReferenceLayout) (field_align : Std.Usize) - : - Result (Option layout.composition_checks.ReferenceLayout) +/-- [zerocopy::util::padding_needed_for]: + Source: 'src/util/mod.rs', lines 170:0-230:1 -/ +def util.padding_needed_for + (len : Std.Usize) + (align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) : + Result Std.Usize := do - match preceding.size with - | layout.composition_checks.ReferenceSize.Fixed bytes => - let o ← layout.composition_checks.reference_round_up bytes field_align - match o with - | none => ok none - | some offset => - match field.size with - | layout.composition_checks.ReferenceSize.Fixed bytes1 => - let o1 ← lift (Usize.checked_add offset bytes1) - match o1 with - | none => ok none - | some size => - let i ← - if preceding.align > field_align - then ok preceding.align - else ok field_align - ok (some - { - align := i, - size := (layout.composition_checks.ReferenceSize.Fixed size), - unpadded := - ((preceding.unpadded && field.unpadded) && (offset = bytes)) - }) - | layout.composition_checks.ReferenceSize.Tail tail => - let o1 ← lift (Usize.checked_add offset tail.offset) - match o1 with - | none => ok none - | some offset1 => - let o2 ← lift (Usize.checked_add offset tail.base) - match o2 with - | none => ok none - | some base => - let i ← - if preceding.align > field_align - then ok preceding.align - else ok field_align - ok (some - { - align := i, - size := - (layout.composition_checks.ReferenceSize.Tail - { tail with offset := offset1, base }), - unpadded := - ((preceding.unpadded && field.unpadded) && (offset = bytes)) - }) - | layout.composition_checks.ReferenceSize.Tail _ => ok none + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + let mask ← i - 1#usize + let i1 ← lift (core.num.Usize.wrapping_sub len 1#usize) + let i2 ← lift (~~~ i1) + ok (i2 &&& mask) -/-- [zerocopy::layout::composition_checks::reference_extend]: - Source: 'src/layout/composition_checks.rs', lines 95:0-117:1 -/ -def layout.composition_checks.reference_extend - (preceding : layout.composition_checks.ReferenceLayout) - (field : layout.composition_checks.ReferenceLayout) - (packed : Option (core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner)) : - Result (Option layout.composition_checks.ReferenceLayout) - := do - let b ← layout.composition_checks.extension_alignment preceding.align - if b - then - let b1 ← layout.composition_checks.extension_alignment field.align - if b1 - then - match packed with - | none => - layout.composition_checks.reference_extend_at preceding field - field.align - | some cap => - let i ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner cap - let b2 ← layout.composition_checks.extension_alignment i - if b2 - then - let field_align ← if field.align < i - then ok field.align - else ok i - layout.composition_checks.reference_extend_at preceding field - field_align - else ok none - else ok none - else ok none - -/-- [zerocopy::layout::composition_checks::reference_pad]: - Source: 'src/layout/composition_checks.rs', lines 159:0-194:1 -/ -def layout.composition_checks.reference_pad - (reference : layout.composition_checks.ReferenceLayout) : - Result (Option layout.composition_checks.ReferenceLayout) - := do - let b ← core.num.Usize.is_power_of_two reference.align - if b - then - match reference.size with - | layout.composition_checks.ReferenceSize.Fixed bytes => - let o ← - layout.composition_checks.reference_round_up bytes reference.align - match o with - | none => ok none - | some rounded => - ok (some - { - reference - with - size := (layout.composition_checks.ReferenceSize.Fixed rounded), - unpadded := (reference.unpadded && (rounded = bytes)) - }) - | layout.composition_checks.ReferenceSize.Tail tail => - let b1 ← core.num.Usize.is_power_of_two tail.round_align - if b1 - then - if tail.phase >= tail.round_align - then ok none - else - if tail.round_align >= reference.align - then - let o ← - layout.composition_checks.reference_round_up tail.base - reference.align - match o with - | none => ok none - | some base => - ok (some - { - reference - with - size := - (layout.composition_checks.ReferenceSize.Tail - { tail with base }), - unpadded := (reference.unpadded && true) - }) - else - let o ← - layout.composition_checks.reference_round_up tail.base - tail.round_align - match o with - | none => ok none - | some base => - let o1 ← lift (Usize.checked_add base tail.phase) - match o1 with - | none => ok none - | some fixed => - let phase ← fixed % reference.align - let base1 ← fixed - phase - ok (some - { - reference - with - size := - (layout.composition_checks.ReferenceSize.Tail - { - tail - with - base := base1, - round_align := reference.align, - phase - }), - unpadded := (reference.unpadded && true) - }) - else ok none - else ok none - -/-- [zerocopy::util::min]: - Source: 'src/util/mod.rs', lines 306:0-312:1 -/ -def util.min - (a : core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner) - (b : core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner) : - Result (core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner) - := do - let i ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner a - let i1 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner b - if i > i1 - then ok b - else ok a - -/-- [zerocopy::util::max]: - Source: 'src/util/mod.rs', lines 290:0-296:1 -/ -def util.max - (a : core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner) - (b : core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner) : - Result (core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner) - := do - let i ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner a - let i1 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner b - if i < i1 - then ok b - else ok a - -/-- [zerocopy::util::padding_needed_for]: - Source: 'src/util/mod.rs', lines 170:0-230:1 -/ -def util.padding_needed_for - (len : Std.Usize) - (align : core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner) : - Result Std.Usize +/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::padding_for_elems]: + Source: 'src/layout/mod.rs', lines 424:4-479:5 -/ +def layout.TrailingSliceLayoutUsize.padding_for_elems + (self : layout.TrailingSliceLayout Std.Usize) (elems : Std.Usize) : + Result Std.Usize := do + let (size_align, size_phase) ← + layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase let i ← core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align - let mask ← i - 1#usize - let i1 ← lift (core.num.Usize.wrapping_sub len 1#usize) - let i2 ← lift (~~~ i1) - ok (i2 &&& mask) + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner size_align + let size_mask ← i - 1#usize + let elem_remainder ← lift (self.elem_size &&& size_mask) + let i1 ← lift (core.num.Usize.wrapping_mul elems elem_remainder) + let trailing_remainder ← lift (i1 &&& size_mask) + let rounding_input ← + lift (core.num.Usize.wrapping_add size_phase trailing_remainder) + let rounding_padding ← util.padding_needed_for rounding_input size_align + let i2 ← lift (core.num.Usize.wrapping_add self.size_base size_phase) + let i3 ← lift (core.num.Usize.wrapping_sub i2 self.offset) + ok (core.num.Usize.wrapping_add i3 rounding_padding) -/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::CURRENT_MAX_ALIGN] - Source: 'src/layout/mod.rs', lines 951:4-954:6 -/ -@[global_simps, irreducible] -def layout.DstLayout.CURRENT_MAX_ALIGN - : - Result (core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner) +/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::max_trailing_bytes]: + Source: 'src/layout/mod.rs', lines 310:4-399:5 -/ +def layout.TrailingSliceLayout.max_trailing_bytes + {E : Type} (self : layout.TrailingSliceLayout E) + (available_bytes : Std.Usize) : + Result (Option Std.Usize) := do - let i ← 1#usize <<< 29#i32 - let o ← - core.num.nonzero.NonZero.new - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner i + let (size_align, size_phase) ← + layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase + let rounded_phase ← + if size_phase = 0#usize + then ok 0#usize + else + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner size_align + let o ← lift (Usize.checked_add self.size_base rounded_phase) match o with - | none => fail panic - | some max_align => ok max_align - -/-- [zerocopy::layout::POINTER_WIDTH_BITS] - Source: 'src/layout/mod.rs', lines 32:0-32:62 -/ -@[global_simps, irreducible] -def layout.POINTER_WIDTH_BITS : Result Std.Usize := do - let i ← core.mem.size_of Std.Usize - i * 8#usize + | none => ok none + | some size => + let o1 ← lift (Usize.checked_sub available_bytes size) + match o1 with + | none => ok none + | some bytes => + let aligned_bytes ← + util.round_down_to_next_multiple_of_alignment bytes size_align + let initial_padding ← rounded_phase - size_phase + let trailing_bytes ← lift (aligned_bytes ||| initial_padding) + ok (some trailing_bytes) -/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::THEORETICAL_MAX_ALIGN] - Source: 'src/layout/mod.rs', lines 937:4-941:10 -/ -@[global_simps, irreducible] -def layout.DstLayout.THEORETICAL_MAX_ALIGN - : - Result (core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner) +/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::size_for_elems]: + Source: 'src/layout/mod.rs', lines 497:4-561:5 -/ +def layout.TrailingSliceLayoutUsize.size_for_elems + (self : layout.TrailingSliceLayout Std.Usize) (elems : Std.Usize) : + Result (Option Std.Usize) := do - let i ← layout.POINTER_WIDTH_BITS - let i1 ← i - 1#usize - let i2 ← 1#usize <<< i1 let o ← - core.num.nonzero.NonZero.new - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner i2 + layout.TrailingSliceLayout.max_trailing_bytes self core.num.Usize.MAX match o with - | none => fail panic - | some max_align => ok max_align + | none => ok none + | some bytes => + let o1 ← lift (Usize.checked_mul self.elem_size elems) + match o1 with + | none => ok none + | some bytes1 => + if bytes1 > bytes + then ok none + else + let trailing_end ← + lift (core.num.Usize.wrapping_add self.offset bytes1) + let i ← layout.TrailingSliceLayoutUsize.padding_for_elems self elems + let size ← lift (core.num.Usize.wrapping_add trailing_end i) + ok (some size) -/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::extend]: - Source: 'src/layout/mod.rs', lines 1330:4-1476:5 - Visibility: public -/ -def layout.DstLayout.extend - (self : layout.DstLayout) (field : layout.DstLayout) - (repr_packed : Option (core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner)) : - Result layout.DstLayout +/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::has_same_size_sequence]: + Source: 'src/layout/mod.rs', lines 585:4-662:5 -/ +def layout.TrailingSliceLayoutUsize.has_same_size_sequence + (self : layout.TrailingSliceLayout Std.Usize) + (other : layout.TrailingSliceLayout Std.Usize) : + Result Bool := do - let max_align ← - match repr_packed with - | none => layout.DstLayout.THEORETICAL_MAX_ALIGN - | some max_align1 => ok max_align1 - let i ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner max_align - let b ← core.num.Usize.is_power_of_two i - massert b - let i1 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner self.align - let nz ← layout.DstLayout.CURRENT_MAX_ALIGN - let i2 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner nz - massert (i1 <= i2) - let i3 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner field.align - let i4 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner nz - massert (i3 <= i4) - let _ ← - match repr_packed with - | none => ok none - | some repr_packed1 => - do - let i5 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner - repr_packed1 - let i6 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner nz - massert (i5 <= i6) - ok repr_packed - let field_align ← util.min field.align max_align - let align ← util.max self.align field_align - match self.size_info with - | layout.SizeInfo.Sized preceding_size => - let padding ← util.padding_needed_for preceding_size field_align - let o ← lift (Usize.checked_add preceding_size padding) + if self.elem_size != other.elem_size + then ok false + else + let o ← layout.TrailingSliceLayoutUsize.size_for_elems self 0#usize + let o1 ← layout.TrailingSliceLayoutUsize.size_for_elems other 0#usize match o with - | none => fail panic - | some offset => - match field.size_info with - | layout.SizeInfo.Sized field_size => - let o1 ← lift (Usize.checked_add offset field_size) - match o1 with - | none => fail panic - | some size => - if self.statically_shallow_unpadded - then - if field.statically_shallow_unpadded - then - ok - { - align, - size_info := (layout.SizeInfo.Sized size), - statically_shallow_unpadded := (padding = 0#usize) - } - else - ok - { - align, - size_info := (layout.SizeInfo.Sized size), - statically_shallow_unpadded := false - } + | none => ok false + | some self_size => + match o1 with + | none => ok false + | some other_size => + if self_size = other_size + then + let (self_align, self_phase) ← + layout.RoundingAlignAndPhase.components + self.size_rounding_align_and_phase + let (other_align, other_phase) ← + layout.RoundingAlignAndPhase.components + other.size_rounding_align_and_phase + let self_align1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + self_align + let other_align1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + other_align + let max_align ← + if self_align1 > other_align1 + then ok self_align1 + else ok other_align1 + let i ← self.elem_size % max_align + if i = 0#usize + then ok true else - ok - { - align, - size_info := (layout.SizeInfo.Sized size), - statically_shallow_unpadded := false - } - | layout.SizeInfo.SliceDst tsl => - let o1 ← lift (Usize.checked_add offset tsl.offset) - match o1 with - | none => fail panic - | some offset1 => - let o2 ← lift (Usize.checked_add offset tsl.size_base) - match o2 with - | none => fail panic - | some base => - if self.statically_shallow_unpadded - then - if field.statically_shallow_unpadded - then - ok - { - align, - size_info := - (layout.SizeInfo.SliceDst - { tsl with offset := offset1, size_base := base }), - statically_shallow_unpadded := (padding = 0#usize) - } - else - ok - { - align, - size_info := - (layout.SizeInfo.SliceDst - { tsl with offset := offset1, size_base := base }), - statically_shallow_unpadded := false - } - else - ok - { - align, - size_info := - (layout.SizeInfo.SliceDst - { tsl with offset := offset1, size_base := base }), - statically_shallow_unpadded := false - } - | layout.SizeInfo.SliceDst _ => fail panic + if self_align1 != other_align1 + then ok false + else ok (self_phase = other_phase) + else ok false -/-- [zerocopy::layout::composition_checks::check_extend]: - Source: 'src/layout/composition_checks.rs', lines 203:0-218:1 -/ -def layout.composition_checks.check_extend - (preceding : layout.DstLayout) (field : layout.DstLayout) - (packed : Option (core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner)) - (preceding_reference : layout.composition_checks.ReferenceLayout) - (field_reference : layout.composition_checks.ReferenceLayout) : - Result Unit +/-- [zerocopy::layout::cast_from::{zerocopy::layout::cast_from::CastPlan}::size_sequences_match]: + Source: 'src/layout/cast_from.rs', lines 85:4-99:5 -/ +def layout.cast_from.CastPlan.size_sequences_match + (src : layout.TrailingSliceLayout Std.Usize) + (dst : layout.TrailingSliceLayout Std.Usize) (dst_base : Std.Usize) : + Result Bool := do - let b ← - layout.composition_checks.matches_reference preceding preceding_reference - if b - then - let b1 ← - layout.composition_checks.matches_reference field field_reference - if b1 - then - let o ← - layout.composition_checks.reference_extend preceding_reference - field_reference packed - match o with - | none => ok () - | some expected => - let actual ← layout.DstLayout.extend preceding field packed - let b2 ← layout.composition_checks.matches_reference actual expected - massert b2 - else ok () - else ok () + let o ← lift (Usize.checked_mul dst_base dst.elem_size) + match o with + | none => ok false + | some bytes => + let o1 ← layout.TrailingSliceLayoutUsize.advance dst bytes src.elem_size + match o1 with + | none => ok false + | some advanced => + layout.TrailingSliceLayoutUsize.has_same_size_sequence src advanced -/-- [zerocopy::util::round_down_to_next_multiple_of_alignment]: - Source: 'src/util/mod.rs', lines 262:0-280:1 -/ -def util.round_down_to_next_multiple_of_alignment - (n : Std.Usize) - (align : core.num.nonzero.NonZero Std.Usize +/-- [zerocopy::layout::max_elems_for_bytes]: + Source: 'src/layout/mod.rs', lines 892:0-907:1 -/ +def layout.max_elems_for_bytes + (bytes : Std.Usize) + (elem_size : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner) : + Result (Std.Usize × Std.Usize) + := do + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner elem_size + let elems ← bytes / i + let o ← lift (Usize.checked_mul elems i) + match o with + | none => fail panic + | some used => ok (elems, used) + +/-- [zerocopy::layout::{zerocopy::layout::SizeInfo}::try_to_nonzero_elem_size]: + Source: 'src/layout/mod.rs', lines 836:4-864:5 -/ +def layout.SizeInfoUsize.try_to_nonzero_elem_size + (self : layout.SizeInfo Std.Usize) : + Result (Option (layout.SizeInfo (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner))) + := do + match self with + | layout.SizeInfo.Sized size => ok (some (layout.SizeInfo.Sized size)) + | layout.SizeInfo.SliceDst tsl => + let o ← + core.num.nonzero.NonZero.new + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + tsl.elem_size + match o with + | none => ok none + | some elem_size => + ok (some (layout.SizeInfo.SliceDst + { + offset := tsl.offset, + elem_size, + size_base := tsl.size_base, + size_rounding_align_and_phase := tsl.size_rounding_align_and_phase + })) + +/-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::align]: + Source: 'src/layout/mod.rs', lines 185:4-194:5 -/ +def layout.RoundingAlignAndPhase.align + (self : layout.RoundingAlignAndPhase) : + Result (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) + := do + let (nz, _) ← layout.RoundingAlignAndPhase.components self + ok nz + +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::validate_cast_and_convert_metadata]: + Source: 'src/layout/mod.rs', lines 1839:4-1986:5 -/ +def layout.DstLayout.validate_cast_and_convert_metadata + (self : layout.DstLayout) (addr : Std.Usize) (bytes_len : Std.Usize) + (cast_type : layout.CastType) : + Result (core.result.Result (Std.Usize × Std.Usize) layout.MetadataCastError) + := do + let o ← layout.SizeInfoUsize.try_to_nonzero_elem_size self.size_info + match o with + | none => fail panic + | some size_info => + let o1 ← lift (Usize.checked_add addr bytes_len) + let e := core.option.Option.is_some o1 + massert e + let offset ← + match cast_type with + | layout.CastType.Prefix => ok 0#usize + | layout.CastType.Suffix => ok bytes_len + let i ← addr + offset + let i1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + self.align + let i2 ← i % i1 + if i2 != 0#usize + then ok (core.result.Result.Err layout.MetadataCastError.Alignment) + else + match size_info with + | layout.SizeInfo.Sized size => + massert ((size > bytes_len) || (size <= bytes_len)) + if size > bytes_len + then ok (core.result.Result.Err layout.MetadataCastError.Size) + else + match cast_type with + | layout.CastType.Prefix => + ok (core.result.Result.Ok (0#usize, size)) + | layout.CastType.Suffix => + let split_at ← bytes_len - size + ok (core.result.Result.Ok (0#usize, split_at)) + | layout.SizeInfo.SliceDst trailing => + let o2 ← + layout.TrailingSliceLayout.max_trailing_bytes trailing bytes_len + match o2 with + | none => ok (core.result.Result.Err layout.MetadataCastError.Size) + | some bytes => + let (elems, _) ← + layout.max_elems_for_bytes bytes trailing.elem_size + let size_align ← + layout.RoundingAlignAndPhase.align + trailing.size_rounding_align_and_phase + let i3 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + trailing.elem_size + let unused_bytes ← bytes % i3 + let unused_aligned_bytes ← + util.round_down_to_next_multiple_of_alignment unused_bytes + size_align + let i4 ← bytes_len - trailing.size_base + let max_rounded_bytes ← + util.round_down_to_next_multiple_of_alignment i4 size_align + let i5 ← max_rounded_bytes - unused_aligned_bytes + let self_bytes ← trailing.size_base + i5 + massert (self_bytes <= bytes_len) + match cast_type with + | layout.CastType.Prefix => + ok (core.result.Result.Ok (elems, self_bytes)) + | layout.CastType.Suffix => + let split_at ← bytes_len - self_bytes + ok (core.result.Result.Ok (elems, split_at)) + +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::metadata_for_exact_size]: + Source: 'src/layout/mod.rs', lines 1701:4-1724:5 -/ +def layout.DstLayout.metadata_for_exact_size + (self : layout.DstLayout) (size : Std.Usize) : + Result (Option Std.Usize) + := do + match self.size_info with + | layout.SizeInfo.Sized _ => ok none + | layout.SizeInfo.SliceDst tsl => + match tsl.elem_size.val with + | 0 => ok none + | _ => + let r ← + layout.DstLayout.validate_cast_and_convert_metadata self 0#usize size + layout.CastType.Prefix + match r with + | core.result.Result.Ok p => + let (elems, object_size) := p + if object_size = size + then ok (some elems) + else ok none + | core.result.Result.Err _ => ok none + +/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::size_offset]: + Source: 'src/layout/mod.rs', lines 274:4-287:5 -/ +def layout.TrailingSliceLayout.size_offset + {E : Type} (self : layout.TrailingSliceLayout E) : Result Std.Usize := do + let (size_align, size_phase) ← + layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase + let aligned_base ← + util.round_down_to_next_multiple_of_alignment self.size_base size_align + ok (aligned_base ||| size_phase) + +/-- [zerocopy::layout::cast_from::{zerocopy::layout::cast_from::CastPlan}::try_compute]: + Source: 'src/layout/cast_from.rs', lines 122:4-217:5 -/ +def layout.cast_from.CastPlan.try_compute + (src_layout : layout.DstLayout) (dst_layout : layout.DstLayout) : + Result (Option layout.cast_from.CastPlan) + := do + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + src_layout.align + let i1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + dst_layout.align + if i < i1 + then ok none + else + match src_layout.size_info with + | layout.SizeInfo.Sized src_size => + match dst_layout.size_info with + | layout.SizeInfo.Sized dst_size => + if src_size != dst_size + then ok none + else ok (some layout.cast_from.CastPlan.SizedToSized) + | layout.SizeInfo.SliceDst _ => + let o ← layout.DstLayout.metadata_for_exact_size dst_layout src_size + match o with + | none => ok none + | some «meta» => + ok (some (layout.cast_from.CastPlan.SizedToUnsized «meta»)) + | layout.SizeInfo.SliceDst src => + match dst_layout.size_info with + | layout.SizeInfo.Sized _ => ok none + | layout.SizeInfo.SliceDst dst => + let o ← + core.num.nonzero.NonZero.new + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + dst.elem_size + match o with + | none => ok none + | some e => + if src.elem_size < dst.elem_size + then ok none + else + let (elem_multiple, described_src_elem_size) ← + layout.max_elems_for_bytes src.elem_size e + if described_src_elem_size != src.elem_size + then ok none + else + let i2 ← layout.TrailingSliceLayout.size_offset src + let i3 ← layout.TrailingSliceLayout.size_offset dst + let o1 ← lift (Usize.checked_sub i2 i3) + let exact_offset_delta_elems ← + match o1 with + | none => ok none + | some delta => + do + let (elems, described_delta) ← + layout.max_elems_for_bytes delta e + if described_delta = delta + then ok (some elems) + else ok none + match exact_offset_delta_elems with + | none => + let o2 ← + layout.TrailingSliceLayoutUsize.size_for_elems src 0#usize + match o2 with + | none => ok none + | some size => + let o3 ← + layout.DstLayout.metadata_for_exact_size dst_layout size + match o3 with + | none => ok none + | some elems => + let b ← + layout.cast_from.CastPlan.size_sequences_match src dst + elems + if b + then + ok (some (layout.cast_from.CastPlan.UnsizedToUnsized + elems elem_multiple)) + else ok none + | some elems => + let b ← + layout.cast_from.CastPlan.size_sequences_match src dst elems + if b + then + ok (some (layout.cast_from.CastPlan.UnsizedToUnsized elems + elem_multiple)) + else + let o2 ← + layout.TrailingSliceLayoutUsize.size_for_elems src 0#usize + match o2 with + | none => ok none + | some size => + let o3 ← + layout.DstLayout.metadata_for_exact_size dst_layout size + match o3 with + | none => ok none + | some elems1 => + let b1 ← + layout.cast_from.CastPlan.size_sequences_match src dst + elems1 + if b1 + then + ok (some (layout.cast_from.CastPlan.UnsizedToUnsized + elems1 elem_multiple)) + else ok none + +/-- [zerocopy::layout::add_scaled_metadata]: + Source: 'src/layout/mod.rs', lines 2008:0-2082:1 -/ +def layout.add_scaled_metadata + (base : Std.Usize) (metadata : Std.Usize) (multiple : Std.Usize) : Result Std.Usize := do - let align1 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align - let b ← core.num.Usize.is_power_of_two align1 - massert b - let i ← align1 - 1#usize - let mask ← lift (~~~ i) - ok (n &&& mask) + let scaled ← core.num.Usize.unchecked_mul metadata multiple + core.num.Usize.unchecked_add base scaled -/-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::components]: - Source: 'src/layout/mod.rs', lines 145:4-172:5 -/ -def layout.RoundingAlignAndPhase.components - (self : layout.RoundingAlignAndPhase) : - Result ((core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner) × Std.Usize) +/-- [zerocopy::layout::cast_from::{zerocopy::layout::cast_from::CastPlan}::cast_metadata]: + Source: 'src/layout/cast_from.rs', lines 233:4-243:5 -/ +def layout.cast_from.CastPlan.cast_metadata + (self : layout.cast_from.CastPlan) (src_meta : Std.Usize) : + Result Std.Usize := do - let i ← layout.POINTER_WIDTH_BITS - let i1 ← i - 1#usize - let i2 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner self._0 - let i3 ← lift (core.num.Usize.leading_zeros i2) - let i4 ← lift (UScalar.cast .Usize i3) - let shift ← i1 - i4 - let align ← 1#usize <<< shift - let o ← - core.num.nonzero.NonZero.new - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align - match o with - | none => fail panic - | some align1 => - let i5 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align1 - let phase ← lift (i2 ^^^ i5) - ok (align1, phase) + match self with + | layout.cast_from.CastPlan.UnsizedToUnsized offset_delta_elems elem_multiple + => + layout.add_scaled_metadata offset_delta_elems src_meta elem_multiple + | layout.cast_from.CastPlan.SizedToUnsized dst_meta => ok dst_meta + | layout.cast_from.CastPlan.SizedToSized => ok 0#usize -/-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::new]: - Source: 'src/layout/mod.rs', lines 112:4-131:5 -/ -def layout.RoundingAlignAndPhase.new - (align : core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) : - Result layout.RoundingAlignAndPhase +/-- [zerocopy::layout::composition_checks::matches_reference]: + Source: 'src/layout/composition_checks.rs', lines 57:0-75:1 -/ +def layout.composition_checks.matches_reference + (runtime_layout : layout.DstLayout) + (reference : layout.composition_checks.ReferenceLayout) : + Result Bool := do let i ← core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align - let b ← core.num.Usize.is_power_of_two i - massert b - massert (phase < i) - let encoded ← lift (i ||| phase) - let o ← - core.num.nonzero.NonZero.new - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner encoded - match o with - | none => fail panic - | some encoded1 => ok { _0 := encoded1 } + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + runtime_layout.align + if i = reference.align + then + if runtime_layout.statically_shallow_unpadded = reference.unpadded + then + match runtime_layout.size_info with + | layout.SizeInfo.Sized size => + match reference.size with + | layout.composition_checks.ReferenceSize.Fixed expected => + ok (size = expected) + | layout.composition_checks.ReferenceSize.Tail _ => ok false + | layout.SizeInfo.SliceDst actual => + match reference.size with + | layout.composition_checks.ReferenceSize.Fixed _ => ok false + | layout.composition_checks.ReferenceSize.Tail expected => + let b ← core.num.Usize.is_power_of_two expected.round_align + if b + then + if expected.phase < expected.round_align + then + if actual.offset = expected.offset + then + if actual.elem_size = expected.elem_size + then + if actual.size_base = expected.base + then + let o ← + lift (Usize.checked_add expected.round_align + expected.phase) + match o with + | none => ok false + | some encoded => + let i1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + actual.size_rounding_align_and_phase._0 + ok (i1 = encoded) + else ok false + else ok false + else ok false + else ok false + else ok false + else ok false + else ok false -/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::pad_to_align]: - Source: 'src/layout/mod.rs', lines 1512:4-1602:5 - Visibility: public -/ -def layout.DstLayout.pad_to_align - (self : layout.DstLayout) : Result layout.DstLayout := do - match self.size_info with - | layout.SizeInfo.Sized unpadded_size => - let padding ← util.padding_needed_for unpadded_size self.align - let o ← lift (Usize.checked_add unpadded_size padding) +/-- [zerocopy::layout::composition_checks::reference_round_up]: + Source: 'src/layout/composition_checks.rs', lines 78:0-84:1 -/ +def layout.composition_checks.reference_round_up + (bytes : Std.Usize) (align : Std.Usize) : Result (Option Std.Usize) := do + if align = 0#usize + then ok none + else + let i ← bytes % align + let i1 ← align - i + let padding ← i1 % align + ok (Usize.checked_add bytes padding) + +/-- [zerocopy::layout::composition_checks::extension_alignment]: + Source: 'src/layout/composition_checks.rs', lines 87:0-89:1 -/ +def layout.composition_checks.extension_alignment + (align : Std.Usize) : Result Bool := do + let b ← core.num.Usize.is_power_of_two align + if b + then let i ← 1#usize <<< 29#i32 + ok (align <= i) + else ok false + +/-- [zerocopy::layout::composition_checks::reference_extend_at]: + Source: 'src/layout/composition_checks.rs', lines 121:0-156:1 -/ +def layout.composition_checks.reference_extend_at + (preceding : layout.composition_checks.ReferenceLayout) + (field : layout.composition_checks.ReferenceLayout) (field_align : Std.Usize) + : + Result (Option layout.composition_checks.ReferenceLayout) + := do + match preceding.size with + | layout.composition_checks.ReferenceSize.Fixed bytes => + let o ← layout.composition_checks.reference_round_up bytes field_align match o with - | none => fail panic - | some size => - if self.statically_shallow_unpadded - then - ok - { - self - with - size_info := (layout.SizeInfo.Sized size), - statically_shallow_unpadded := (padding = 0#usize) - } - else ok { self with size_info := (layout.SizeInfo.Sized size) } - | layout.SizeInfo.SliceDst trailing => - let (size_align, size_phase) ← - layout.RoundingAlignAndPhase.components - trailing.size_rounding_align_and_phase - let i ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner size_align - let i1 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner - self.align - if i < i1 - then - let base_padding ← - util.padding_needed_for trailing.size_base size_align - let o ← lift (Usize.checked_add trailing.size_base base_padding) - match o with - | none => fail panic - | some base => - let o1 ← lift (Usize.checked_add base size_phase) + | none => ok none + | some offset => + match field.size with + | layout.composition_checks.ReferenceSize.Fixed bytes1 => + let o1 ← lift (Usize.checked_add offset bytes1) match o1 with - | none => fail panic - | some bytes => - let i2 ← i1 - 1#usize - let phase ← lift (bytes &&& i2) - let size_base ← - util.round_down_to_next_multiple_of_alignment bytes self.align - let raap ← layout.RoundingAlignAndPhase.new self.align phase - if self.statically_shallow_unpadded - then - ok - { - self - with - size_info := - (layout.SizeInfo.SliceDst - { - trailing - with - size_base, size_rounding_align_and_phase := raap - }), - statically_shallow_unpadded := (0#usize = 0#usize) - } - else - ok - { - self - with - size_info := - (layout.SizeInfo.SliceDst - { - trailing - with - size_base, size_rounding_align_and_phase := raap - }) - } - else - let padding ← util.padding_needed_for trailing.size_base self.align - let o ← lift (Usize.checked_add trailing.size_base padding) - match o with - | none => fail panic - | some base => - if self.statically_shallow_unpadded + | none => ok none + | some size => + let i ← + if preceding.align > field_align + then ok preceding.align + else ok field_align + ok (some + { + align := i, + size := (layout.composition_checks.ReferenceSize.Fixed size), + unpadded := + ((preceding.unpadded && field.unpadded) && (offset = bytes)) + }) + | layout.composition_checks.ReferenceSize.Tail tail => + let o1 ← lift (Usize.checked_add offset tail.offset) + match o1 with + | none => ok none + | some offset1 => + let o2 ← lift (Usize.checked_add offset tail.base) + match o2 with + | none => ok none + | some base => + let i ← + if preceding.align > field_align + then ok preceding.align + else ok field_align + ok (some + { + align := i, + size := + (layout.composition_checks.ReferenceSize.Tail + { tail with offset := offset1, base }), + unpadded := + ((preceding.unpadded && field.unpadded) && (offset = bytes)) + }) + | layout.composition_checks.ReferenceSize.Tail _ => ok none + +/-- [zerocopy::layout::composition_checks::reference_extend]: + Source: 'src/layout/composition_checks.rs', lines 95:0-117:1 -/ +def layout.composition_checks.reference_extend + (preceding : layout.composition_checks.ReferenceLayout) + (field : layout.composition_checks.ReferenceLayout) + (packed : Option (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner)) : + Result (Option layout.composition_checks.ReferenceLayout) + := do + let b ← layout.composition_checks.extension_alignment preceding.align + if b + then + let b1 ← layout.composition_checks.extension_alignment field.align + if b1 + then + match packed with + | none => + layout.composition_checks.reference_extend_at preceding field + field.align + | some cap => + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner cap + let b2 ← layout.composition_checks.extension_alignment i + if b2 then - ok - { - self - with - size_info := - (layout.SizeInfo.SliceDst - { trailing with size_base := base }), - statically_shallow_unpadded := (0#usize = 0#usize) - } - else - ok - { - self - with - size_info := - (layout.SizeInfo.SliceDst - { trailing with size_base := base }) - } + let field_align ← if field.align < i + then ok field.align + else ok i + layout.composition_checks.reference_extend_at preceding field + field_align + else ok none + else ok none + else ok none -/-- [zerocopy::layout::composition_checks::check_pad]: - Source: 'src/layout/composition_checks.rs', lines 226:0-233:1 -/ -def layout.composition_checks.check_pad - (runtime_layout : layout.DstLayout) +/-- [zerocopy::layout::composition_checks::reference_pad]: + Source: 'src/layout/composition_checks.rs', lines 159:0-194:1 -/ +def layout.composition_checks.reference_pad (reference : layout.composition_checks.ReferenceLayout) : - Result Unit + Result (Option layout.composition_checks.ReferenceLayout) := do - let b ← - layout.composition_checks.matches_reference runtime_layout reference + let b ← core.num.Usize.is_power_of_two reference.align if b then - let o ← layout.composition_checks.reference_pad reference - match o with - | none => ok () - | some expected => - let actual ← layout.DstLayout.pad_to_align runtime_layout - let b1 ← layout.composition_checks.matches_reference actual expected - massert b1 - else ok () + match reference.size with + | layout.composition_checks.ReferenceSize.Fixed bytes => + let o ← + layout.composition_checks.reference_round_up bytes reference.align + match o with + | none => ok none + | some rounded => + ok (some + { + reference + with + size := (layout.composition_checks.ReferenceSize.Fixed rounded), + unpadded := (reference.unpadded && (rounded = bytes)) + }) + | layout.composition_checks.ReferenceSize.Tail tail => + let b1 ← core.num.Usize.is_power_of_two tail.round_align + if b1 + then + if tail.phase >= tail.round_align + then ok none + else + if tail.round_align >= reference.align + then + let o ← + layout.composition_checks.reference_round_up tail.base + reference.align + match o with + | none => ok none + | some base => + ok (some + { + reference + with + size := + (layout.composition_checks.ReferenceSize.Tail + { tail with base }), + unpadded := (reference.unpadded && true) + }) + else + let o ← + layout.composition_checks.reference_round_up tail.base + tail.round_align + match o with + | none => ok none + | some base => + let o1 ← lift (Usize.checked_add base tail.phase) + match o1 with + | none => ok none + | some fixed => + let phase ← fixed % reference.align + let base1 ← fixed - phase + ok (some + { + reference + with + size := + (layout.composition_checks.ReferenceSize.Tail + { + tail + with + base := base1, + round_align := reference.align, + phase + }), + unpadded := (reference.unpadded && true) + }) + else ok none + else ok none -/-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::align]: - Source: 'src/layout/mod.rs', lines 185:4-194:5 -/ -def layout.RoundingAlignAndPhase.align - (self : layout.RoundingAlignAndPhase) : +/-- [zerocopy::util::min]: + Source: 'src/util/mod.rs', lines 306:0-312:1 -/ +def util.min + (a : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) + (b : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) : Result (core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner) := do - let (nz, _) ← layout.RoundingAlignAndPhase.components self - ok nz - -/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::size_offset]: - Source: 'src/layout/mod.rs', lines 274:4-287:5 -/ -def layout.TrailingSliceLayout.size_offset - {E : Type} (self : layout.TrailingSliceLayout E) : Result Std.Usize := do - let (size_align, size_phase) ← - layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase - let aligned_base ← - util.round_down_to_next_multiple_of_alignment self.size_base size_align - ok (aligned_base ||| size_phase) - -/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::max_trailing_bytes]: - Source: 'src/layout/mod.rs', lines 310:4-399:5 -/ -def layout.TrailingSliceLayout.max_trailing_bytes - {E : Type} (self : layout.TrailingSliceLayout E) - (available_bytes : Std.Usize) : - Result (Option Std.Usize) - := do - let (size_align, size_phase) ← - layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase - let rounded_phase ← - if size_phase = 0#usize - then ok 0#usize - else - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner size_align - let o ← lift (Usize.checked_add self.size_base rounded_phase) - match o with - | none => ok none - | some size => - let o1 ← lift (Usize.checked_sub available_bytes size) - match o1 with - | none => ok none - | some bytes => - let aligned_bytes ← - util.round_down_to_next_multiple_of_alignment bytes size_align - let initial_padding ← rounded_phase - size_phase - let trailing_bytes ← lift (aligned_bytes ||| initial_padding) - ok (some trailing_bytes) + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner a + let i1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner b + if i > i1 + then ok b + else ok a -/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::padding_for_elems]: - Source: 'src/layout/mod.rs', lines 424:4-479:5 -/ -def layout.TrailingSliceLayoutUsize.padding_for_elems - (self : layout.TrailingSliceLayout Std.Usize) (elems : Std.Usize) : - Result Std.Usize +/-- [zerocopy::util::max]: + Source: 'src/util/mod.rs', lines 290:0-296:1 -/ +def util.max + (a : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) + (b : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) : + Result (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) := do - let (size_align, size_phase) ← - layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase let i ← core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner size_align - let size_mask ← i - 1#usize - let elem_remainder ← lift (self.elem_size &&& size_mask) - let i1 ← lift (core.num.Usize.wrapping_mul elems elem_remainder) - let trailing_remainder ← lift (i1 &&& size_mask) - let rounding_input ← - lift (core.num.Usize.wrapping_add size_phase trailing_remainder) - let rounding_padding ← util.padding_needed_for rounding_input size_align - let i2 ← lift (core.num.Usize.wrapping_add self.size_base size_phase) - let i3 ← lift (core.num.Usize.wrapping_sub i2 self.offset) - ok (core.num.Usize.wrapping_add i3 rounding_padding) + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner a + let i1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner b + if i < i1 + then ok b + else ok a + +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::CURRENT_MAX_ALIGN] + Source: 'src/layout/mod.rs', lines 951:4-954:6 -/ +@[global_simps, irreducible] +def layout.DstLayout.CURRENT_MAX_ALIGN + : + Result (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) + := do + let i ← 1#usize <<< 29#i32 + let o ← + core.num.nonzero.NonZero.new + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner i + match o with + | none => fail panic + | some max_align => ok max_align -/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::size_for_elems]: - Source: 'src/layout/mod.rs', lines 497:4-561:5 -/ -def layout.TrailingSliceLayoutUsize.size_for_elems - (self : layout.TrailingSliceLayout Std.Usize) (elems : Std.Usize) : - Result (Option Std.Usize) +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::THEORETICAL_MAX_ALIGN] + Source: 'src/layout/mod.rs', lines 937:4-941:10 -/ +@[global_simps, irreducible] +def layout.DstLayout.THEORETICAL_MAX_ALIGN + : + Result (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) := do + let i ← layout.POINTER_WIDTH_BITS + let i1 ← i - 1#usize + let i2 ← 1#usize <<< i1 let o ← - layout.TrailingSliceLayout.max_trailing_bytes self core.num.Usize.MAX + core.num.nonzero.NonZero.new + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner i2 match o with - | none => ok none - | some bytes => - let o1 ← lift (Usize.checked_mul self.elem_size elems) - match o1 with - | none => ok none - | some bytes1 => - if bytes1 > bytes - then ok none - else - let trailing_end ← - lift (core.num.Usize.wrapping_add self.offset bytes1) - let i ← layout.TrailingSliceLayoutUsize.padding_for_elems self elems - let size ← lift (core.num.Usize.wrapping_add trailing_end i) - ok (some size) + | none => fail panic + | some max_align => ok max_align -/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::has_same_size_sequence]: - Source: 'src/layout/mod.rs', lines 585:4-662:5 -/ -def layout.TrailingSliceLayoutUsize.has_same_size_sequence - (self : layout.TrailingSliceLayout Std.Usize) - (other : layout.TrailingSliceLayout Std.Usize) : - Result Bool +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::extend]: + Source: 'src/layout/mod.rs', lines 1330:4-1476:5 + Visibility: public -/ +def layout.DstLayout.extend + (self : layout.DstLayout) (field : layout.DstLayout) + (repr_packed : Option (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner)) : + Result layout.DstLayout := do - if self.elem_size != other.elem_size - then ok false - else - let o ← layout.TrailingSliceLayoutUsize.size_for_elems self 0#usize - let o1 ← layout.TrailingSliceLayoutUsize.size_for_elems other 0#usize + let max_align ← + match repr_packed with + | none => layout.DstLayout.THEORETICAL_MAX_ALIGN + | some max_align1 => ok max_align1 + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner max_align + let b ← core.num.Usize.is_power_of_two i + massert b + let i1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner self.align + let nz ← layout.DstLayout.CURRENT_MAX_ALIGN + let i2 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner nz + massert (i1 <= i2) + let i3 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner field.align + let i4 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner nz + massert (i3 <= i4) + let _ ← + match repr_packed with + | none => ok none + | some repr_packed1 => + do + let i5 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + repr_packed1 + let i6 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner nz + massert (i5 <= i6) + ok repr_packed + let field_align ← util.min field.align max_align + let align ← util.max self.align field_align + match self.size_info with + | layout.SizeInfo.Sized preceding_size => + let padding ← util.padding_needed_for preceding_size field_align + let o ← lift (Usize.checked_add preceding_size padding) match o with - | none => ok false - | some self_size => - match o1 with - | none => ok false - | some other_size => - if self_size = other_size - then - let (self_align, self_phase) ← - layout.RoundingAlignAndPhase.components - self.size_rounding_align_and_phase - let (other_align, other_phase) ← - layout.RoundingAlignAndPhase.components - other.size_rounding_align_and_phase - let self_align1 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner - self_align - let other_align1 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner - other_align - let max_align ← - if self_align1 > other_align1 - then ok self_align1 - else ok other_align1 - let i ← self.elem_size % max_align - if i = 0#usize - then ok true + | none => fail panic + | some offset => + match field.size_info with + | layout.SizeInfo.Sized field_size => + let o1 ← lift (Usize.checked_add offset field_size) + match o1 with + | none => fail panic + | some size => + if self.statically_shallow_unpadded + then + if field.statically_shallow_unpadded + then + ok + { + align, + size_info := (layout.SizeInfo.Sized size), + statically_shallow_unpadded := (padding = 0#usize) + } + else + ok + { + align, + size_info := (layout.SizeInfo.Sized size), + statically_shallow_unpadded := false + } else - if self_align1 != other_align1 - then ok false - else ok (self_phase = other_phase) - else ok false + ok + { + align, + size_info := (layout.SizeInfo.Sized size), + statically_shallow_unpadded := false + } + | layout.SizeInfo.SliceDst tsl => + let o1 ← lift (Usize.checked_add offset tsl.offset) + match o1 with + | none => fail panic + | some offset1 => + let o2 ← lift (Usize.checked_add offset tsl.size_base) + match o2 with + | none => fail panic + | some base => + if self.statically_shallow_unpadded + then + if field.statically_shallow_unpadded + then + ok + { + align, + size_info := + (layout.SizeInfo.SliceDst + { tsl with offset := offset1, size_base := base }), + statically_shallow_unpadded := (padding = 0#usize) + } + else + ok + { + align, + size_info := + (layout.SizeInfo.SliceDst + { tsl with offset := offset1, size_base := base }), + statically_shallow_unpadded := false + } + else + ok + { + align, + size_info := + (layout.SizeInfo.SliceDst + { tsl with offset := offset1, size_base := base }), + statically_shallow_unpadded := false + } + | layout.SizeInfo.SliceDst _ => fail panic -/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::advance]: - Source: 'src/layout/mod.rs', lines 706:4-802:5 -/ -def layout.TrailingSliceLayoutUsize.advance - (self : layout.TrailingSliceLayout Std.Usize) (bytes : Std.Usize) - (elem_size : Std.Usize) : - Result (Option (layout.TrailingSliceLayout Std.Usize)) +/-- [zerocopy::layout::composition_checks::check_extend]: + Source: 'src/layout/composition_checks.rs', lines 203:0-218:1 -/ +def layout.composition_checks.check_extend + (preceding : layout.DstLayout) (field : layout.DstLayout) + (packed : Option (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner)) + (preceding_reference : layout.composition_checks.ReferenceLayout) + (field_reference : layout.composition_checks.ReferenceLayout) : + Result Unit := do - let (size_align, size_phase) ← - layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase - let i ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner size_align - let align_mask ← i - 1#usize - let i1 ← core.num.Usize.MAX - self.size_base - let phase_capacity ← lift (i1 ||| align_mask) - let max_advance ← phase_capacity - size_phase - if bytes > max_advance - then ok none - else - let advanced_phase ← size_phase + bytes - let normalized_phase ← lift (advanced_phase &&& align_mask) - let whole_bytes ← - util.round_down_to_next_multiple_of_alignment advanced_phase size_align - let size_base ← self.size_base + whole_bytes - let raap ← layout.RoundingAlignAndPhase.new size_align normalized_phase - ok (some - { self with elem_size, size_base, size_rounding_align_and_phase := raap }) + let b ← + layout.composition_checks.matches_reference preceding preceding_reference + if b + then + let b1 ← + layout.composition_checks.matches_reference field field_reference + if b1 + then + let o ← + layout.composition_checks.reference_extend preceding_reference + field_reference packed + match o with + | none => ok () + | some expected => + let actual ← layout.DstLayout.extend preceding field packed + let b2 ← layout.composition_checks.matches_reference actual expected + massert b2 + else ok () + else ok () -/-- [zerocopy::layout::{zerocopy::layout::SizeInfo}::try_to_nonzero_elem_size]: - Source: 'src/layout/mod.rs', lines 836:4-864:5 -/ -def layout.SizeInfoUsize.try_to_nonzero_elem_size - (self : layout.SizeInfo Std.Usize) : - Result (Option (layout.SizeInfo (core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner))) - := do - match self with - | layout.SizeInfo.Sized size => ok (some (layout.SizeInfo.Sized size)) - | layout.SizeInfo.SliceDst tsl => - let o ← - core.num.nonzero.NonZero.new - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner - tsl.elem_size +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::pad_to_align]: + Source: 'src/layout/mod.rs', lines 1512:4-1602:5 + Visibility: public -/ +def layout.DstLayout.pad_to_align + (self : layout.DstLayout) : Result layout.DstLayout := do + match self.size_info with + | layout.SizeInfo.Sized unpadded_size => + let padding ← util.padding_needed_for unpadded_size self.align + let o ← lift (Usize.checked_add unpadded_size padding) match o with - | none => ok none - | some elem_size => - ok (some (layout.SizeInfo.SliceDst - { - offset := tsl.offset, - elem_size, - size_base := tsl.size_base, - size_rounding_align_and_phase := tsl.size_rounding_align_and_phase - })) + | none => fail panic + | some size => + if self.statically_shallow_unpadded + then + ok + { + self + with + size_info := (layout.SizeInfo.Sized size), + statically_shallow_unpadded := (padding = 0#usize) + } + else ok { self with size_info := (layout.SizeInfo.Sized size) } + | layout.SizeInfo.SliceDst trailing => + let (size_align, size_phase) ← + layout.RoundingAlignAndPhase.components + trailing.size_rounding_align_and_phase + let i ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner size_align + let i1 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner + self.align + if i < i1 + then + let base_padding ← + util.padding_needed_for trailing.size_base size_align + let o ← lift (Usize.checked_add trailing.size_base base_padding) + match o with + | none => fail panic + | some base => + let o1 ← lift (Usize.checked_add base size_phase) + match o1 with + | none => fail panic + | some bytes => + let i2 ← i1 - 1#usize + let phase ← lift (bytes &&& i2) + let size_base ← + util.round_down_to_next_multiple_of_alignment bytes self.align + let raap ← layout.RoundingAlignAndPhase.new self.align phase + if self.statically_shallow_unpadded + then + ok + { + self + with + size_info := + (layout.SizeInfo.SliceDst + { + trailing + with + size_base, size_rounding_align_and_phase := raap + }), + statically_shallow_unpadded := (0#usize = 0#usize) + } + else + ok + { + self + with + size_info := + (layout.SizeInfo.SliceDst + { + trailing + with + size_base, size_rounding_align_and_phase := raap + }) + } + else + let padding ← util.padding_needed_for trailing.size_base self.align + let o ← lift (Usize.checked_add trailing.size_base padding) + match o with + | none => fail panic + | some base => + if self.statically_shallow_unpadded + then + ok + { + self + with + size_info := + (layout.SizeInfo.SliceDst + { trailing with size_base := base }), + statically_shallow_unpadded := (0#usize = 0#usize) + } + else + ok + { + self + with + size_info := + (layout.SizeInfo.SliceDst + { trailing with size_base := base }) + } -/-- [zerocopy::layout::max_elems_for_bytes]: - Source: 'src/layout/mod.rs', lines 892:0-907:1 -/ -def layout.max_elems_for_bytes - (bytes : Std.Usize) - (elem_size : core.num.nonzero.NonZero Std.Usize - core.num.niche_types.NonZeroUsizeInner) : - Result (Std.Usize × Std.Usize) +/-- [zerocopy::layout::composition_checks::check_pad]: + Source: 'src/layout/composition_checks.rs', lines 226:0-233:1 -/ +def layout.composition_checks.check_pad + (runtime_layout : layout.DstLayout) + (reference : layout.composition_checks.ReferenceLayout) : + Result Unit := do - let i ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner elem_size - let elems ← bytes / i - let o ← lift (Usize.checked_mul elems i) - match o with - | none => fail panic - | some used => ok (elems, used) + let b ← + layout.composition_checks.matches_reference runtime_layout reference + if b + then + let o ← layout.composition_checks.reference_pad reference + match o with + | none => ok () + | some expected => + let actual ← layout.DstLayout.pad_to_align runtime_layout + let b1 ← layout.composition_checks.matches_reference actual expected + massert b1 + else ok () /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::MIN_ALIGN] Source: 'src/layout/mod.rs', lines 927:4-930:6 -/ @@ -1674,100 +1916,6 @@ def layout.DstLayout.requires_dynamic_padding then ok true else ok (¬ (i1 = 0#usize)) -/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::validate_cast_and_convert_metadata]: - Source: 'src/layout/mod.rs', lines 1839:4-1986:5 -/ -def layout.DstLayout.validate_cast_and_convert_metadata - (self : layout.DstLayout) (addr : Std.Usize) (bytes_len : Std.Usize) - (cast_type : layout.CastType) : - Result (core.result.Result (Std.Usize × Std.Usize) layout.MetadataCastError) - := do - let o ← layout.SizeInfoUsize.try_to_nonzero_elem_size self.size_info - match o with - | none => fail panic - | some size_info => - let o1 ← lift (Usize.checked_add addr bytes_len) - let e := core.option.Option.is_some o1 - massert e - let offset ← - match cast_type with - | layout.CastType.Prefix => ok 0#usize - | layout.CastType.Suffix => ok bytes_len - let i ← addr + offset - let i1 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner - self.align - let i2 ← i % i1 - if i2 != 0#usize - then ok (core.result.Result.Err layout.MetadataCastError.Alignment) - else - match size_info with - | layout.SizeInfo.Sized size => - massert ((size > bytes_len) || (size <= bytes_len)) - if size > bytes_len - then ok (core.result.Result.Err layout.MetadataCastError.Size) - else - match cast_type with - | layout.CastType.Prefix => - ok (core.result.Result.Ok (0#usize, size)) - | layout.CastType.Suffix => - let split_at ← bytes_len - size - ok (core.result.Result.Ok (0#usize, split_at)) - | layout.SizeInfo.SliceDst trailing => - let o2 ← - layout.TrailingSliceLayout.max_trailing_bytes trailing bytes_len - match o2 with - | none => ok (core.result.Result.Err layout.MetadataCastError.Size) - | some bytes => - let (elems, _) ← - layout.max_elems_for_bytes bytes trailing.elem_size - let size_align ← - layout.RoundingAlignAndPhase.align - trailing.size_rounding_align_and_phase - let i3 ← - core.num.nonzero.NonZero.get - Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner - trailing.elem_size - let unused_bytes ← bytes % i3 - let unused_aligned_bytes ← - util.round_down_to_next_multiple_of_alignment unused_bytes - size_align - let i4 ← bytes_len - trailing.size_base - let max_rounded_bytes ← - util.round_down_to_next_multiple_of_alignment i4 size_align - let i5 ← max_rounded_bytes - unused_aligned_bytes - let self_bytes ← trailing.size_base + i5 - massert (self_bytes <= bytes_len) - match cast_type with - | layout.CastType.Prefix => - ok (core.result.Result.Ok (elems, self_bytes)) - | layout.CastType.Suffix => - let split_at ← bytes_len - self_bytes - ok (core.result.Result.Ok (elems, split_at)) - -/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::metadata_for_exact_size]: - Source: 'src/layout/mod.rs', lines 1701:4-1724:5 -/ -def layout.DstLayout.metadata_for_exact_size - (self : layout.DstLayout) (size : Std.Usize) : - Result (Option Std.Usize) - := do - match self.size_info with - | layout.SizeInfo.Sized _ => ok none - | layout.SizeInfo.SliceDst tsl => - match tsl.elem_size.val with - | 0 => ok none - | _ => - let r ← - layout.DstLayout.validate_cast_and_convert_metadata self 0#usize size - layout.CastType.Prefix - match r with - | core.result.Result.Ok p => - let (elems, object_size) := p - if object_size = size - then ok (some elems) - else ok none - | core.result.Result.Err _ => ok none - /-- [zerocopy::layout::nested_reference::round_up]: Source: 'src/layout/nested_reference.rs', lines 46:0-56:1 -/ def layout.nested_reference.round_up diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean index 7a0028e10c..09e67e6e18 100644 --- a/verification/aeneas/golden/FunsExternal_Template.lean +++ b/verification/aeneas/golden/FunsExternal_Template.lean @@ -75,3 +75,19 @@ axiom core.num.nonzero.NonZero.get core.num.nonzero.ZeroablePrimitive T Clause0_NonZeroInner) : core.num.nonzero.NonZero T Clause0_NonZeroInner → Result T +/-- [core::num::{usize}::unchecked_add]: + Source: '/rustc/library/core/src/num/uint_macros.rs', lines 1031:8-1031:66 + Name pattern: [core::num::{usize}::unchecked_add] + Visibility: public -/ +@[rust_fun "core::num::{usize}::unchecked_add"] +axiom core.num.Usize.unchecked_add + : Std.Usize → Std.Usize → Result Std.Usize + +/-- [core::num::{usize}::unchecked_mul]: + Source: '/rustc/library/core/src/num/uint_macros.rs', lines 1419:8-1419:66 + Name pattern: [core::num::{usize}::unchecked_mul] + Visibility: public -/ +@[rust_fun "core::num::{usize}::unchecked_mul"] +axiom core.num.Usize.unchecked_mul + : Std.Usize → Std.Usize → Result Std.Usize + diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index a4c2f9fae7..3d04b8065c 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -99,30 +99,13 @@ structure byteorder.U32 (O : Type) where _0 : Array Std.U8 4#usize _1 : core.marker.PhantomData O -/-- [zerocopy::layout::composition_checks::ReferenceTail] - Source: 'src/layout/composition_checks.rs', lines 32:0-38:1 -/ -structure layout.composition_checks.ReferenceTail where - offset : Std.Usize - elem_size : Std.Usize - base : Std.Usize - round_align : Std.Usize - phase : Std.Usize - -/-- [zerocopy::layout::composition_checks::ReferenceSize] - Source: 'src/layout/composition_checks.rs', lines 42:0-45:1 -/ +/-- [zerocopy::layout::cast_from::CastPlan] + Source: 'src/layout/cast_from.rs', lines 29:0-60:1 -/ @[discriminant isize] -inductive layout.composition_checks.ReferenceSize where -| Fixed : Std.Usize → layout.composition_checks.ReferenceSize -| Tail : - layout.composition_checks.ReferenceTail → - layout.composition_checks.ReferenceSize - -/-- [zerocopy::layout::composition_checks::ReferenceLayout] - Source: 'src/layout/composition_checks.rs', lines 48:0-52:1 -/ -structure layout.composition_checks.ReferenceLayout where - align : Std.Usize - size : layout.composition_checks.ReferenceSize - unpadded : Bool +inductive layout.cast_from.CastPlan where +| UnsizedToUnsized : Std.Usize → Std.Usize → layout.cast_from.CastPlan +| SizedToUnsized : Std.Usize → layout.cast_from.CastPlan +| SizedToSized : layout.cast_from.CastPlan /-- [zerocopy::layout::RoundingAlignAndPhase] Source: 'src/layout/mod.rs', lines 93:0-93:54 -/ @@ -138,6 +121,21 @@ structure layout.TrailingSliceLayout (E : Type) where size_base : Std.Usize size_rounding_align_and_phase : layout.RoundingAlignAndPhase +/-- [zerocopy::layout::MetadataCastError] + Source: 'src/layout/mod.rs', lines 920:0-923:1 -/ +@[discriminant isize] +inductive layout.MetadataCastError where +| Alignment : layout.MetadataCastError +| Size : layout.MetadataCastError + +/-- [zerocopy::layout::CastType] + Source: 'src/layout/mod.rs', lines 913:0-916:1 + Visibility: public -/ +@[discriminant isize] +inductive layout.CastType where +| Prefix : layout.CastType +| Suffix : layout.CastType + /-- [zerocopy::layout::SizeInfo] Source: 'src/layout/mod.rs', lines 62:0-65:1 -/ @[discriminant isize] @@ -154,20 +152,30 @@ structure layout.DstLayout where size_info : layout.SizeInfo Std.Usize statically_shallow_unpadded : Bool -/-- [zerocopy::layout::CastType] - Source: 'src/layout/mod.rs', lines 913:0-916:1 - Visibility: public -/ -@[discriminant isize] -inductive layout.CastType where -| Prefix : layout.CastType -| Suffix : layout.CastType +/-- [zerocopy::layout::composition_checks::ReferenceTail] + Source: 'src/layout/composition_checks.rs', lines 32:0-38:1 -/ +structure layout.composition_checks.ReferenceTail where + offset : Std.Usize + elem_size : Std.Usize + base : Std.Usize + round_align : Std.Usize + phase : Std.Usize -/-- [zerocopy::layout::MetadataCastError] - Source: 'src/layout/mod.rs', lines 920:0-923:1 -/ +/-- [zerocopy::layout::composition_checks::ReferenceSize] + Source: 'src/layout/composition_checks.rs', lines 42:0-45:1 -/ @[discriminant isize] -inductive layout.MetadataCastError where -| Alignment : layout.MetadataCastError -| Size : layout.MetadataCastError +inductive layout.composition_checks.ReferenceSize where +| Fixed : Std.Usize → layout.composition_checks.ReferenceSize +| Tail : + layout.composition_checks.ReferenceTail → + layout.composition_checks.ReferenceSize + +/-- [zerocopy::layout::composition_checks::ReferenceLayout] + Source: 'src/layout/composition_checks.rs', lines 48:0-52:1 -/ +structure layout.composition_checks.ReferenceLayout where + align : Std.Usize + size : layout.composition_checks.ReferenceSize + unpadded : Bool /-- [zerocopy::layout::nested_reference::NestedLayer] Source: 'src/layout/nested_reference.rs', lines 27:0-31:1 -/ diff --git a/verification/aeneas/lean/CastMath.lean b/verification/aeneas/lean/CastMath.lean new file mode 100644 index 0000000000..cacc659a7c --- /dev/null +++ b/verification/aeneas/lean/CastMath.lean @@ -0,0 +1,44 @@ +/- 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 LayoutMath +@[expose] public section + +/-! +Pure arithmetic for composing a selected cast plan with its metadata map. +All metadata and sizes are unbounded natural numbers. These lemmas concern +complete numerical sizes, not physical slice offsets, pointer validity, or +provenance. Bounds on the two metadata operations are derived separately +from equality of complete sizes. +-/ +namespace Zerocopy.LayoutMath + +/- Byte advancement implements the affine element-count map exactly when the +source stride is a multiple of the destination stride. Positivity is needed +only for the later bounds, not for this identity. +-/ +theorem advance_affine_size (src dst : Formula) (offset multiple n : Nat) + (he : src.elem = multiple * dst.elem) : + (dst.advance (offset * dst.elem) src.elem).size n = + dst.size (offset + n * multiple) := by + rw [advance_size] + simp only [Formula.size, Formula.bytes, he, Nat.add_mul, Nat.mul_assoc, + Nat.add_assoc] + +/- A size-sequence certificate for the shifted formula can therefore be +applied to every source metadata value, including values whose sizes exceed +any particular machine bound. +-/ +theorem affine_size_of_advance (src dst : Formula) (offset multiple : Nat) + (he : src.elem = multiple * dst.elem) + (hseq : ∀ n, src.size n = (dst.advance (offset * dst.elem) src.elem).size n) + (n : Nat) : src.size n = dst.size (offset + n * multiple) := by + rw [hseq n, advance_affine_size src dst offset multiple n he] + +end Zerocopy.LayoutMath diff --git a/verification/aeneas/lean/LayoutModel.lean b/verification/aeneas/lean/LayoutModel.lean index 87586631af..bfb79671e5 100644 --- a/verification/aeneas/lean/LayoutModel.lean +++ b/verification/aeneas/lean/LayoutModel.lean @@ -108,6 +108,40 @@ def metadataSpec (self : layout.DstLayout) (size : Nat) (r : Option Usize) : Pro | some elems => (trailingFormula tail).size elems.val = size ∧ (∀ n : Nat, (trailingFormula tail).size n ≤ size ↔ n ≤ elems.val) +/- A selected plan maps element counts, not byte offsets. Sized variants ignore +the source count; the affine variant retains both of its numerical parameters. +-/ +def castPlanMetadata (plan : layout.cast_from.CastPlan) (count : Nat) : Nat := + match plan with + | .UnsizedToUnsized base multiple => base.val + count * multiple.val + | .SizedToUnsized metadata => metadata.val + | .SizedToSized => 0 + +def castMetadataFits (plan : layout.cast_from.CastPlan) (count : Nat) : Prop := + castPlanMetadata plan count ≤ Usize.max + +/- Acceptance certifies alignment and a size-preserving map for every count. +Rejection deliberately makes no completeness claim: the selector recognizes +sufficient conditions and may reject equivalent layouts. Variant compatibility, +positive destination stride and the exact stride ratio are retained explicitly, +so subsequent proofs can derive arithmetic bounds without assuming them. +-/ +def castPlanSpec (src dst : layout.DstLayout) + (result : Option layout.cast_from.CastPlan) : Prop := + match result with + | none => True + | some plan => + dst.align.val.val ≤ src.align.val.val ∧ + (match src.size_info, dst.size_info, plan with + | .Sized srcSize, .Sized dstSize, .SizedToSized => srcSize = dstSize + | .Sized srcSize, .SliceDst dstTail, .SizedToUnsized metadata => + 0 < dstTail.elem_size.val ∧ (trailingFormula dstTail).size metadata.val = srcSize.val + | .SliceDst srcTail, .SliceDst dstTail, .UnsizedToUnsized base multiple => + 0 < dstTail.elem_size.val ∧ srcTail.elem_size.val = multiple.val * dstTail.elem_size.val ∧ + ∀ count : Nat, (trailingFormula srcTail).size count = + (trailingFormula dstTail).size (base.val + count * multiple.val) + | _, _, _ => False) + /- Project the raw record to the fragment vocabulary used by layout operations. This preserves alignment, payload, physical offset, stride, and unpadded flag. diff --git a/verification/aeneas/lean/Obligations/CastPlan.lean b/verification/aeneas/lean/Obligations/CastPlan.lean new file mode 100644 index 0000000000..e3a23a08e5 --- /dev/null +++ b/verification/aeneas/lean/Obligations/CastPlan.lean @@ -0,0 +1,78 @@ +/- 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 + +/-! +Independent expectations for selected cast operations. Each contract describes +an arbitrary execution outcome; its unsuffixed alias supplies the actual call. +The numerical and layout domains are stated over the raw words and records. +-/ +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Obligations +open Zerocopy.Proofs + +def cast_size_sequences_spec_contract (src dst : layout.TrailingSliceLayout Usize) + (dst_base : Usize) (run : Result Bool) : Prop := + 0 < src.size_rounding_align_and_phase._0.val.val → + 0 < dst.size_rounding_align_and_phase._0.val.val → + 0 < dst.elem_size.val → src.elem_size.val % dst.elem_size.val = 0 → + run ⦃ same => same = true → ∀ count : Nat, + (trailingFormula src).size count = + (trailingFormula dst).size + (dst_base.val + count * (src.elem_size.val / dst.elem_size.val)) ⦄ + +def cast_size_sequences_spec : Prop := + ∀ src dst dst_base, cast_size_sequences_spec_contract src dst dst_base + (layout.cast_from.CastPlan.size_sequences_match src dst dst_base) + +def cast_plan_spec_contract (src dst : layout.DstLayout) + (run : Result (Option layout.cast_from.CastPlan)) : Prop := + 0 < src.align.val.val → 0 < dst.align.val.val → + canonicalLayout src → canonicalLayout dst → + run ⦃ result => match result with + | none => True + | some plan => + dst.align.val.val ≤ src.align.val.val ∧ + (match src.size_info, dst.size_info, plan with + | .Sized srcSize, .Sized dstSize, .SizedToSized => srcSize = dstSize + | .Sized srcSize, .SliceDst dstTail, .SizedToUnsized metadata => + 0 < dstTail.elem_size.val ∧ + (trailingFormula dstTail).size metadata.val = srcSize.val + | .SliceDst srcTail, .SliceDst dstTail, .UnsizedToUnsized base multiple => + 0 < dstTail.elem_size.val ∧ + srcTail.elem_size.val = multiple.val * dstTail.elem_size.val ∧ + ∀ count : Nat, (trailingFormula srcTail).size count = + (trailingFormula dstTail).size (base.val + count * multiple.val) + | _, _, _ => False) ⦄ + +def cast_plan_spec : Prop := + ∀ src dst, cast_plan_spec_contract src dst + (layout.cast_from.CastPlan.try_compute src dst) + +def cast_metadata_spec_contract (self : layout.cast_from.CastPlan) (src_meta : Usize) + (run : Result Usize) : Prop := + castPlanMetadata self src_meta.val ≤ Usize.max → + run ⦃ metadata => metadata.val = castPlanMetadata self src_meta.val ⦄ + +def cast_metadata_spec : Prop := + ∀ self src_meta, cast_metadata_spec_contract self src_meta + (layout.cast_from.CastPlan.cast_metadata self src_meta) + +def add_scaled_metadata_spec_contract (base metadata multiple : Usize) + (run : Result Usize) : Prop := + base.val + metadata.val * multiple.val ≤ Usize.max → + run ⦃ result => result.val = base.val + metadata.val * multiple.val ⦄ + +def add_scaled_metadata_spec : Prop := + ∀ base metadata multiple, add_scaled_metadata_spec_contract base metadata multiple + (layout.add_scaled_metadata base metadata multiple) + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs/CastArithmetic.lean b/verification/aeneas/lean/Proofs/CastArithmetic.lean new file mode 100644 index 0000000000..e43738758b --- /dev/null +++ b/verification/aeneas/lean/Proofs/CastArithmetic.lean @@ -0,0 +1,65 @@ +/- 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 +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw + +/- The complete affine bound implies representability of both intermediate +operations. On that domain the concrete unchecked-operation models use the +backend's checked arithmetic and return exactly the natural-number result. +-/ +theorem add_scaled_metadata_spec (base metadata multiple : Usize) + (fits : base.val + metadata.val * multiple.val ≤ Usize.max) : + layout.add_scaled_metadata base metadata multiple + ⦃ result => result.val = base.val + metadata.val * multiple.val ⦄ := by + unfold layout.add_scaled_metadata core.num.Usize.unchecked_mul + core.num.Usize.unchecked_add + step with Usize.mul_spec (x := metadata) (y := multiple) (by omega) as ⟨scaled, hscaled⟩ + step with Usize.add_spec (x := base) (y := scaled) + (by rw [hscaled]; exact fits) as ⟨result, hresult⟩ + simpa only [WP.spec_ok, hscaled] using hresult + +/- Every plan variant follows its numerical map. Only the affine variant +needs an arithmetic bound; the other variants return their literal metadata. +-/ +theorem cast_metadata_spec (self : layout.cast_from.CastPlan) (src_meta : Usize) + (fits : castMetadataFits self src_meta.val) : + layout.cast_from.CastPlan.cast_metadata self src_meta + ⦃ metadata => metadata.val = castPlanMetadata self src_meta.val ⦄ := by + cases self with + | UnsizedToUnsized base multiple => + exact add_scaled_metadata_spec base src_meta multiple fits + | SizedToUnsized metadata => + simp [layout.cast_from.CastPlan.cast_metadata, castPlanMetadata] + | SizedToSized => + simp [layout.cast_from.CastPlan.cast_metadata, castPlanMetadata] + +end Zerocopy.Proofs.Raw + +namespace Zerocopy.Proofs +open AeneasSpecs + +theorem add_scaled_metadata_spec : Zerocopy.Specs.add_scaled_metadata_spec := by + unfold Zerocopy.Specs.add_scaled_metadata_spec + representation_simps + intro base metadata multiple fits + exact Raw.add_scaled_metadata_spec base metadata multiple fits +register_spec_step add_scaled_metadata_spec + +theorem cast_metadata_spec : Zerocopy.Specs.cast_metadata_spec := by + unfold Zerocopy.Specs.cast_metadata_spec + representation_simps + intro self src_meta _validity fits + exact Raw.cast_metadata_spec self src_meta fits +register_spec_step cast_metadata_spec + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Proofs/CastSelection.lean b/verification/aeneas/lean/Proofs/CastSelection.lean new file mode 100644 index 0000000000..ba5429ba83 --- /dev/null +++ b/verification/aeneas/lean/Proofs/CastSelection.lean @@ -0,0 +1,221 @@ +/- 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.CastSequence +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw +set_option linter.unusedVariables false + +/- Both candidate-selection paths finish with the same complete-sequence +check. Keep this final arithmetic obligation independent of candidate choice. +-/ +theorem cast_plan_accept + (src_layout dst_layout : layout.DstLayout) + (src dst : layout.TrailingSliceLayout Usize) (base multiple : Usize) + (hs : src_layout.size_info = .SliceDst src) + (hd : dst_layout.size_info = .SliceDst dst) + (ha : dst_layout.align.val.val ≤ src_layout.align.val.val) + (hp : 0 < dst.elem_size.val) + (hm : multiple.val = src.elem_size.val / dst.elem_size.val) + (hr : src.elem_size.val = multiple.val * dst.elem_size.val) + (same : ∀ n : Nat, (trailingFormula src).size n = + (trailingFormula dst).size + (base.val + n * (src.elem_size.val / dst.elem_size.val))) : + castPlanSpec src_layout dst_layout (some (.UnsizedToUnsized base multiple)) := by + simp only [castPlanSpec, hs, hd] + exact ⟨ha, hp, hr, by simpa only [hm] using same⟩ + +/- The fallback chooses exact metadata for the zero-count source size, then +checks the entire sequence. A rejected candidate has no completeness promise. +-/ +theorem cast_plan_fallback_spec + (src_layout dst_layout : layout.DstLayout) + (src dst : layout.TrailingSliceLayout Usize) (multiple : Usize) + (hs : src_layout.size_info = .SliceDst src) + (hd : dst_layout.size_info = .SliceDst dst) + (ha : dst_layout.align.val.val ≤ src_layout.align.val.val) + (hda : 0 < dst_layout.align.val.val) + (hsrc : 0 < src.size_rounding_align_and_phase._0.val.val) + (hdst : 0 < dst.size_rounding_align_and_phase._0.val.val) + (hp : 0 < dst.elem_size.val) + (hm : multiple.val = src.elem_size.val / dst.elem_size.val) + (hr : src.elem_size.val = multiple.val * dst.elem_size.val) + (hdiv : src.elem_size.val % dst.elem_size.val = 0) : + (do + let zeroSize ← layout.TrailingSliceLayoutUsize.size_for_elems src 0#usize + match zeroSize with + | none => Result.ok none + | some size => + let metadata ← layout.DstLayout.metadata_for_exact_size dst_layout size + match metadata with + | none => Result.ok none + | some elems => + let same ← layout.cast_from.CastPlan.size_sequences_match src dst elems + if same then + Result.ok (some (layout.cast_from.CastPlan.UnsizedToUnsized elems multiple)) + else Result.ok none) + ⦃ plan => castPlanSpec src_layout dst_layout plan ⦄ := by + step with size_for_elems_spec src 0#usize hsrc as ⟨zeroSize, _⟩ + cases zeroSize with + | none => simp only [WP.spec_ok, castPlanSpec] + | some size => + step with metadata_exact_spec dst_layout size hda + (by simp only [hd]; exact fun _ => hdst) as ⟨metadata, _⟩ + cases metadata with + | none => simp only [WP.spec_ok, castPlanSpec] + | some elems => + step with cast_size_sequences_spec src dst elems hsrc hdst hp hdiv as ⟨same, hsame⟩ + split + · rename_i htrue + apply WP.spec.ret + exact cast_plan_accept src_layout dst_layout src dst elems multiple + hs hd ha hp hm hr (hsame htrue) + · simp only [WP.spec_ok, castPlanSpec] + +/- Accepted plans preserve complete size for all natural metadata values. +The only raw admission conditions are positive alignments and canonical +rounding encodings; all stride requirements follow from executed guards. +-/ +theorem cast_plan_spec + (src_layout dst_layout : layout.DstLayout) + (hsa : 0 < src_layout.align.val.val) + (hda : 0 < dst_layout.align.val.val) + (hsc : canonicalLayout src_layout) + (hdc : canonicalLayout dst_layout) : + layout.cast_from.CastPlan.try_compute src_layout dst_layout + ⦃ plan => castPlanSpec src_layout dst_layout plan ⦄ := by + unfold layout.cast_from.CastPlan.try_compute + simp only [core.num.nonzero.NonZero.get, bind_ok] + split + · simp only [WP.spec_ok, castPlanSpec] + · rename_i halign + have ha : dst_layout.align.val.val ≤ src_layout.align.val.val := by + simpa only [UScalar.lt_equiv, Nat.not_lt] using halign + cases hs : src_layout.size_info with + | Sized srcSize => + simp only [] + cases hd : dst_layout.size_info with + | Sized dstSize => + simp only [] + split + · simp only [WP.spec_ok, castPlanSpec] + · rename_i heq + apply WP.spec.ret + simp only [castPlanSpec, hs, hd] + exact ⟨ha, (UScalar.eq_equiv _ _).mpr (by simpa using heq)⟩ + | SliceDst dst => + simp only [] + have hdst : 0 < dst.size_rounding_align_and_phase._0.val.val := by + simpa only [canonicalLayout, hd] using hdc + step with metadata_exact_spec dst_layout srcSize hda + (by simp only [hd]; exact fun _ => hdst) as ⟨metadata, hmeta⟩ + cases metadata with + | none => simp only [WP.spec_ok, castPlanSpec] + | some elems => + simp only [metadataSpec, hd] at hmeta + split at hmeta + · contradiction + · rename_i hn + apply WP.spec.ret + simp only [castPlanSpec, hs, hd] + exact ⟨ha, by omega, hmeta.1⟩ + | SliceDst src => + simp only [] + cases hd : dst_layout.size_info with + | Sized _ => simp only [hd, WP.spec_ok, castPlanSpec] + | SliceDst dst => + simp only [] + have hsrc : 0 < src.size_rounding_align_and_phase._0.val.val := by + simpa only [canonicalLayout, hs] using hsc + have hdst : 0 < dst.size_rounding_align_and_phase._0.val.val := by + simpa only [canonicalLayout, hd] using hdc + by_cases hz : dst.elem_size = 0#usize + · simp only [core.num.nonzero.NonZero.new, cast_eq, hz, + ↓reduceDIte, ↓reduceIte, bind_ok, WP.spec_ok, castPlanSpec] + · simp only [core.num.nonzero.NonZero.new, cast_eq, hz, + ↓reduceDIte, ↓reduceIte, bind_ok] + have hp : 0 < dst.elem_size.val := by + have hn : dst.elem_size.val ≠ 0 := by + intro he + apply hz + exact (UScalar.eq_equiv _ _).mpr he + omega + split + · simp only [WP.spec_ok, castPlanSpec] + · step with max_elems_for_bytes_spec src.elem_size ⟨dst.elem_size⟩ hp as + ⟨multiple, described, hm, hused, _, _, _⟩ + split + · simp only [WP.spec_ok, castPlanSpec] + · rename_i hexact + have heq : described = src.elem_size := + (UScalar.eq_equiv _ _).mpr (by simpa using hexact) + have hr : src.elem_size.val = multiple.val * dst.elem_size.val := by + simpa only [heq] using hused + have hdiv : src.elem_size.val % dst.elem_size.val = 0 := by + rw [hr, Nat.mul_mod_left] + have fallback := cast_plan_fallback_spec src_layout dst_layout src dst + multiple hs hd ha hda hsrc hdst hp hm hr hdiv + step with size_offset_spec src hsrc as ⟨srcOffset, _⟩ + step with size_offset_spec dst hdst as ⟨dstOffset, _⟩ + step as ⟨delta, _⟩ + cases delta with + | none => + simp only [bind_ok] + exact fallback + | some delta => + step with max_elems_for_bytes_spec delta ⟨dst.elem_size⟩ hp as + ⟨pair, _, _, _, _, _⟩ + rcases pair with ⟨elems, describedDelta⟩ + change (Std.bind + (if describedDelta = delta then Result.ok (some elems) else Result.ok none) _) + ⦃ plan => castPlanSpec src_layout dst_layout plan ⦄ + split + · simp only [bind_ok] + step with cast_size_sequences_spec src dst elems hsrc hdst hp hdiv as + ⟨same, hsame⟩ + split + · rename_i htrue + apply WP.spec.ret + exact cast_plan_accept src_layout dst_layout src dst elems multiple + hs hd ha hp hm hr (hsame htrue) + · exact fallback + · simp only [bind_ok] + exact fallback + +end Zerocopy.Proofs.Raw + +namespace Zerocopy.Proofs +open AeneasSpecs + +theorem cast_plan_spec : Zerocopy.Specs.cast_plan_spec := by + unfold Zerocopy.Specs.cast_plan_spec + representation_simps + intro src dst hsrc hdst + have hcsrc : canonicalLayout src := by + cases hs : src.size_info with + | Sized _ => simp only [canonicalLayout, hs] + | SliceDst _ => simpa only [canonicalLayout, hs] using hsrc.2 + have hcdst : canonicalLayout dst := by + cases hs : dst.size_info with + | Sized _ => simp only [canonicalLayout, hs] + | SliceDst _ => simpa only [canonicalLayout, hs] using hdst.2 + apply WP.spec_mono (Raw.cast_plan_spec src dst hsrc.1 hdst.1 hcsrc hcdst) + intro result facts + refine ⟨?_, facts⟩ + change isValid result + cases result with + | none => simp + | some plan => + cases plan <;> simp [isValid, RustModel.decode, + layout.cast_from.CastPlan.decode, layout.cast_from.CastPlan.decodeFields] +register_spec_step cast_plan_spec + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Proofs/CastSequence.lean b/verification/aeneas/lean/Proofs/CastSequence.lean new file mode 100644 index 0000000000..d54b437828 --- /dev/null +++ b/verification/aeneas/lean/Proofs/CastSequence.lean @@ -0,0 +1,72 @@ +/- 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 CastMath +@[expose] public section + +/-! +The cast selector compares complete size sequences after advancing the +destination's formula. A positive comparison certifies an affine map of +element counts; it says nothing about the physical trailing-field offsets. +Failure to represent the adjustment or a negative comparison promises no +inequality, since this recognizer intentionally need not be complete. +-/ +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw + +theorem cast_size_sequences_spec (src dst : layout.TrailingSliceLayout Usize) + (dst_base : Usize) + (hsrc : 0 < src.size_rounding_align_and_phase._0.val.val) + (hdst : 0 < dst.size_rounding_align_and_phase._0.val.val) + (_positive : 0 < dst.elem_size.val) + (divides : src.elem_size.val % dst.elem_size.val = 0) : + layout.cast_from.CastPlan.size_sequences_match src dst dst_base + ⦃ same => same = true → ∀ count : Nat, + (trailingFormula src).size count = + (trailingFormula dst).size + (dst_base.val + count * (src.elem_size.val / dst.elem_size.val)) ⦄ := by + unfold layout.cast_from.CastPlan.size_sequences_match + cases hm : Usize.checked_mul dst_base dst.elem_size with + | none => simp [lift, WP.spec_ok] + | some bytes => + have bytes_value : bytes.val = dst_base.val * dst.elem_size.val := by + have facts := Usize.checked_mul_bv_spec dst_base dst.elem_size + simp only [hm] at facts + exact facts.2.1 + simp only [lift, bind_ok] + step with advance_spec dst bytes src.elem_size hdst as ⟨advanced, admitted, formula⟩ + cases advanced with + | none => simp [WP.spec_ok] + | some advanced => + have advanced_positive : 0 < advanced.size_rounding_align_and_phase._0.val.val := + admitted advanced (by simp) + step with same_size_sequence_spec src advanced hsrc advanced_positive as ⟨same, equal⟩ + rename_i same_true count + have sequences := equal same_true + rw [formula.1, bytes_value] at sequences + have stride : (trailingFormula src).elem = + (src.elem_size.val / dst.elem_size.val) * (trailingFormula dst).elem := by + exact (Nat.div_mul_cancel (Nat.dvd_of_mod_eq_zero divides)).symm + exact LayoutMath.affine_size_of_advance (trailingFormula src) (trailingFormula dst) + dst_base.val (src.elem_size.val / dst.elem_size.val) stride sequences count + +end Zerocopy.Proofs.Raw + +namespace Zerocopy.Proofs +open AeneasSpecs + +theorem cast_size_sequences_spec : Specs.cast_size_sequences_spec := by + unfold Specs.cast_size_sequences_spec + representation_simps + intro src dst dst_base hsrc hdst positive divides + exact Raw.cast_size_sequences_spec src dst dst_base hsrc hdst positive divides +register_spec_step cast_size_sequences_spec + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RequiredModelContracts/CastPlan.lean b/verification/aeneas/lean/RequiredModelContracts/CastPlan.lean new file mode 100644 index 0000000000..efe83ab4e0 --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/CastPlan.lean @@ -0,0 +1,71 @@ +/- 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.CastPlan +public import RequiredModelContracts +public import RequiredModelContracts.PrimitiveChecks +@[expose] public section + +/-! +These adapters consume the generated contract for the same arbitrary outcome. +They construct every automatic decoded-input witness from the broad raw +premises and retain the independent output observations. They do not prove an +extracted call or use a canonical operation theorem as a substitute premise. +-/ +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +theorem cast_plan_admitted (self : layout.cast_from.CastPlan) : + ∃ value, RustModel.decode self = some value := by + cases self <;> exact ⟨_, rfl⟩ + +@[contract_simps] theorem required_cast_size_sequences + (src dst : layout.TrailingSliceLayout Usize) (dst_base : Usize) (run : Result Bool) + (provided : Specs.cast_size_sequences_spec_contract src dst dst_base run) : + Obligations.cast_size_sequences_spec_contract src dst dst_base run := by + intro srcPositive dstPositive dstElemPositive divides + obtain ⟨srcValue, srcDecoded⟩ := (trailing_usize_admitted_iff src).mpr srcPositive + obtain ⟨dstValue, dstDecoded⟩ := (trailing_usize_admitted_iff dst).mpr dstPositive + apply WP.spec_mono (provided srcValue srcDecoded dstValue dstDecoded + (unsignedWord dst_base) rfl dstElemPositive divides) + rintro same ⟨_value, _decoded, facts⟩ + exact facts + +@[contract_simps] theorem required_cast_plan (src dst : layout.DstLayout) + (run : Result (Option layout.cast_from.CastPlan)) + (provided : Specs.cast_plan_spec_contract src dst run) : + Obligations.cast_plan_spec_contract src dst run := by + intro srcPositive dstPositive srcCanonical dstCanonical + obtain ⟨srcValue, srcDecoded⟩ := layout_admitted_of_canonical src srcPositive srcCanonical + obtain ⟨dstValue, dstDecoded⟩ := layout_admitted_of_canonical dst dstPositive dstCanonical + apply WP.spec_mono (provided srcValue srcDecoded dstValue dstDecoded) + rintro result ⟨_value, _decoded, facts⟩ + exact facts + +@[contract_simps] theorem required_cast_metadata (self : layout.cast_from.CastPlan) + (src_meta : Usize) (run : Result Usize) + (provided : Specs.cast_metadata_spec_contract self src_meta run) : + Obligations.cast_metadata_spec_contract self src_meta run := by + intro fits + obtain ⟨value, decoded⟩ := cast_plan_admitted self + apply WP.spec_mono (provided value decoded (unsignedWord src_meta) rfl fits) + rintro metadata ⟨_value, _decoded, facts⟩ + exact facts + +@[contract_simps] theorem required_add_scaled_metadata (base metadata multiple : Usize) + (run : Result Usize) + (provided : Specs.add_scaled_metadata_spec_contract base metadata multiple run) : + Obligations.add_scaled_metadata_spec_contract base metadata multiple run := by + intro fits + apply WP.spec_mono (provided (unsignedWord base) rfl (unsignedWord metadata) rfl + (unsignedWord multiple) rfl fits) + rintro result ⟨_value, _decoded, facts⟩ + exact facts + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Zerocopy/FunsExternal.lean b/verification/aeneas/lean/Zerocopy/FunsExternal.lean index 5d1706a7f2..318b01ddfa 100644 --- a/verification/aeneas/lean/Zerocopy/FunsExternal.lean +++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean @@ -19,6 +19,13 @@ def core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone (x : core.num.niche_types.NonZeroUsizeInner) : Result core.num.niche_types.NonZeroUsizeInner := .ok x +-- Rust's unchecked integer operations are defined only when their exact +-- arithmetic fits. Use the backend's checked operations on that domain. A +-- failed model run outside it establishes no Rust behavior: the corresponding +-- Rust operation has undefined behavior, rather than a promised panic. +def core.num.Usize.unchecked_add (left right : Usize) : Result Usize := left + right +def core.num.Usize.unchecked_mul (left right : Usize) : Result Usize := left * right + @[simp] def core.num.nonzero.NonZero.get {T Inner : Type} (_inst : core.num.nonzero.ZeroablePrimitive T Inner) (x : core.num.nonzero.NonZero T Inner) : Result T := .ok x.val diff --git a/zerocopy/src/layout/cast_from.rs b/zerocopy/src/layout/cast_from.rs index eea5a6812c..11f9ea2cd7 100644 --- a/zerocopy/src/layout/cast_from.rs +++ b/zerocopy/src/layout/cast_from.rs @@ -73,6 +73,15 @@ impl CastPlan { /// `false` result also includes equivalent size sequences /// that this test cannot recognize, or an adjustment whose /// normalized components cannot be represented in `usize`. + /// + /// ```aeneas + /// spec cast_size_sequences_spec + /// requires(raw) positive : 0 < dst.elem_size.val + /// requires(raw) divides : src.elem_size.val % dst.elem_size.val = 0 + /// ensures(raw) same => same = true → ∀ count : Nat, + /// (trailingFormula src).size count = + /// (trailingFormula dst).size (dst_base.val + count * (src.elem_size.val / dst.elem_size.val)) + /// ``` const fn size_sequences_match( src: TrailingSliceLayout, dst: TrailingSliceLayout, @@ -83,7 +92,7 @@ impl CastPlan { None => return false, }; let shifted_dst = match dst.advance(base_bytes, src.elem_size) { - Some(layout) => layout, + Some(advanced) => advanced, None => return false, }; src.has_same_size_sequence(shifted_dst) @@ -105,6 +114,11 @@ impl CastPlan { /// Produces `None` for unsupported casts or when this method /// cannot establish a size-preserving metadata map. Rejection /// does not establish that no such map exists. + /// + /// ```aeneas + /// spec cast_plan_spec + /// ensures(raw) plan => castPlanSpec src_layout dst_layout plan + /// ``` const fn try_compute(src_layout: &DstLayout, dst_layout: &DstLayout) -> Option { if src_layout.align.get() < dst_layout.align.get() { return None; @@ -210,6 +224,12 @@ impl CastPlan { /// `offset_delta_elems + src_meta * elem_multiple` may overflow `usize`. /// The other variants impose no condition on `src_meta` and ignore it. #[inline(always)] + /// + /// ```aeneas + /// spec cast_metadata_spec + /// requires(raw) fits : castMetadataFits self src_meta.val + /// ensures(raw) metadata => metadata.val = castPlanMetadata self src_meta.val + /// ``` unsafe fn cast_metadata(self, src_meta: usize) -> usize { match self { CastPlan::UnsizedToUnsized { offset_delta_elems, elem_multiple } => { diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs index d2d0ccf852..31e59e5091 100644 --- a/zerocopy/src/layout/mod.rs +++ b/zerocopy/src/layout/mod.rs @@ -1999,6 +1999,12 @@ impl DstLayout { #[cfg_attr(kani, kani::ensures(|&result| { metadata.checked_mul(multiple).and_then(|scaled| base.checked_add(scaled)) == Some(result) }))] +/// +/// ```aeneas +/// spec add_scaled_metadata_spec +/// requires(raw) fits : base.val + metadata.val * multiple.val ≤ Usize.max +/// ensures(raw) result => result.val = base.val + metadata.val * multiple.val +/// ``` unsafe fn add_scaled_metadata(base: usize, metadata: usize, multiple: usize) -> usize { // The call-site safety argument establishes that both operations are // representable for valid source metadata. This harness verifies the