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