From 58e305df2eadcd6dd5b73e6da3fac8476c818a11 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Fri, 2 Oct 2026 10:54:19 -0400 Subject: [PATCH] Prove normalized layout padding and field extension Prove normalized padding and field placement while preserving complete inner sizes, including packed-field padding. Derive canonical decoding contracts from Raw operation lemmas and retain explicit fit conditions. Express padding and field extension through mathematical layout views. Reuse the retained-provider decoder bridge for the compact specs. Arbitrary-outcome comparisons recover every existing exact alignment, payload, flag and physical field guarantee. Add total Rust harnesses comparing extension and both padding branches with independent remainder/checked arithmetic. Compare every layout field, including physical offset, normalized size encoding, and shallow-padding flags. Avoid proof dependence on the generator-selected name of a shared matcher. Validation: fresh pinned extraction and complete-model golden comparison; independent golden/live Lean builds, required-contract checks, and the transitive axiom audit. gherrit-pr-id: Gzv73p3q2jm6ohnisvlbsd62wdsi6mjku Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/README.md | 6 +- verification/aeneas/golden/Funs.lean | 769 +++++++++++++++--- verification/aeneas/golden/Types.lean | 33 +- .../aeneas/lean/CompositionReference.lean | 500 ++++++++++++ verification/aeneas/lean/Corollaries.lean | 37 + .../aeneas/lean/ModelProjectionLaws.lean | 167 ++++ verification/aeneas/lean/Obligations.lean | 50 ++ .../lean/Obligations/CompositionChecks.lean | 42 + verification/aeneas/lean/Proofs.lean | 525 ++++++++++++ .../aeneas/lean/Proofs/CompositionChecks.lean | 104 +++ .../aeneas/lean/RequiredModelContracts.lean | 48 ++ .../CompositionChecks.lean | 70 ++ zerocopy/src/layout/composition_checks.rs | 233 ++++++ zerocopy/src/layout/mod.rs | 23 + 14 files changed, 2498 insertions(+), 109 deletions(-) create mode 100644 verification/aeneas/lean/CompositionReference.lean create mode 100644 verification/aeneas/lean/Obligations/CompositionChecks.lean create mode 100644 verification/aeneas/lean/Proofs/CompositionChecks.lean create mode 100644 verification/aeneas/lean/RequiredModelContracts/CompositionChecks.lean create mode 100644 zerocopy/src/layout/composition_checks.rs diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 2c78a5ecb0..4b0f72345f 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -127,7 +127,7 @@ zerocopy's unsafe pointer operations are sound. ## Scope and proofs -Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs), [nested reference](../../zerocopy/src/layout/nested_reference.rs), [primitive assertions](../../zerocopy/src/layout/primitive_checks.rs), [tail assertions](../../zerocopy/src/layout/tail_checks.rs). +Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs), [nested reference](../../zerocopy/src/layout/nested_reference.rs), [primitive assertions](../../zerocopy/src/layout/primitive_checks.rs), [tail assertions](../../zerocopy/src/layout/tail_checks.rs), [composition assertions](../../zerocopy/src/layout/composition_checks.rs). Extraction starts from the function and nominal-type owners of every present `aeneas` fence in `zerocopy/src`, including their dependencies. Every present @@ -144,6 +144,7 @@ added without extending the specification set. | `SizeInfo::try_to_nonzero_elem_size`, `max_elems_for_bytes` | Exact zero handling, preserved representation fields, and greatest fitting element count. | | `DstLayout::requires_static_padding` | Exact negation of the recorded shallow-unpadded flag. | | Trailing size, padding, and capacity | Exact size-offset and capacity formulas, checked-size overflow, and wrapping padding; successful sizes and physical padding refine the independent recursive semantics. | +| `DstLayout::{extend,pad_to_align}` | Exact field placement, alignment, padding flags, and normalized size formulas; outer padding preserves each field's complete inner size. | Every registered function uses total `spec`: accepted raw representations, supplied mathematical ghosts, and explicit requirements imply successful @@ -175,6 +176,9 @@ See [SEMANTICS.md](SEMANTICS.md) for the Rust correspondence premise. The checked trailing-size and padding contracts connect machine arithmetic to the independent recursive semantics. +Extension and normalized padding preserve complete inner sizes, including +padding inside packed fields. + Plain arithmetic clauses use mathematical word values carrying machine bounds and NonZero positivity. Their Nat/Int arithmetic does not wrap; explicit raw clauses preserve the extracted representation vocabulary while retaining diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index cc921925ec..adea680a89 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -642,36 +642,524 @@ 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 + := 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 + +/-- [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 => 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 + +/-- [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 305:0-311: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 289:0-295: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 169:0-229: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 + 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::{zerocopy::layout::DstLayout}::CURRENT_MAX_ALIGN] + Source: 'src/layout/mod.rs', lines 935:4-938: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::POINTER_WIDTH_BITS] - Source: 'src/layout/mod.rs', lines 26:0-26:62 -/ + Source: 'src/layout/mod.rs', lines 29:0-29: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}::new]: - Source: 'src/layout/mod.rs', lines 106:4-125: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::{zerocopy::layout::DstLayout}::THEORETICAL_MAX_ALIGN] + Source: 'src/layout/mod.rs', lines 921:4-925: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 ← - 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 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 encoded + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner i2 match o with | none => fail panic - | some encoded1 => ok { _0 := encoded1 } + | some max_align => ok max_align + +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::extend]: + Source: 'src/layout/mod.rs', lines 1314:4-1460: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 + 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 => 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 + 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::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 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::util::round_down_to_next_multiple_of_alignment]: + Source: 'src/util/mod.rs', lines 261:0-279: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::{zerocopy::layout::RoundingAlignAndPhase}::components]: - Source: 'src/layout/mod.rs', lines 139:4-166:5 -/ + Source: 'src/layout/mod.rs', lines 142:4-169:5 -/ def layout.RoundingAlignAndPhase.components (self : layout.RoundingAlignAndPhase) : Result ((core.num.nonzero.NonZero Std.Usize @@ -698,8 +1186,154 @@ def layout.RoundingAlignAndPhase.components let phase ← lift (i2 ^^^ i5) ok (align1, phase) +/-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::new]: + Source: 'src/layout/mod.rs', lines 109:4-128: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 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::{zerocopy::layout::DstLayout}::pad_to_align]: + Source: 'src/layout/mod.rs', lines 1496:4-1586: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 => 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::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 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::RoundingAlignAndPhase}::align]: - Source: 'src/layout/mod.rs', lines 179:4-188:5 -/ + Source: 'src/layout/mod.rs', lines 182:4-191:5 -/ def layout.RoundingAlignAndPhase.align (self : layout.RoundingAlignAndPhase) : Result (core.num.nonzero.NonZero Std.Usize @@ -708,25 +1342,8 @@ def layout.RoundingAlignAndPhase.align let (nz, _) ← layout.RoundingAlignAndPhase.components self ok nz -/-- [zerocopy::util::round_down_to_next_multiple_of_alignment]: - Source: 'src/util/mod.rs', lines 261:0-279: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::{zerocopy::layout::TrailingSliceLayout}::size_offset]: - Source: 'src/layout/mod.rs', lines 268:4-281:5 -/ + Source: 'src/layout/mod.rs', lines 271:4-284:5 -/ def layout.TrailingSliceLayout.size_offset {E : Type} (self : layout.TrailingSliceLayout E) : Result Std.Usize := do let (size_align, size_phase) ← @@ -736,7 +1353,7 @@ def layout.TrailingSliceLayout.size_offset ok (aligned_base ||| size_phase) /-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::max_trailing_bytes]: - Source: 'src/layout/mod.rs', lines 304:4-393:5 -/ + Source: 'src/layout/mod.rs', lines 307:4-396:5 -/ def layout.TrailingSliceLayout.max_trailing_bytes {E : Type} (self : layout.TrailingSliceLayout E) (available_bytes : Std.Usize) : @@ -764,24 +1381,8 @@ def layout.TrailingSliceLayout.max_trailing_bytes let trailing_bytes ← lift (aligned_bytes ||| initial_padding) ok (some trailing_bytes) -/-- [zerocopy::util::padding_needed_for]: - Source: 'src/util/mod.rs', lines 169:0-229: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 - 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::{zerocopy::layout::TrailingSliceLayout}::padding_for_elems]: - Source: 'src/layout/mod.rs', lines 418:4-473:5 -/ + Source: 'src/layout/mod.rs', lines 421:4-476:5 -/ def layout.TrailingSliceLayoutUsize.padding_for_elems (self : layout.TrailingSliceLayout Std.Usize) (elems : Std.Usize) : Result Std.Usize @@ -803,7 +1404,7 @@ def layout.TrailingSliceLayoutUsize.padding_for_elems ok (core.num.Usize.wrapping_add i3 rounding_padding) /-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout}::size_for_elems]: - Source: 'src/layout/mod.rs', lines 491:4-555:5 -/ + Source: 'src/layout/mod.rs', lines 494:4-558:5 -/ def layout.TrailingSliceLayoutUsize.size_for_elems (self : layout.TrailingSliceLayout Std.Usize) (elems : Std.Usize) : Result (Option Std.Usize) @@ -827,7 +1428,7 @@ def layout.TrailingSliceLayoutUsize.size_for_elems ok (some size) /-- [zerocopy::layout::{zerocopy::layout::SizeInfo}::try_to_nonzero_elem_size]: - Source: 'src/layout/mod.rs', lines 817:4-845:5 -/ + Source: 'src/layout/mod.rs', lines 820:4-848:5 -/ def layout.SizeInfoUsize.try_to_nonzero_elem_size (self : layout.SizeInfo Std.Usize) : Result (Option (layout.SizeInfo (core.num.nonzero.NonZero Std.Usize @@ -852,7 +1453,7 @@ def layout.SizeInfoUsize.try_to_nonzero_elem_size })) /-- [zerocopy::layout::max_elems_for_bytes]: - Source: 'src/layout/mod.rs', lines 873:0-888:1 -/ + Source: 'src/layout/mod.rs', lines 876:0-891:1 -/ def layout.max_elems_for_bytes (bytes : Std.Usize) (elem_size : core.num.nonzero.NonZero Std.Usize @@ -869,7 +1470,7 @@ def layout.max_elems_for_bytes | some used => ok (elems, used) /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::MIN_ALIGN] - Source: 'src/layout/mod.rs', lines 908:4-911:6 -/ + Source: 'src/layout/mod.rs', lines 911:4-914:6 -/ @[global_simps, irreducible] def layout.DstLayout.MIN_ALIGN : @@ -884,13 +1485,13 @@ def layout.DstLayout.MIN_ALIGN | some min_align => ok min_align /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::assume_shallow_unpadded]: - Source: 'src/layout/mod.rs', lines 977:4-986:5 -/ + Source: 'src/layout/mod.rs', lines 980:4-989:5 -/ def layout.DstLayout.assume_shallow_unpadded (self : layout.DstLayout) : Result layout.DstLayout := do ok { self with statically_shallow_unpadded := true } /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::new_zst]: - Source: 'src/layout/mod.rs', lines 1015:4-1035:5 + Source: 'src/layout/mod.rs', lines 1018:4-1038:5 Visibility: public -/ def layout.DstLayout.new_zst (repr_align : Option (core.num.nonzero.NonZero Std.Usize @@ -914,7 +1515,7 @@ def layout.DstLayout.new_zst } /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_type]: - Source: 'src/layout/mod.rs', lines 1059:4-1084:5 + Source: 'src/layout/mod.rs', lines 1062:4-1087:5 Visibility: public -/ def layout.DstLayout.for_type (T : Type) : Result layout.DstLayout := do let i ← core.mem.align_of T @@ -933,7 +1534,7 @@ def layout.DstLayout.for_type (T : Type) : Result layout.DstLayout := do } /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_unpadded_type]: - Source: 'src/layout/mod.rs', lines 1114:4-1128:5 + Source: 'src/layout/mod.rs', lines 1117:4-1131:5 Visibility: public -/ def layout.DstLayout.for_unpadded_type (T : Type) : Result layout.DstLayout := do @@ -941,7 +1542,7 @@ def layout.DstLayout.for_unpadded_type layout.DstLayout.assume_shallow_unpadded dl /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_slice]: - Source: 'src/layout/mod.rs', lines 1153:4-1189:5 -/ + Source: 'src/layout/mod.rs', lines 1156:4-1192:5 -/ def layout.DstLayout.for_slice (T : Type) : Result layout.DstLayout := do let i ← core.mem.align_of T let o ← @@ -967,7 +1568,7 @@ def layout.DstLayout.for_slice (T : Type) : Result layout.DstLayout := do } /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::requires_static_padding]: - Source: 'src/layout/mod.rs', lines 1580:4-1589:5 + Source: 'src/layout/mod.rs', lines 1603:4-1612:5 Visibility: public -/ def layout.DstLayout.requires_static_padding (self : layout.DstLayout) : Result Bool := do @@ -1402,44 +2003,4 @@ def util.checks.check_arithmetic massert (i3 = i4) else ok () -/-- [zerocopy::util::max]: - Source: 'src/util/mod.rs', lines 289:0-295: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::min]: - Source: 'src/util/mod.rs', lines 305:0-311: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 - end Zerocopy diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index 565f2aaf74..995d8e49aa 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -99,14 +99,39 @@ 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 -/ +@[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 + /-- [zerocopy::layout::RoundingAlignAndPhase] - Source: 'src/layout/mod.rs', lines 87:0-87:54 -/ + Source: 'src/layout/mod.rs', lines 90:0-90:54 -/ structure layout.RoundingAlignAndPhase where _0 : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner /-- [zerocopy::layout::TrailingSliceLayout] - Source: 'src/layout/mod.rs', lines 194:0-248:1 -/ + Source: 'src/layout/mod.rs', lines 197:0-251:1 -/ structure layout.TrailingSliceLayout (E : Type) where offset : Std.Usize elem_size : E @@ -114,14 +139,14 @@ structure layout.TrailingSliceLayout (E : Type) where size_rounding_align_and_phase : layout.RoundingAlignAndPhase /-- [zerocopy::layout::SizeInfo] - Source: 'src/layout/mod.rs', lines 56:0-59:1 -/ + Source: 'src/layout/mod.rs', lines 59:0-62:1 -/ @[discriminant isize] inductive layout.SizeInfo (E : Type) where | Sized : Std.Usize → layout.SizeInfo E | SliceDst : layout.TrailingSliceLayout E → layout.SizeInfo E /-- [zerocopy::layout::DstLayout] - Source: 'src/layout/mod.rs', lines 43:0-51:1 + Source: 'src/layout/mod.rs', lines 46:0-54:1 Visibility: public -/ structure layout.DstLayout where align : core.num.nonzero.NonZero Std.Usize diff --git a/verification/aeneas/lean/CompositionReference.lean b/verification/aeneas/lean/CompositionReference.lean new file mode 100644 index 0000000000..72ce682052 --- /dev/null +++ b/verification/aeneas/lean/CompositionReference.lean @@ -0,0 +1,500 @@ +/- 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 + +/-! +The Rust reference stores independent numeric alignment and phase witnesses. +These observations connect those witnesses to the mathematical fragment model. +The raw helper proofs check the extracted remainder and checked arithmetic; +they do not substitute a mathematical algorithm for an extracted computation. +-/ +open Aeneas Aeneas.Std +namespace Zerocopy.CompositionReference +open Zerocopy.Proofs +set_option linter.unusedSimpArgs false + +abbrev ReferenceLayout := layout.composition_checks.ReferenceLayout +abbrev ReferenceTail := layout.composition_checks.ReferenceTail +abbrev ReferenceSize := layout.composition_checks.ReferenceSize + +def tailValue (tail : ReferenceTail) : LayoutMath.Formula := + ⟨tail.base.val, tail.phase.val, tail.round_align.val, tail.elem_size.val, tail.offset.val⟩ + +def value (reference : ReferenceLayout) : LayoutMath.LayoutValue := + ⟨reference.align.val, + match reference.size with + | .Fixed bytes => .fixed bytes.val + | .Tail tail => .trailing (tailValue tail), + reference.unpadded⟩ + +def valid (reference : ReferenceLayout) : Prop := + match reference.size with + | .Fixed _ => True + | .Tail tail => tail.round_align.val.isPowerOfTwo ∧ tail.phase.val < tail.round_align.val + +def Matches (runtime_layout : layout.DstLayout) (reference : ReferenceLayout) : Prop := + runtime_layout.align.val = reference.align ∧ + runtime_layout.statically_shallow_unpadded = reference.unpadded ∧ + match runtime_layout.size_info, reference.size with + | .Sized bytes, .Fixed expected => bytes = expected + | .SliceDst actual, .Tail expected => + expected.round_align.val.isPowerOfTwo ∧ expected.phase < expected.round_align ∧ + actual.offset = expected.offset ∧ actual.elem_size = expected.elem_size ∧ + actual.size_base = expected.base ∧ + Usize.checked_add expected.round_align expected.phase = + some actual.size_rounding_align_and_phase._0.val + | _, _ => False + +theorem checked_encoding (tail : ReferenceTail) (encoded : Usize) + (h : Usize.checked_add tail.round_align tail.phase = some encoded) : + encoded.val = tail.round_align.val + tail.phase.val := by + have facts := Usize.checked_add_bv_spec tail.round_align tail.phase + rw [h] at facts + exact facts.2.1 + +theorem matches_value (runtime_layout : layout.DstLayout) (reference : ReferenceLayout) + (h : Matches runtime_layout reference) : + valid reference ∧ canonicalLayout runtime_layout ∧ layoutValue runtime_layout = value reference := by + obtain ⟨ha, hu, h⟩ := h + cases hr : runtime_layout.size_info <;> cases hs : reference.size <;> + simp only [hr, hs] at h + case Sized.Fixed bytes expected => + subst expected + exact ⟨by simp [valid, hs], by simp [canonicalLayout, hr], by simp [layoutValue, value, hr, hs, ha, hu]⟩ + case SliceDst.Tail actual expected => + obtain ⟨hp, hphase, ho, he, hb, hc⟩ := h + have hl := (UScalar.lt_equiv _ _).mp hphase + have hn := checked_encoding expected _ hc + have hv := Raw.trailing_view actual expected.round_align.val expected.phase.val hp hl hn + have positive := Nat.pos_of_isPowerOfTwo hp + refine ⟨by simpa only [valid, hs] using And.intro hp hl, ?_, ?_⟩ + · simp only [canonicalLayout, hr] + omega + · simp only [layoutValue, value, hr, hs, hv, tailValue, ha, hu, ho, he, hb] + +/- A checked sum succeeds exactly when its expected stored word is the sum. +This lemma also recovers the guard's machine-overflow bound. -/ +theorem checked_add_of_value (a b encoded : Usize) + (sum : encoded.val = a.val + b.val) : Usize.checked_add a b = some encoded := by + have facts := Usize.checked_add_bv_spec a b + have bound : encoded.val ≤ Usize.max := by scalar_tac + cases hc : Usize.checked_add a b with + | none => rw [hc] at facts; omega + | some result => + rw [hc] at facts + have same : result = encoded := UScalar.eq_of_val_eq (by omega) + simp only [same] + +theorem matches_of_value (runtime_layout : layout.DstLayout) (reference : ReferenceLayout) + (hrc : canonicalLayout runtime_layout) (hrv : valid reference) + (hv : layoutValue runtime_layout = value reference) : Matches runtime_layout reference := by + have ha := congrArg LayoutMath.LayoutValue.align hv + have hu := congrArg LayoutMath.LayoutValue.unpadded hv + have hp := congrArg LayoutMath.LayoutValue.payload hv + refine ⟨UScalar.eq_of_val_eq ha, hu, ?_⟩ + cases hr : runtime_layout.size_info <;> cases hs : reference.size <;> + simp only [layoutValue, value, hr, hs] at hp ⊢ + case Sized.Fixed bytes expected => + injection hp with he + exact UScalar.eq_of_val_eq he + case Sized.Tail => cases hp + case SliceDst.Fixed => cases hp + case SliceDst.Tail actual expected => + injection hp with formula + have hb := congrArg LayoutMath.Formula.base formula + have hphase := congrArg LayoutMath.Formula.phase formula + have hround := congrArg LayoutMath.Formula.align formula + have he := congrArg LayoutMath.Formula.elem formula + have ho := congrArg LayoutMath.Formula.offset formula + simp only [tailValue, trailingFormula, byteFormula] at hb hphase hround he ho + obtain ⟨pow2, phase_lt⟩ := (show expected.round_align.val.isPowerOfTwo ∧ + expected.phase.val < expected.round_align.val by simpa only [valid, hs] using hrv) + have positive : 0 < actual.size_rounding_align_and_phase._0.val.val := by + simpa only [canonicalLayout, hr] using hrc + have reconstruct := RoundingFacts.reconstruction _ positive + refine ⟨pow2, (UScalar.lt_equiv _ _).mpr phase_lt, + UScalar.eq_of_val_eq ho, UScalar.eq_of_val_eq he, UScalar.eq_of_val_eq hb, ?_⟩ + apply checked_add_of_value + omega + +/- Every canonical raw representation has a numeric witness. In particular, +this covers every nonzero rounding encoding, not just constructor outputs. -/ +theorem witness_exists (runtime_layout : layout.DstLayout) (hc : canonicalLayout runtime_layout) : + ∃ reference : ReferenceLayout, Matches runtime_layout reference := by + cases hs : runtime_layout.size_info with + | Sized bytes => + exact ⟨⟨runtime_layout.align.val, .Fixed bytes, runtime_layout.statically_shallow_unpadded⟩, + by simp [Matches, hs]⟩ + | SliceDst tail => + have positive : 0 < tail.size_rounding_align_and_phase._0.val.val := by + simpa only [canonicalLayout, hs] using hc + obtain ⟨⟨align, phase⟩, _, pow2, phase_lt, encoding, _, _⟩ := + WP.spec_imp_exists (Raw.encoding_components_spec tail.size_rounding_align_and_phase positive) + refine ⟨⟨runtime_layout.align.val, + .Tail ⟨tail.offset, tail.elem_size, tail.size_base, align.val, phase⟩, + runtime_layout.statically_shallow_unpadded⟩, ?_⟩ + refine ⟨rfl, rfl, ?_⟩ + simp only [hs] + exact ⟨pow2, (UScalar.lt_equiv _ _).mpr phase_lt, trivial, trivial, trivial, + checked_add_of_value _ _ _ encoding.symm⟩ + +theorem no_rounding_padding (bytes align rounded : Usize) (positive : 0 < align.val) + (hr : rounded.val = LayoutMath.roundUp bytes.val align.val) : + (rounded = bytes) ↔ bytes.val % align.val = 0 := by + constructor + · intro same + have aligned := (LayoutMath.roundUp_properties bytes.val align.val positive).2.2 + rw [← hr, same] at aligned + exact aligned + · intro zero + apply UScalar.eq_of_val_eq + rw [hr, LayoutMath.roundUp_eq bytes.val align.val zero] + +theorem scalar_max_value (a b : Usize) : + max a.val b.val = (if a > b then a else b).val := by + split <;> rename_i comparison + · exact max_eq_left (by scalar_tac) + · exact max_eq_right (by scalar_tac) + +end Zerocopy.CompositionReference + +namespace Zerocopy.Proofs.Raw +open Zerocopy.CompositionReference +set_option linter.unusedSimpArgs false + +theorem composition_matches_spec (runtime_layout : layout.DstLayout) (reference : ReferenceLayout) : + layout.composition_checks.matches_reference runtime_layout reference + ⦃ b => (b = true ↔ Matches runtime_layout reference) ⦄ := by + unfold layout.composition_checks.matches_reference + simp only [core.num.nonzero.NonZero.get, bind_ok] + split + · rename_i ha + split + · rename_i hu + cases hr : runtime_layout.size_info <;> cases hs : reference.size <;> + simp only [bind_ok, WP.spec_ok] + case Sized.Fixed bytes expected => simp [Matches, hr, hs, ha, hu] + case Sized.Tail bytes expected => simp [Matches, hr, hs] + case SliceDst.Fixed actual expected => simp [Matches, hr, hs] + case SliceDst.Tail actual expected => + step as ⟨enabled, he⟩ + split + · rename_i hp + have pow2 := Eq.mp he hp + split + · rename_i hphase + split + · rename_i ho + split + · rename_i hel + split + · rename_i hb + simp only [lift, bind_ok] + cases hc : Usize.checked_add expected.round_align expected.phase with + | none => simp [Matches, hr, hs, ha, hu, pow2, hphase, ho, hel, hb, hc] + | some encoded => + simp [core.num.nonzero.NonZero.get, bind_ok, WP.spec_ok, + Matches, hr, hs, ha, hu, pow2, hphase, ho, hel, hb, hc, eq_comm] + · simp [Matches, hr, hs, ha, hu, pow2, hphase, ho, hel, *] + · simp [Matches, hr, hs, ha, hu, pow2, hphase, ho, *] + · simp [Matches, hr, hs, ha, hu, pow2, hphase, *] + · simp [Matches, hr, hs, ha, hu, *] + · have np : ¬expected.round_align.val.isPowerOfTwo := by + intro h + have yes : enabled = true := Eq.mpr he h + contradiction + simp [Matches, hr, hs, ha, hu, np] + · simp [Matches, *] + · simp [Matches, *] + +theorem composition_round_up_spec (bytes align : Usize) : + layout.composition_checks.reference_round_up bytes align + ⦃ result => if align.val = 0 then result = none else + match result with + | none => Usize.max < LayoutMath.roundUp bytes.val align.val + | some rounded => rounded.val = LayoutMath.roundUp bytes.val align.val ⦄ := by + unfold layout.composition_checks.reference_round_up + split + · rename_i hz + simp [hz, UScalar.val] + · rename_i hn + have positive : 0 < align.val := by + have : align.val ≠ 0 := by simpa only [UScalar.eq_equiv, show (0#usize).val = 0 by simp] using hn + omega + step as ⟨remainder, hr⟩ + step with Usize.sub_spec (show remainder.val ≤ align.val by + have := Nat.mod_lt bytes.val positive + omega) as ⟨gap, hg, _⟩ + step as ⟨padding, hp⟩ + simp only [WP.spec_ok, show ¬align.val = 0 by omega, if_false] + have padding_value : padding.val = (align.val - bytes.val % align.val) % align.val := by + rw [hp, hg, hr] + have hc := Usize.checked_add_bv_spec bytes padding + rw [padding_value] at hc + cases hresult : Usize.checked_add bytes padding with + | none => + rw [hresult] at hc + unfold LayoutMath.roundUp + omega + | some rounded => + rw [hresult] at hc + unfold LayoutMath.roundUp + omega + +theorem composition_alignment_spec (align : Usize) : + layout.composition_checks.extension_alignment align + ⦃ b => (b = true ↔ alignmentDomain align.val) ⦄ := by + unfold layout.composition_checks.extension_alignment + step as ⟨enabled, he⟩ + split + · rename_i yes + have power := Eq.mp he yes + step as ⟨bound, hb⟩ + · rcases System.Platform.numBits_eq with h | h <;> simp [h] + have bv : bound.val = 2 ^ 29 := by + rw [hb] + rcases System.Platform.numBits_eq with h | h <;> simp [Usize.size, Usize.numBits, UScalarTy.Usize_numBits_eq, h] + simp only [WP.spec_ok, alignmentDomain, power, true_and, decide_eq_true_eq, + UScalar.le_equiv, bv] + · rename_i no + have np : ¬align.val.isPowerOfTwo := by + intro h + exact no (Eq.mpr he h) + simp [alignmentDomain, np] + +/- Successful independent padding exposes exactly the production fit predicate +and the complete stored result. Failed intermediate sums stay outside that +success domain; no metadata or isize bound is added. -/ +theorem composition_reference_pad_spec (reference : ReferenceLayout) : + layout.composition_checks.reference_pad reference + ⦃ result => ∀ expected, result = some expected → + reference.align.val.isPowerOfTwo ∧ (value reference).padFits Usize.max ∧ + value expected = (value reference).pad ∧ valid expected ⦄ := by + unfold layout.composition_checks.reference_pad + step as ⟨enabled, he⟩ + split + · rename_i yes + have power := Eq.mp he yes + have positive := Nat.pos_of_isPowerOfTwo power + cases hs : reference.size with + | Fixed bytes => + step with composition_round_up_spec bytes reference.align as ⟨rounded, hr⟩ + simp only [show ¬reference.align.val = 0 by omega, if_false] at hr + cases rounded with + | none => simp + | some rounded => + have bound : rounded.val ≤ Usize.max := by scalar_tac + have no_padding : (rounded = bytes) ↔ bytes.val % reference.align.val = 0 := by + constructor + · intro same + have aligned := (LayoutMath.roundUp_properties bytes.val reference.align.val positive).2.2 + rw [← hr, same] at aligned + exact aligned + · intro zero + apply UScalar.eq_of_val_eq + rw [hr, LayoutMath.roundUp_eq bytes.val reference.align.val zero] + simp only [WP.spec_ok] + intro expected same + cases same + refine ⟨power, ?_, ?_, by simp [valid]⟩ + · simpa only [value, hs, LayoutMath.LayoutValue.padFits, ← hr] using bound + · simp [value, hs, LayoutMath.LayoutValue.pad, hr, no_padding] + | Tail tail => + step as ⟨tail_enabled, hte⟩ + split + · rename_i ty + have tail_power := Eq.mp hte ty + split + · simp + · rename_i phase_small + have phase_lt : tail.phase.val < tail.round_align.val := by scalar_tac + split + · rename_i inner_large + have nlt : ¬tail.round_align.val < reference.align.val := by scalar_tac + step with composition_round_up_spec tail.base reference.align as ⟨base, hb⟩ + simp only [show ¬reference.align.val = 0 by omega, if_false] at hb + cases base with + | none => simp + | some base => + have bound : base.val ≤ Usize.max := by scalar_tac + simp only [WP.spec_ok] + intro expected same + cases same + refine ⟨power, ?_, ?_, ?_⟩ + · simpa only [value, hs, tailValue, LayoutMath.LayoutValue.padFits, + nlt, if_false, ← hb] using bound + · simp [value, hs, tailValue, LayoutMath.LayoutValue.pad, + LayoutMath.Formula.pad, nlt, hb] + · simpa only [valid] using And.intro tail_power phase_lt + · rename_i outer_large + have lt : tail.round_align.val < reference.align.val := by scalar_tac + have tail_positive := Nat.pos_of_isPowerOfTwo tail_power + step with composition_round_up_spec tail.base tail.round_align as ⟨base, hb⟩ + simp only [show ¬tail.round_align.val = 0 by omega, if_false] at hb + cases base with + | none => simp + | some base => + step as ⟨fixed, hf⟩ + cases fixed with + | none => simp + | some fixed => + simp only [] at hf + step as ⟨phase, hp⟩ + step with Usize.sub_spec (show phase.val ≤ fixed.val by + rw [hp]; exact Nat.mod_le _ _) as ⟨newbase, hn, _⟩ + have small : phase.val < reference.align.val := by + rw [hp]; exact Nat.mod_lt _ positive + intro expected same + cases same + refine ⟨power, ?_, ?_, by simpa only [valid] using And.intro power small⟩ + · simp only [value, hs, tailValue, LayoutMath.LayoutValue.padFits, + lt, if_true] + omega + · have fixed_value : fixed.val = LayoutMath.roundUp tail.base.val tail.round_align.val + tail.phase.val := by omega + simp [value, hs, tailValue, LayoutMath.LayoutValue.pad, + LayoutMath.Formula.pad, lt, hn, hp, fixed_value] + · simp + · simp + +theorem composition_reference_extend_at_spec (preceding field : ReferenceLayout) + (field_align : Usize) (positive : 0 < field_align.val) + (minimum : field_align.val ≤ field.align.val) : + layout.composition_checks.reference_extend_at preceding field field_align + ⦃ result => ∀ expected, result = some expected → + (value preceding).extendFits (value field) field_align.val Usize.max ∧ + value expected = (value preceding).extend (value field) field_align.val ∧ + (valid field → valid expected) ⦄ := by + unfold layout.composition_checks.reference_extend_at + have min_eq : min field.align.val field_align.val = field_align.val := min_eq_right minimum + cases hs : preceding.size with + | Tail tail => simp + | Fixed bytes => + step with composition_round_up_spec bytes field_align as ⟨offset, ho⟩ + simp only [show ¬field_align.val = 0 by omega, if_false] at ho + cases offset with + | none => simp + | some offset => + have no_padding := no_rounding_padding bytes field_align offset positive ho + cases hf : field.size with + | Fixed fieldbytes => + step as ⟨total, ht⟩ + cases total with + | none => simp + | some total => + simp only [] at ht + by_cases comparison : preceding.align > field_align + all_goals + simp only [comparison, if_true, if_false, bind_ok, WP.spec_ok] + intro expected same + cases same + refine ⟨?_, ?_, ?_⟩ + · simp only [value, hs, hf, LayoutMath.LayoutValue.extendFits, min_eq] + omega + · simp only [value, hs, hf, LayoutMath.LayoutValue.extend, min_eq] + have total_value : total.val = LayoutMath.roundUp bytes.val field_align.val + fieldbytes.val := by omega + simp [total_value, ho, no_padding, scalar_max_value, comparison] + · simp [valid] + | Tail tail => + step as ⟨slice_offset, ht⟩ + cases slice_offset with + | none => simp + | some slice_offset => + simp only [] at ht + step as ⟨base, hb⟩ + cases base with + | none => simp + | some base => + simp only [] at hb + by_cases comparison : preceding.align > field_align + all_goals + simp only [comparison, if_true, if_false, bind_ok, WP.spec_ok] + intro expected same + cases same + refine ⟨?_, ?_, ?_⟩ + · simp only [value, hs, hf, tailValue, LayoutMath.LayoutValue.extendFits, min_eq] + constructor <;> omega + · simp only [value, hs, hf, tailValue, LayoutMath.LayoutValue.extend, min_eq] + have offset_value : slice_offset.val = LayoutMath.roundUp bytes.val field_align.val + tail.offset.val := by omega + have base_value : base.val = LayoutMath.roundUp bytes.val field_align.val + tail.base.val := by omega + simp [offset_value, base_value, ho, no_padding, scalar_max_value, comparison] + · intro validity + simpa only [valid, hf] using validity + +theorem composition_reference_extend_spec (preceding field : ReferenceLayout) + (packed : Option NonZeroUsize) : + layout.composition_checks.reference_extend preceding field packed + ⦃ result => ∀ expected, result = some expected → + alignmentDomain preceding.align.val ∧ alignmentDomain field.align.val ∧ + (∀ a ∈ packed, alignmentDomain a.val.val) ∧ + (value preceding).extendFits (value field) (packingValue packed) Usize.max ∧ + value expected = (value preceding).extend (value field) (packingValue packed) ∧ + (valid field → valid expected) ⦄ := by + unfold layout.composition_checks.reference_extend + step with composition_alignment_spec preceding.align as ⟨preceding_ok, hp⟩ + split + · rename_i py + have preceding_domain := hp.mp py + step with composition_alignment_spec field.align as ⟨field_ok, hf⟩ + split + · rename_i fy + have field_domain := hf.mp fy + cases packed with + | none => + have limit : 2 ^ 29 ≤ packingValue none := by + rcases System.Platform.numBits_eq with h | h <;> simp [packingValue, h] + have field_bound := field_domain.2 + have minimum : min field.align.val (packingValue none) = field.align.val := + min_eq_left (by omega) + apply WP.spec_mono (composition_reference_extend_at_spec preceding field field.align + (Nat.pos_of_isPowerOfTwo field_domain.1) le_rfl) + intro result facts expected same + obtain ⟨fits, output, validity⟩ := facts expected same + refine ⟨preceding_domain, field_domain, by simp, ?_, ?_, validity⟩ + · simpa only [LayoutMath.LayoutValue.extendFits, minimum, + show (value field).align = field.align.val from rfl, min_self] using fits + · simpa only [LayoutMath.LayoutValue.extend, minimum, + show (value field).align = field.align.val from rfl, min_self] using output + | some cap => + simp only [core.num.nonzero.NonZero.get, bind_ok] + step with composition_alignment_spec cap.val as ⟨cap_ok, hc⟩ + split + · rename_i cy + have cap_domain := hc.mp cy + have choice : (if field.align < cap.val then Result.ok field.align else Result.ok cap.val) + ⦃ effective => effective.val = min field.align.val cap.val.val ∧ 0 < effective.val ⦄ := by + by_cases cmp : field.align < cap.val + · simp only [cmp, if_true, WP.spec_ok] + exact ⟨(min_eq_left (by scalar_tac)).symm, Nat.pos_of_isPowerOfTwo field_domain.1⟩ + · simp only [cmp, if_false, WP.spec_ok] + exact ⟨(min_eq_right (by scalar_tac)).symm, Nat.pos_of_isPowerOfTwo cap_domain.1⟩ + step with choice as ⟨effective, he, positive⟩ + apply WP.spec_mono (composition_reference_extend_at_spec preceding field effective positive + (by rw [he]; exact min_le_left _ _)) + intro result facts expected same + obtain ⟨fits, output, validity⟩ := facts expected same + refine ⟨preceding_domain, field_domain, ?_, ?_, ?_, validity⟩ + · intro a member + have same : a = cap := by simpa [eq_comm] using member + subst a + exact cap_domain + · simpa only [LayoutMath.LayoutValue.extendFits, packingValue, Option.map_some, + Option.getD_some, show (value field).align = field.align.val from rfl, + min_eq_right (show effective.val ≤ field.align.val by rw [he]; exact min_le_left _ _), he, + min_eq_right (min_le_left field.align.val cap.val.val)] using fits + · simpa only [LayoutMath.LayoutValue.extend, packingValue, Option.map_some, + Option.getD_some, show (value field).align = field.align.val from rfl, + min_eq_right (show effective.val ≤ field.align.val by rw [he]; exact min_le_left _ _), he, + min_eq_right (min_le_left field.align.val cap.val.val)] using output + · simp + · simp + · simp + +end Zerocopy.Proofs.Raw diff --git a/verification/aeneas/lean/Corollaries.lean b/verification/aeneas/lean/Corollaries.lean index 8adb0db7fd..f5ccc84d61 100644 --- a/verification/aeneas/lean/Corollaries.lean +++ b/verification/aeneas/lean/Corollaries.lean @@ -83,6 +83,43 @@ theorem round_down_monotone (a b : Usize) (align : NonZeroUsize) apply (UScalar.le_equiv _ _).mpr exact hgreatest m.val ((UScalar.le_equiv _ _).mp (le_trans hbound hab)) haligned +theorem pad_to_align_sized_headroom (self : layout.DstLayout) (size : Usize) + (hs : self.size_info = .Sized size) + (hpow : self.align.val.val.isPowerOfTwo) + (hroom : size.val + self.align.val.val - 1 ≤ Usize.max) : + ∃ r, layout.DstLayout.pad_to_align self = .ok r := by + have hpos := Nat.pos_of_isPowerOfTwo hpow + have hlt := Nat.mod_lt (self.align.val.val - size.val % self.align.val.val) hpos + have hp := Proofs.Raw.pad_to_align_spec self hpow (by + simp only [hs, LayoutMath.roundUp] + omega) + obtain ⟨r, hr, _⟩ := WP.spec_imp_exists hp + exact ⟨r, hr⟩ + +theorem pad_to_align_size (self : layout.DstLayout) + (ha : self.align.val.val.isPowerOfTwo) + (hc : canonicalLayout self) + (hf : (layoutValue self).padFits Usize.max) : + layout.DstLayout.pad_to_align self + ⦃ r => ∀ n : Nat, (layoutValue r).size n = + LayoutMath.roundUp ((layoutValue self).size n) self.align.val.val ⦄ := by + step with Proofs.Raw.pad_value_spec self ha hc hf as ⟨r, hr, _⟩ + rw [hr] + rename_i n + cases hs : self.size_info with + | Sized size => simp only [layoutValue, hs, LayoutMath.LayoutValue.pad, LayoutMath.LayoutValue.size] + | SliceDst tail => + simp only [layoutValue, hs, LayoutMath.LayoutValue.pad, LayoutMath.LayoutValue.size] + apply LayoutMath.pad_size _ _ _ (trailing_align_pos tail) (Nat.pos_of_isPowerOfTwo ha) + have hinner : (trailingFormula tail).align.isPowerOfTwo := by + simp only [trailingFormula, byteFormula] + exact ⟨_, rfl⟩ + split + · rename_i h + exact power_dvd_of_le _ _ hinner ha (by omega) + · rename_i h + exact power_dvd_of_le _ _ ha hinner (by omega) + theorem size_matches_recursive (tail : layout.TrailingSliceLayout Usize) (description : LayoutMath.Description) (n : Usize) (hn : 0 < tail.size_rounding_align_and_phase._0.val.val) diff --git a/verification/aeneas/lean/ModelProjectionLaws.lean b/verification/aeneas/lean/ModelProjectionLaws.lean index 0c97fd6b6d..ee370fdc45 100644 --- a/verification/aeneas/lean/ModelProjectionLaws.lean +++ b/verification/aeneas/lean/ModelProjectionLaws.lean @@ -80,4 +80,171 @@ theorem optionalSize_decode (raw : Option Usize) (value : Option (UnsignedWord . Option.some.injEq] at h <;> cases h <;> rfl +/-- Padding's existing view retains every exact field observation required by +its raw contract, including the size variant and the unpadded flag. -/ +theorem layout_pad_iff (self result : layout.DstLayout) : + layoutValue result = (layoutValue self).pad ↔ + result.align = self.align ∧ match self.size_info with + | .Sized bytes => ∃ padded, result.size_info = .Sized padded ∧ + padded.val = LayoutMath.roundUp bytes.val self.align.val.val ∧ + result.statically_shallow_unpadded = + (self.statically_shallow_unpadded && decide (bytes.val % self.align.val.val = 0)) + | .SliceDst tail => ∃ next, result.size_info = .SliceDst next ∧ + trailingFormula next = (trailingFormula tail).pad self.align.val.val ∧ + result.statically_shallow_unpadded = self.statically_shallow_unpadded := by + constructor + · intro h + have ha := congrArg LayoutMath.LayoutValue.align h + have hp := congrArg LayoutMath.LayoutValue.payload h + have hu := congrArg LayoutMath.LayoutValue.unpadded h + have align : result.align = self.align := by + have hv : result.align.val = self.align.val := UScalar.eq_of_val_eq ha + have ext : ∀ a b : NonZeroUsize, a.val = b.val → a = b := by + rintro ⟨a⟩ ⟨b⟩ h + cases h + rfl + exact ext result.align self.align hv + refine ⟨align, ?_⟩ + cases hs : self.size_info <;> cases hr : result.size_info <;> + simp only [layoutValue, LayoutMath.LayoutValue.pad, hs, hr, + LayoutMath.Payload.fixed.injEq, LayoutMath.Payload.trailing.injEq, + reduceCtorEq] at hp hu ⊢ + all_goals exact ⟨_, rfl, hp, hu⟩ + · rintro ⟨ha, h⟩ + cases hs : self.size_info with + | Sized bytes => + simp only [hs] at h + rcases h with ⟨padded, hr, hp, hu⟩ + simp only [layoutValue, LayoutMath.LayoutValue.pad, hs, hr, ha, hp, hu] + | SliceDst tail => + simp only [hs] at h + rcases h with ⟨next, hr, hp, hu⟩ + simp only [layoutValue, LayoutMath.LayoutValue.pad, hs, hr, ha, hp, hu] + +/-- Exact physical offset and stride remain observable through the padding view; +equality of bounded words follows from equality of their numeric projections. -/ +theorem layout_pad_trailing_fields (self result : layout.DstLayout) + (tail : layout.TrailingSliceLayout Usize) + (hs : self.size_info = .SliceDst tail) + (h : layoutValue result = (layoutValue self).pad) : + ∃ next, result.size_info = .SliceDst next ∧ + next.offset = tail.offset ∧ next.elem_size = tail.elem_size := by + have facts := (layout_pad_iff self result).mp h + simp only [hs] at facts + obtain ⟨next, hn, hf, _⟩ := facts.2 + refine ⟨next, hn, UScalar.eq_of_val_eq ?_, UScalar.eq_of_val_eq ?_⟩ + · have ho := congrArg LayoutMath.Formula.offset hf + dsimp only [LayoutMath.Formula.pad] at ho + split at ho <;> exact ho + · have he := congrArg LayoutMath.Formula.elem hf + dsimp only [LayoutMath.Formula.pad] at he + split at he <;> exact he + +theorem packingValue_decode (raw : Option NonZeroUsize) + (value : Option NonZeroUsizeValue) + (h : RustModel.decode raw = some value) : + ModelViews.packingValue value = packingValue raw := by + cases raw with + | none => simp only [RustModel.decode, Option.some.injEq] at h; cases h; rfl + | some align => + obtain ⟨decoded, hd, rfl⟩ := (Option.map_eq_some_iff).mp h + have ha := (decodeNonZeroUScalar_iff align decoded).mp hd + simp only [ModelViews.packingValue, packingValue, Option.map_some, + Option.getD_some, ha] + +/-- The optional packing model preserves every admitted alignment observation. -/ +theorem packing_alignment_decode (raw : Option NonZeroUsize) + (value : Option NonZeroUsizeValue) (h : RustModel.decode raw = some value) : + (∀ a ∈ value, alignmentDomain a.value) ↔ + (∀ a ∈ raw, alignmentDomain a.val.val) := by + cases raw with + | none => simp only [RustModel.decode, Option.some.injEq] at h; cases h; simp + | some align => + obtain ⟨decoded, hd, rfl⟩ := (Option.map_eq_some_iff).mp h + have ha := (decodeNonZeroUScalar_iff align decoded).mp hd + simp only [Option.mem_some_iff, forall_eq', ha] + +/-- Positive rounding encodings are recovered from both observed components. -/ +theorem rounding_eq_of_components (left right : layout.RoundingAlignAndPhase) + (hl : 0 < left._0.val.val) (hr : 0 < right._0.val.val) + (ha : 2 ^ Nat.log2 left._0.val.val = 2 ^ Nat.log2 right._0.val.val) + (hp : left._0.val.val - 2 ^ Nat.log2 left._0.val.val = + right._0.val.val - 2 ^ Nat.log2 right._0.val.val) : left = right := by + have hleft := RoundingFacts.reconstruction left._0.val.val hl + have hright := RoundingFacts.reconstruction right._0.val.val hr + have words : left._0.val.val = right._0.val.val := by omega + cases left; cases right + congr 1 + cases ‹NonZeroUsize›; cases ‹NonZeroUsize› + congr 1 + exact UScalar.eq_of_val_eq words + +/-- Extension admission uses the same two machine bounds as the raw contract. -/ +theorem layout_extendFits_iff (self field : layout.DstLayout) + (packed : Option NonZeroUsize) (size : Usize) + (hs : self.size_info = .Sized size) : + (layoutValue self).extendFits (layoutValue field) (packingValue packed) Usize.max ↔ + match field.size_info with + | .Sized field_size => placement size field packed + field_size.val ≤ Usize.max + | .SliceDst tail => placement size field packed + tail.offset.val ≤ Usize.max ∧ + placement size field packed + tail.size_base.val ≤ Usize.max := by + cases hf : field.size_info <;> + simp only [layoutValue, hs, hf, LayoutMath.LayoutValue.extendFits, + placement, fieldAlignment, trailingFormula, byteFormula] + +/-- The extension equation preserves all original observations, including the +stored rounding code, throughout the independently promised admitted domain. -/ +theorem layout_extend_iff (self field result : layout.DstLayout) + (packed : Option NonZeroUsize) (size : Usize) + (hs : self.size_info = .Sized size) + (hcfield : canonicalLayout field) (hcresult : canonicalLayout result) : + layoutValue result = (layoutValue self).extend (layoutValue field) (packingValue packed) ↔ + result.align.val.val = max self.align.val.val (fieldAlignment field packed) ∧ + result.statically_shallow_unpadded = (self.statically_shallow_unpadded && + field.statically_shallow_unpadded && decide (size.val % fieldAlignment field packed = 0)) ∧ + match field.size_info with + | .Sized field_size => ∃ next, result.size_info = .Sized next ∧ + next.val = placement size field packed + field_size.val + | .SliceDst tail => ∃ next, result.size_info = .SliceDst next ∧ + next.offset.val = placement size field packed + tail.offset.val ∧ + next.size_base.val = placement size field packed + tail.size_base.val ∧ + next.elem_size = tail.elem_size ∧ + next.size_rounding_align_and_phase = tail.size_rounding_align_and_phase := by + constructor + · intro h + have ha := congrArg LayoutMath.LayoutValue.align h + have hp := congrArg LayoutMath.LayoutValue.payload h + have hu := congrArg LayoutMath.LayoutValue.unpadded h + simp only [layoutValue, hs, LayoutMath.LayoutValue.extend] at ha hu + refine ⟨ha, hu, ?_⟩ + cases hf : field.size_info <;> cases hr : result.size_info <;> + simp only [layoutValue, hs, hf, hr, LayoutMath.LayoutValue.extend, + LayoutMath.Payload.fixed.injEq, LayoutMath.Payload.trailing.injEq, + reduceCtorEq] at hp ⊢ + · exact ⟨_, rfl, hp⟩ + · rename_i tail next + have ho := congrArg LayoutMath.Formula.offset hp + have hb := congrArg LayoutMath.Formula.base hp + have he := congrArg LayoutMath.Formula.elem hp + have halign := congrArg LayoutMath.Formula.align hp + have hphase := congrArg LayoutMath.Formula.phase hp + simp only [canonicalLayout, hf] at hcfield + simp only [canonicalLayout, hr] at hcresult + exact ⟨next, rfl, ho, hb, UScalar.eq_of_val_eq he, + rounding_eq_of_components _ _ hcresult hcfield halign hphase⟩ + · rintro ⟨ha, hu, h⟩ + cases hf : field.size_info with + | Sized fieldSize => + simp only [hf] at h + obtain ⟨next, hr, hv⟩ := h + simp only [layoutValue, hs, hf, hr, LayoutMath.LayoutValue.extend, + placement, fieldAlignment, ha, hu, hv] + rfl + | SliceDst tail => + simp only [hf] at h + obtain ⟨next, hr, ho, hb, he, hc⟩ := h + simp only [layoutValue, hs, hf, hr, LayoutMath.LayoutValue.extend, + placement, fieldAlignment, trailingFormula, byteFormula, ha, hu, ho, hb, he, hc] + rfl + end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Obligations.lean b/verification/aeneas/lean/Obligations.lean index a645741c05..62ce35cca4 100644 --- a/verification/aeneas/lean/Obligations.lean +++ b/verification/aeneas/lean/Obligations.lean @@ -250,6 +250,56 @@ def for_slice_spec : Prop := ∀ (T : Type), for_slice_spec_contract T (layout.DstLayout.for_slice T) +def extend_spec_contract (self field : layout.DstLayout) (packing : Option NonZeroUsize) + (run : Result layout.DstLayout) : Prop := + ∀ (size : Usize), + layoutValid self → layoutValid field → (∀ a ∈ packing, 0 < a.val.val) → + self.size_info = .Sized size → + (self.align.val.val.isPowerOfTwo ∧ self.align.val.val ≤ 2 ^ 29) → + (field.align.val.val.isPowerOfTwo ∧ field.align.val.val ≤ 2 ^ 29) → + (∀ a ∈ packing, a.val.val.isPowerOfTwo ∧ a.val.val ≤ 2 ^ 29) → + (match field.size_info with + | .Sized s => placement size field packing + s.val ≤ Usize.max + | .SliceDst t => placement size field packing + t.offset.val ≤ Usize.max ∧ + placement size field packing + t.size_base.val ≤ Usize.max) → + run ⦃ r => layoutValid r ∧ + r.align.val.val = Nat.max self.align.val.val (fieldAlignment field packing) ∧ + r.statically_shallow_unpadded = (self.statically_shallow_unpadded && + field.statically_shallow_unpadded && decide (size.val % fieldAlignment field packing = 0)) ∧ + match field.size_info with + | .Sized s => ∃ bytes, r.size_info = .Sized bytes ∧ bytes.val = placement size field packing + s.val + | .SliceDst t => ∃ next, r.size_info = .SliceDst next ∧ + next.offset.val = placement size field packing + t.offset.val ∧ + next.size_base.val = placement size field packing + t.size_base.val ∧ + next.elem_size = t.elem_size ∧ next.size_rounding_align_and_phase = t.size_rounding_align_and_phase ⦄ + +def extend_spec : Prop := + ∀ (self field : layout.DstLayout) (packing : Option NonZeroUsize), + extend_spec_contract self field packing (layout.DstLayout.extend self field packing) + +def pad_to_align_spec_contract (self : layout.DstLayout) + (run : Result layout.DstLayout) : Prop := + layoutValid self → self.align.val.val.isPowerOfTwo → + (match self.size_info with + | .Sized bytes => LayoutMath.roundUp bytes.val self.align.val.val ≤ Usize.max + | .SliceDst t => 0 < t.size_rounding_align_and_phase._0.val.val ∧ + (if (trailingFormula t).align < self.align.val.val then + LayoutMath.roundUp t.size_base.val (trailingFormula t).align + (trailingFormula t).phase ≤ Usize.max + else LayoutMath.roundUp t.size_base.val self.align.val.val ≤ Usize.max)) → + run ⦃ r => layoutValid r ∧ r.align = self.align ∧ + match self.size_info with + | .Sized bytes => ∃ padded, r.size_info = .Sized padded ∧ + padded.val = LayoutMath.roundUp bytes.val self.align.val.val ∧ + r.statically_shallow_unpadded = + (self.statically_shallow_unpadded && decide (bytes.val % self.align.val.val = 0)) + | .SliceDst t => ∃ next, r.size_info = .SliceDst next ∧ + trailingFormula next = (trailingFormula t).pad self.align.val.val ∧ + r.statically_shallow_unpadded = self.statically_shallow_unpadded ⦄ + +def pad_to_align_spec : Prop := + ∀ (self : layout.DstLayout), + pad_to_align_spec_contract self (layout.DstLayout.pad_to_align self) + def requires_static_padding_spec_contract (self : layout.DstLayout) (run : Result Bool) : Prop := layoutValid self → ∃ r, run = .ok r ∧ diff --git a/verification/aeneas/lean/Obligations/CompositionChecks.lean b/verification/aeneas/lean/Obligations/CompositionChecks.lean new file mode 100644 index 0000000000..758492ba82 --- /dev/null +++ b/verification/aeneas/lean/Obligations/CompositionChecks.lean @@ -0,0 +1,42 @@ +/- 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 +@[expose] public section + +/-! +These independent expectations require each ordinary Rust harness to terminate +successfully, including its assertions. The premises describe the positive +NonZeroUsize representations admitted by Rust's types; numeric witnesses carry +no semantic validity requirement, since the harnesses check them themselves. +-/ +open Aeneas Aeneas.Std +namespace Zerocopy.Obligations +open Zerocopy.Proofs +abbrev CompositionReferenceLayout := layout.composition_checks.ReferenceLayout + +def composition_extend_checks_spec_contract (preceding field : layout.DstLayout) + (packed : Option NonZeroUsize) (_preceding_reference _field_reference : CompositionReferenceLayout) + (run : Result Unit) : Prop := + layoutValid preceding → layoutValid field → (∀ a ∈ packed, 0 < a.val.val) → run ⦃ _ => True ⦄ + +def composition_extend_checks_spec : Prop := + ∀ preceding field packed preceding_reference field_reference, + composition_extend_checks_spec_contract preceding field packed preceding_reference field_reference + (layout.composition_checks.check_extend preceding field packed preceding_reference field_reference) + +def composition_pad_checks_spec_contract (runtime_layout : layout.DstLayout) + (_reference : CompositionReferenceLayout) (run : Result Unit) : Prop := + layoutValid runtime_layout → run ⦃ _ => True ⦄ + +def composition_pad_checks_spec : Prop := + ∀ runtime_layout reference, composition_pad_checks_spec_contract runtime_layout reference + (layout.composition_checks.check_pad runtime_layout reference) + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs.lean b/verification/aeneas/lean/Proofs.lean index 79cb66444e..026aec8d1a 100644 --- a/verification/aeneas/lean/Proofs.lean +++ b/verification/aeneas/lean/Proofs.lean @@ -583,6 +583,407 @@ theorem new_zst_spec : exact Eq.mpr hb' trivial simp [massert, hbt, bind_ok, WP.spec_ok] +theorem decoded_encoding (a p : Nat) (ha : a.isPowerOfTwo) (hp : p < a) : + 2 ^ Nat.log2 (a + p) = a ∧ a + p - 2 ^ Nat.log2 (a + p) = p := by + obtain ⟨k, hk⟩ := ha + have hpos := Nat.two_pow_pos k + have hlog : Nat.log2 (a + p) = k := by + apply (Nat.log2_eq_iff (by omega)).mpr + rw [Nat.pow_succ] + omega + rw [hlog, ← hk] + omega + +theorem trailing_view (self : layout.TrailingSliceLayout Usize) (a p : Nat) + (ha : a.isPowerOfTwo) (hp : p < a) + (hn : self.size_rounding_align_and_phase._0.val.val = a + p) : + trailingFormula self = ⟨self.size_base.val, p, a, self.elem_size.val, self.offset.val⟩ := by + obtain ⟨hd, _⟩ := decoded_encoding a p ha hp + simp only [trailingFormula, byteFormula, hn, hd, Nat.add_sub_cancel_left] + +/- Preserve the inner complete-size calculation while adding outer padding. The +proof separately tracks physical offset, normalized base/phase, alignment, +and the unpadded flag; equal total sizes alone would be insufficient. +-/ +theorem pad_to_align_spec : + ∀ (self : layout.DstLayout), ∀ (ha : (self.align.val.val.isPowerOfTwo : Prop)), ∀ (hfit : (match self.size_info with + | .Sized size => LayoutMath.roundUp size.val self.align.val.val ≤ Usize.max + | .SliceDst tail => + 0 < tail.size_rounding_align_and_phase._0.val.val ∧ + (if (trailingFormula tail).align < self.align.val.val then + LayoutMath.roundUp tail.size_base.val (trailingFormula tail).align + + (trailingFormula tail).phase ≤ Usize.max + else LayoutMath.roundUp tail.size_base.val self.align.val.val ≤ Usize.max) : Prop)), + @Zerocopy.layout.DstLayout.pad_to_align self ⦃ r => canonicalLayout r ∧ r.align = self.align ∧ match self.size_info with + | .Sized size => ∃ padded, + r.size_info = .Sized padded ∧ padded.val = LayoutMath.roundUp size.val self.align.val.val ∧ + r.statically_shallow_unpadded = (self.statically_shallow_unpadded && decide (size.val % self.align.val.val = 0)) + | .SliceDst tail => ∃ t, + r.size_info = .SliceDst t ∧ trailingFormula t = (trailingFormula tail).pad self.align.val.val ∧ + r.statically_shallow_unpadded = self.statically_shallow_unpadded ⦄ := by + intro self ha hfit + unfold layout.DstLayout.pad_to_align + cases hs : self.size_info with + | Sized size => + simp only [hs] at hfit + step with Zerocopy.Proofs.Raw.padding_lt_alignment size self.align ha as ⟨p, _, hp, _, _, hz⟩ + have hsum : size.val + p.val = LayoutMath.roundUp size.val self.align.val.val := by + rw [hp] + rfl + step as ⟨checked, hc⟩ + cases checked with + | none => simp only [] at hc; omega + | some padded => + simp only [] at hc + have hzero : (p = 0#usize) = (size.val % self.align.val.val = 0) := by + apply propext + simpa only [UScalar.eq_equiv, show (0#usize).val = 0 by simp] using hz + cases hb : self.statically_shallow_unpadded <;> + simp only [Bool.false_and, Bool.true_and, Bool.false_eq_true, + if_false, if_true, WP.spec_ok, canonicalLayout] + all_goals exact ⟨True.intro, by trivial, _, by trivial, by omega, by simp only [hzero]⟩ + | SliceDst tail => + simp only [hs] at hfit + step with encoding_components_spec _ hfit.1 as ⟨a, p, hap, hpa, henc, halign, hphase⟩ + have hv := trailing_view tail a.val.val p.val hap hpa henc.symm + rw [hv] at hfit + dsimp only at hfit + simp only [core.num.nonzero.NonZero.get, bind_ok, UScalar.lt_equiv] + split + · rename_i hab + have hbound := hfit.2 + simp only [hab, if_true] at hbound + step with Zerocopy.Proofs.Raw.padding_lt_alignment tail.size_base a hap as ⟨bp, _, hbp, _, _, _⟩ + have hb : tail.size_base.val + bp.val = LayoutMath.roundUp tail.size_base.val a.val.val := by rw [hbp]; rfl + step as ⟨checked, hc⟩ + cases checked with + | none => simp only [] at hc; omega + | some base => + simp only [] at hc + step as ⟨checked, hbytes⟩ + cases checked with + | none => simp only [] at hbytes; omega + | some bytes => + simp only [] at hbytes + simp only [] + have apos := Nat.pos_of_isPowerOfTwo ha + step with Usize.sub_spec (show (1#usize).val ≤ self.align.val.val by simpa using (show 1 ≤ self.align.val.val by omega)) as ⟨mask, hm, _⟩ + have hlow : (bytes &&& mask).val = bytes.val % self.align.val.val := by + obtain ⟨k, hk⟩ := ha + rw [UScalar.val_and, hm, hk, Nat.and_two_pow_sub_one_eq_mod] + simp only [lift, bind_ok] + step with round_down_spec bytes self.align ha as ⟨normalized, _, hnorm, _, _, _⟩ + step with encoding_new_spec self.align (bytes &&& mask) ha (by rw [hlow]; exact Nat.mod_lt _ apos) as ⟨encoded, he⟩ + have hencoded : encodingValid encoded := by + unfold encodingValid + rw [he] + omega + have hnew := trailing_view + ({ tail with size_base := normalized, size_rounding_align_and_phase := encoded }) + self.align.val.val (bytes.val % self.align.val.val) ha (Nat.mod_lt _ apos) + (by rw [he, hlow]) + cases hflag : self.statically_shallow_unpadded <;> + simp only [Bool.false_eq_true, decide_true, + if_true, if_false, WP.spec_ok, canonicalLayout] + all_goals + refine ⟨hencoded, by trivial, _, by trivial, ?_, by trivial⟩ + rw [hnew, hv] + simp only [LayoutMath.Formula.pad, hab, if_true] + rw [hnorm, hbytes.2.1, hc.2.1, hb] + · rename_i hab + have hbound := hfit.2 + simp only [hab, if_false] at hbound + step with Zerocopy.Proofs.Raw.padding_lt_alignment tail.size_base self.align ha as ⟨bp, _, hbp, _, _, _⟩ + have hb : tail.size_base.val + bp.val = LayoutMath.roundUp tail.size_base.val self.align.val.val := by rw [hbp]; rfl + step as ⟨checked, hc⟩ + cases checked with + | none => simp only [] at hc; omega + | some base => + simp only [] at hc + have hnew := trailing_view ({ tail with size_base := base }) a.val.val p.val hap hpa henc.symm + cases hflag : self.statically_shallow_unpadded <;> + simp only [Bool.false_eq_true, decide_true, + if_true, if_false, WP.spec_ok, canonicalLayout] + all_goals + refine ⟨hfit.1, by trivial, _, by trivial, ?_, by trivial⟩ + rw [hnew, hv] + simp only [LayoutMath.Formula.pad, hab, if_false] + rw [hc.2.1, hb] + +theorem current_max_align_spec : + layout.DstLayout.CURRENT_MAX_ALIGN + ⦃ a => a.val.val = 2 ^ 29 ⦄ := by + unfold layout.DstLayout.CURRENT_MAX_ALIGN + step as ⟨i, hi, _⟩ + · have := System.Platform.numBits_eq + scalar_tac + · have hv : i.val = 2 ^ 29 := by + rw [Nat.shiftLeft_eq, Nat.one_mul] at hi + have hfit : 2 ^ 29 < Usize.size := by + rw [Usize.size, Usize.numBits, UScalarTy.Usize_numBits_eq] + rcases System.Platform.numBits_eq with h | h <;> rw [h] <;> decide + simpa only [Nat.mod_eq_of_lt hfit] using hi + have hnz : i ≠ 0#usize := by + intro h + have := congrArg UScalar.val h + rw [hv] at this + change 2 ^ 29 = 0 at this + omega + simp only [core.num.nonzero.NonZero.new, cast_eq, hnz, + ↓reduceDIte, ↓reduceIte, bind_ok, WP.spec_ok] + exact hv + +theorem theoretical_max_align_spec : + layout.DstLayout.THEORETICAL_MAX_ALIGN + ⦃ a => a.val.val = 2 ^ (System.Platform.numBits - 1) ⦄ := by + unfold layout.DstLayout.THEORETICAL_MAX_ALIGN + step with pointer_width_spec as ⟨w, hw⟩ + have hb : 32 ≤ System.Platform.numBits := by + rcases System.Platform.numBits_eq with h | h <;> omega + step with Usize.sub_spec (show (1#usize).val ≤ w.val by simpa only [show (1#usize).val = 1 by simp, hw] using (show 1 ≤ System.Platform.numBits by omega)) as ⟨shift, hs, _⟩ + have hs' : shift.val = System.Platform.numBits - 1 := by + simpa only [hw, show (1#usize).val = 1 by simp] using hs + step with Usize.ShiftLeft_spec 1#usize shift (by rw [hs']; omega) as ⟨a, hav, _⟩ + have hv : a.val = 2 ^ (System.Platform.numBits - 1) := by + rw [hs', Nat.shiftLeft_eq, Nat.one_mul] at hav + have hfit : 2 ^ (System.Platform.numBits - 1) < Usize.size := by + rw [Usize.size, Usize.numBits, UScalarTy.Usize_numBits_eq] + exact (Nat.pow_lt_pow_iff_right (by decide : 1 < 2)).mpr (by omega) + simpa only [Nat.mod_eq_of_lt hfit] using hav + have hnz : a ≠ 0#usize := by + intro h + have := congrArg UScalar.val h + rw [hv] at this + change 2 ^ (System.Platform.numBits - 1) = 0 at this + have := Nat.two_pow_pos (System.Platform.numBits - 1) + omega + simp only [core.num.nonzero.NonZero.new, cast_eq, hnz, + ↓reduceDIte, ↓reduceIte, bind_ok, WP.spec_ok] + exact hv + +theorem packing_limit_spec (packed : Option NonZeroUsize) + (hp : ∀ a ∈ packed, a.val.val.isPowerOfTwo) : + (match packed with | none => layout.DstLayout.THEORETICAL_MAX_ALIGN | some a => Result.ok a) + ⦃ a => a.val.val = packingValue packed ∧ a.val.val.isPowerOfTwo ⦄ := by + cases packed with + | none => + step with theoretical_max_align_spec as ⟨a, ha⟩ + exact ⟨ha, ⟨_, ha⟩⟩ + | some a => + simp only [WP.spec_ok, packingValue, Option.map_some, Option.getD_some] + exact ⟨by trivial, hp a rfl⟩ + +-- Aeneas shares a generated matcher with the alignment encoder. The model +-- comparison checks that matcher; this proof deliberately names it. +set_option linter.auxLemma false in + +/- Append a field at its effective packed alignment, retaining the field's +complete inner layout. The canonical theorem then proves the concise +mathematical extension equation and successful decoding of the returned +record. +-/ +theorem extend_spec : + ∀ (self field : layout.DstLayout) (repr_packed : Option NonZeroUsize) (size : Usize), ∀ (hs : (self.size_info = .Sized size : Prop)), ∀ (hself : (self.align.val.val.isPowerOfTwo ∧ self.align.val.val ≤ 2 ^ 29 : Prop)), ∀ (hfield : (field.align.val.val.isPowerOfTwo ∧ field.align.val.val ≤ 2 ^ 29 : Prop)), ∀ (hpacked : (∀ a ∈ repr_packed, a.val.val.isPowerOfTwo ∧ a.val.val ≤ 2 ^ 29 : Prop)), ∀ (hfit : (match field.size_info with + | .Sized field_size => placement size field repr_packed + field_size.val ≤ Usize.max + | .SliceDst t => placement size field repr_packed + t.offset.val ≤ Usize.max ∧ + placement size field repr_packed + t.size_base.val ≤ Usize.max : Prop)), + @Zerocopy.layout.DstLayout.extend self field repr_packed ⦃ r => r.align.val.val = max self.align.val.val (fieldAlignment field repr_packed) ∧ + r.statically_shallow_unpadded = (self.statically_shallow_unpadded && + field.statically_shallow_unpadded && decide (size.val % fieldAlignment field repr_packed = 0)) ∧ + match field.size_info with + | .Sized field_size => ∃ s, r.size_info = .Sized s ∧ + s.val = placement size field repr_packed + field_size.val + | .SliceDst t => ∃ u, r.size_info = .SliceDst u ∧ + u.offset.val = placement size field repr_packed + t.offset.val ∧ + u.size_base.val = placement size field repr_packed + t.size_base.val ∧ + u.elem_size = t.elem_size ∧ + u.size_rounding_align_and_phase = t.size_rounding_align_and_phase ⦄ := by + intro self field packed size hs hself hfield hpacked hfit + unfold layout.DstLayout.extend + step with packing_limit_spec packed (fun a h => (hpacked a h).1) as ⟨limit, hl, hlpow⟩ + simp only [core.num.nonzero.NonZero.get, bind_ok] + step as ⟨b, hb⟩ + have hbt : b = true := by + have hb' : (b = true) = True := by simpa only [hlpow] using hb + exact Eq.mpr hb' trivial + simp only [massert, hbt, if_true, bind_ok] + step with current_max_align_spec as ⟨maximum, hmaximum⟩ + have hsa : self.align.val ≤ maximum.val := (UScalar.le_equiv _ _).mpr (by omega) + have hfa : field.align.val ≤ maximum.val := (UScalar.le_equiv _ _).mpr (by omega) + simp only [hsa, hfa, if_true, bind_ok] + -- State the match directly. Aeneas may assign its shared matcher to a + -- different declaration when extraction gains another caller. + have hpackcheck : (match (generalizing := false) packed with + | none => Result.ok none + | some a => do + if a.val ≤ maximum.val then Result.ok () else Result.fail .assertionFailure + Result.ok packed) = Result.ok packed := by + cases packed with + | none => rfl + | some a => + have ha : a.val ≤ maximum.val := (UScalar.le_equiv _ _).mpr (by + have := (hpacked a rfl).2 + omega) + simp only [ha, if_true, bind_ok] + -- Convert the initial bind to the same ordinary match before rewriting. + -- The continuation and postcondition are preserved by the placeholders. + change (Aeneas.Std.bind + (match (generalizing := false) packed with + | none => Result.ok none + | some a => do + if a.val ≤ maximum.val then Result.ok () else Result.fail .assertionFailure + Result.ok packed) _) ⦃ _ ⦄ + rw [hpackcheck] + simp only [bind_ok] + step with min_spec field.align limit as ⟨fa, hmin, hchoice, _, _⟩ + have hfp : fa.val.val.isPowerOfTwo := by + rcases hchoice with h | h + · simpa only [h] using hfield.1 + · simpa only [h] using hlpow + have hfv : fa.val.val = fieldAlignment field packed := by + rw [hmin, Arithmetic.coe_min, hl] + rfl + step with max_spec self.align fa as ⟨align, hmax, _, _, _⟩ + have halign : align.val.val = max self.align.val.val (fieldAlignment field packed) := by + rw [hmax, Arithmetic.coe_max, hfv] + rw [hs] + step with Zerocopy.Proofs.Raw.padding_lt_alignment size fa hfp as ⟨pad, _, hpad, _, _, hzero⟩ + have ho : size.val + pad.val = placement size field packed := by + rw [hpad, hfv] + rfl + have hzero' : (pad = 0#usize) = (size.val % fieldAlignment field packed = 0) := by + apply propext + simpa only [UScalar.eq_equiv, show (0#usize).val = 0 by simp, hfv] using hzero + step as ⟨checked, hsum⟩ + cases checked with + | none => + simp only [] at hsum + cases hf : field.size_info <;> simp only [hf] at hfit <;> omega + | some offset => + simp only [] at hsum + have hoff : offset.val = placement size field packed := by omega + cases hf : field.size_info with + | Sized field_size => + simp only [hf] at hfit + step as ⟨checked, hsized⟩ + cases checked with + | none => simp only [] at hsized; omega + | some total => + simp only [] at hsized + simp only [] + cases self.statically_shallow_unpadded <;> cases field.statically_shallow_unpadded <;> + simp only [Bool.false_eq_true, Bool.false_and, Bool.true_and, + if_false, if_true, WP.spec_ok, hzero'] + all_goals + exact ⟨halign, by trivial, total, by trivial, by omega⟩ + | SliceDst tail => + simp only [hf] at hfit + step as ⟨checked, hoffset⟩ + cases checked with + | none => simp only [] at hoffset; omega + | some physical => + simp only [] at hoffset + simp only [] + step as ⟨checked, hbase⟩ + cases checked with + | none => simp only [] at hbase; omega + | some base => + simp only [] at hbase + simp only [] + cases self.statically_shallow_unpadded <;> cases field.statically_shallow_unpadded <;> + simp only [Bool.false_eq_true, Bool.false_and, Bool.true_and, + if_false, if_true, WP.spec_ok, hzero'] + all_goals + exact ⟨halign, by trivial, { tail with offset := physical, size_base := base }, + by trivial, by dsimp only; omega, by dsimp only; omega, rfl, rfl⟩ + +theorem power_dvd_of_le (a b : Nat) (ha : a.isPowerOfTwo) (hb : b.isPowerOfTwo) + (hle : a ≤ b) : a ∣ b := by + obtain ⟨i, hi⟩ := ha + obtain ⟨j, hj⟩ := hb + rw [hi, hj] at hle ⊢ + exact Nat.pow_dvd_pow 2 ((Nat.pow_le_pow_iff_right (by decide : 1 < 2)).mp hle) + +/- Lift detailed raw extension facts to the independent fragment operation. This +supplies the constructor loop's mathematical state transition. +-/ +theorem extend_value_spec (self field : layout.DstLayout) (packed : Option NonZeroUsize) + (hself : alignmentDomain self.align.val.val) + (hfield : alignmentDomain field.align.val.val) + (hpacked : ∀ a ∈ packed, alignmentDomain a.val.val) + (hcanonical : canonicalLayout field) + (hfit : (layoutValue self).extendFits (layoutValue field) (packingValue packed) Usize.max) : + layout.DstLayout.extend self field packed + ⦃ r => layoutValue r = (layoutValue self).extend (layoutValue field) (packingValue packed) ∧ canonicalLayout r ⦄ := by + cases hs : self.size_info with + | SliceDst tail => simp [layoutValue, hs, LayoutMath.LayoutValue.extendFits] at hfit + | Sized size => + have hf : match field.size_info with + | .Sized s => placement size field packed + s.val ≤ Usize.max + | .SliceDst t => placement size field packed + t.offset.val ≤ Usize.max ∧ + placement size field packed + t.size_base.val ≤ Usize.max := by + cases hfs : field.size_info <;> + simpa only [layoutValue, hs, hfs, LayoutMath.LayoutValue.extendFits, + placement, fieldAlignment, trailingFormula, byteFormula] using hfit + apply WP.spec_mono (extend_spec self field packed size hs hself hfield hpacked hf) + rintro r ⟨ha, hu, hr⟩ + cases hfs : field.size_info with + | Sized s => + simp only [hfs] at hr + obtain ⟨bytes, hb, hv⟩ := hr + simp only [layoutValue, hb, hs, hfs, LayoutMath.LayoutValue.extend, + canonicalLayout, ha, hu, hv, placement, fieldAlignment] + exact ⟨rfl, trivial⟩ + | SliceDst t => + simp only [hfs] at hr + simp only [canonicalLayout, hfs] at hcanonical + obtain ⟨u, hsi, ho, hb, he, hc⟩ := hr + simp only [layoutValue, hsi, hs, hfs, LayoutMath.LayoutValue.extend, + canonicalLayout, ha, hu, trailingFormula, byteFormula, ho, hb, he, hc, + placement, fieldAlignment] + exact ⟨rfl, hcanonical⟩ + +attribute [step] extend_value_spec + +/- Lift detailed raw padding facts to the fragment operation used after the +loop. +-/ +theorem pad_value_spec (self : layout.DstLayout) + (ha : self.align.val.val.isPowerOfTwo) + (hc : canonicalLayout self) + (hf : (layoutValue self).padFits Usize.max) : + layout.DstLayout.pad_to_align self + ⦃ r => layoutValue r = (layoutValue self).pad ∧ canonicalLayout r ⦄ := by + have hfit : match self.size_info with + | .Sized s => LayoutMath.roundUp s.val self.align.val.val ≤ Usize.max + | .SliceDst t => 0 < t.size_rounding_align_and_phase._0.val.val ∧ + (if (trailingFormula t).align < self.align.val.val then + LayoutMath.roundUp t.size_base.val (trailingFormula t).align + + (trailingFormula t).phase ≤ Usize.max + else LayoutMath.roundUp t.size_base.val self.align.val.val ≤ Usize.max) := by + cases hs : self.size_info with + | Sized s => simpa only [layoutValue, hs, LayoutMath.LayoutValue.padFits] using hf + | SliceDst t => + simp only [canonicalLayout, hs] at hc + simp only [] + refine ⟨hc, ?_⟩ + simpa only [layoutValue, hs, LayoutMath.LayoutValue.padFits, + trailingFormula, byteFormula] using hf + apply WP.spec_mono (pad_to_align_spec self ha hfit) + rintro r ⟨hcanonical, hr, hp⟩ + refine ⟨?_, hcanonical⟩ + cases hs : self.size_info with + | Sized s => + simp only [hs] at hp + obtain ⟨p, hsi, hv, hu⟩ := hp + simp only [layoutValue, hsi, hs, LayoutMath.LayoutValue.pad, hr, hv, hu] + | SliceDst t => + simp only [hs] at hp + obtain ⟨u, hsi, hv, hu⟩ := hp + simp only [layoutValue, hsi, hs, LayoutMath.LayoutValue.pad, hr, hv, hu] + +attribute [step] pad_value_spec + end Zerocopy.Proofs.Raw namespace Zerocopy.Proofs @@ -835,6 +1236,103 @@ theorem new_zst_spec : Zerocopy.Specs.new_zst_spec := by | some a => simpa only [Option.getD_some, and_true] using Nat.pos_of_isPowerOfTwo (hp a rfl) register_spec_step new_zst_spec +/- Append a field at its effective packed alignment, retaining the field's +complete inner layout. The canonical theorem then proves the concise +mathematical extension equation and successful decoding of the returned +record. +-/ +theorem extend_spec : Zerocopy.Specs.extend_spec := by + intro self field packed value hvalue fieldValue hfieldValue packing hpacking + hself hfield hpacked hfit + have hvself := (layout_decoder_admitted_iff self).mp ⟨value, hvalue⟩ + have hvfield := (layout_decoder_admitted_iff field).mp ⟨fieldValue, hfieldValue⟩ + have hview := layoutValue_decode self value hvalue + have hfview := layoutValue_decode field fieldValue hfieldValue + have hpview := packingValue_decode packed packing hpacking + have halign : value.align.value = self.align.val.val := + congrArg LayoutMath.LayoutValue.align hview + have hfalign : fieldValue.align.value = field.align.val.val := + congrArg LayoutMath.LayoutValue.align hfview + have rawFits : (layoutValue self).extendFits (layoutValue field) + (packingValue packed) Usize.max := by + simpa only [hview, hfview, hpview] using hfit + have rawPacked : ∀ a ∈ packed, alignmentDomain a.val.val := + (packing_alignment_decode packed packing hpacking).mp hpacked + have canonical : canonicalLayout field := by + cases hs : field.size_info with + | Sized _ => simp only [canonicalLayout, hs] + | SliceDst _ => + simpa only [sizeInfoValid, trailingValid, encodingValid, + scalar_valid_iff, true_and, canonicalLayout, hs] using hvfield.2 + apply WP.spec_mono (Raw.extend_value_spec self field packed + (by simpa only [alignmentDomain, halign] using hself) + (by simpa only [alignmentDomain, hfalign] using hfield) rawPacked canonical rawFits) + rintro result ⟨facts, hc⟩ + have valid : layoutValid result := by + refine ⟨?_, ?_⟩ + · cases hs : self.size_info with + | SliceDst _ => simp only [layoutValue, hs, LayoutMath.LayoutValue.extendFits] at rawFits + | Sized _ => + have ha := congrArg LayoutMath.LayoutValue.align facts + simp only [layoutValue, hs, LayoutMath.LayoutValue.extend] at ha + have positive := hvself.1 + rw [ha] + omega + · cases hs : result.size_info with + | Sized _ => trivial + | SliceDst _ => + simpa only [sizeInfoValid, trailingValid, encodingValid, canonicalLayout, + scalar_valid_iff, true_and, hs] using hc + apply decoded_view_post layout.DstLayout.aeneasModel layoutValue + ModelViews.layoutValue layoutValue_decode + (fun r => r = (ModelViews.layoutValue value).extend + (ModelViews.layoutValue fieldValue) (ModelViews.packingValue packing)) result + ((layout_decoder_admitted_iff result).mpr valid) + simpa only [hview, hfview, hpview] using facts +register_spec_step extend_spec + +/- Preserve the inner complete-size calculation while adding outer padding. The +proof separately tracks physical offset, normalized base/phase, alignment, +and the unpadded flag; equal total sizes alone would be insufficient. +-/ +theorem pad_to_align_spec : Zerocopy.Specs.pad_to_align_spec := by + intro self value hvalue ha hfit + have hv := (layout_decoder_admitted_iff self).mp ⟨value, hvalue⟩ + have hview := layoutValue_decode self value hvalue + have halign : value.align.value = self.align.val.val := + congrArg LayoutMath.LayoutValue.align hview + have fits : match self.size_info with + | .Sized bytes => LayoutMath.roundUp bytes.val self.align.val.val ≤ Usize.max + | .SliceDst tail => 0 < tail.size_rounding_align_and_phase._0.val.val ∧ + (if (trailingFormula tail).align < self.align.val.val then + LayoutMath.roundUp tail.size_base.val (trailingFormula tail).align + + (trailingFormula tail).phase ≤ Usize.max + else LayoutMath.roundUp tail.size_base.val self.align.val.val ≤ Usize.max) := by + rw [hview] at hfit + cases hs : self.size_info with + | Sized _ => simpa only [LayoutMath.LayoutValue.padFits, layoutValue, hs] using hfit + | SliceDst tail => + simp only [layoutValid, sizeInfoValid, trailingValid, encodingValid, scalar_valid_iff, + true_and, hs] at hv + exact ⟨hv.2, by simpa only [LayoutMath.LayoutValue.padFits, layoutValue, hs, + trailingFormula, byteFormula] using hfit⟩ + apply WP.spec_mono (Raw.pad_to_align_spec self (by simpa only [halign] using ha) fits) + rintro result ⟨hc, facts⟩ + have hrvalid : layoutValid result := by + refine ⟨?_, ?_⟩ + · simpa only [facts.1] using hv.1 + · cases hs : result.size_info with + | Sized _ => trivial + | SliceDst _ => simpa only [sizeInfoValid, trailingValid, encodingValid, + canonicalLayout, scalar_valid_iff, true_and, hs] using hc + apply decoded_view_post layout.DstLayout.aeneasModel layoutValue + ModelViews.layoutValue layoutValue_decode + (fun r => r = (ModelViews.layoutValue value).pad) result + ((layout_decoder_admitted_iff result).mpr hrvalid) + rw [hview] + exact (layout_pad_iff self result).mpr facts +register_spec_step pad_to_align_spec + /-- An arbitrary proof of the compact mathematical clause implies the separately maintained exact optional-size and overflow obligation. -/ @[contract_simps] theorem size_for_elems_spec_implies_required @@ -853,4 +1351,31 @@ maintained exact optional-size and overflow obligation. -/ rw [optionalSize_decode result decoded hd, hformula, unsignedWord_value] at hsize exact hsize +/-- The compact padding clause implies the independently stated admission, +alignment, size-variant, exact payload and unpadded-flag guarantees. -/ +@[contract_simps] theorem pad_to_align_spec_implies_required + (self : layout.DstLayout) (run : Result layout.DstLayout) + (provided : Zerocopy.Specs.pad_to_align_spec_contract self run) : + Zerocopy.Obligations.pad_to_align_spec_contract self run := by + intro valid power fits + obtain ⟨value, hvalue⟩ := (layout_decoder_admitted_iff self).mpr valid + have hview := layoutValue_decode self value hvalue + have halign : value.align.value = self.align.val.val := + congrArg LayoutMath.LayoutValue.align hview + have hfit : (ModelViews.layoutValue value).padFits Usize.max := by + rw [hview] + cases hs : self.size_info with + | Sized _ => simpa only [LayoutMath.LayoutValue.padFits, layoutValue, hs] using fits + | SliceDst _ => + simp only [hs] at fits + simpa only [LayoutMath.LayoutValue.padFits, layoutValue, hs, + trailingFormula, byteFormula] using fits.2 + apply WP.spec_mono (provided value hvalue + (by simpa only [halign] using power) hfit) + rintro result ⟨decoded, hd, heq⟩ + refine ⟨(layout_decoder_admitted_iff result).mp ⟨decoded, hd⟩, ?_⟩ + change ModelViews.layoutValue decoded = (ModelViews.layoutValue value).pad at heq + rw [layoutValue_decode result decoded hd, hview] at heq + exact (layout_pad_iff self result).mp heq + end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Proofs/CompositionChecks.lean b/verification/aeneas/lean/Proofs/CompositionChecks.lean new file mode 100644 index 0000000000..c1a3d6a4fa --- /dev/null +++ b/verification/aeneas/lean/Proofs/CompositionChecks.lean @@ -0,0 +1,104 @@ +/- 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 CompositionReference +@[expose] public section + +/-! +The roots below prove successful execution of ordinary Rust assertion harnesses. +The checked independent reference supplies the precise production arithmetic +domain. The existing raw operation proofs produce the actual layout, and the +reference matcher checks every stored observation before the assertion succeeds. +-/ +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw +set_option linter.unusedSimpArgs false +open Zerocopy.CompositionReference + +theorem composition_pad_checks (runtime_layout : layout.DstLayout) (reference : ReferenceLayout) : + layout.composition_checks.check_pad runtime_layout reference ⦃ _ => True ⦄ := by + unfold layout.composition_checks.check_pad + step with composition_matches_spec runtime_layout reference as ⟨matching, hm⟩ + split + · rename_i yes + have matched := hm.mp yes + obtain ⟨validity, canonical, view⟩ := matches_value runtime_layout reference matched + have align_view := congrArg LayoutMath.LayoutValue.align view + change runtime_layout.align.val.val = reference.align.val at align_view + step with composition_reference_pad_spec reference as ⟨expected, he⟩ + cases expected with + | none => simp + | some expected => + obtain ⟨power, fits, expected_view, expected_validity⟩ := he expected rfl + step with pad_value_spec runtime_layout + (by simpa only [align_view] using power) canonical (by simpa only [view] using fits) + as ⟨actual, actual_view, actual_canonical⟩ + have same : layoutValue actual = value expected := by + rw [actual_view, view, expected_view] + have matched_result := matches_of_value actual expected actual_canonical expected_validity same + step with composition_matches_spec actual expected as ⟨checked, hc⟩ + have yes : checked = true := hc.mpr matched_result + simp [yes, massert] + · simp + +theorem composition_extend_checks (preceding field : layout.DstLayout) + (packed : Option NonZeroUsize) (preceding_reference field_reference : ReferenceLayout) : + layout.composition_checks.check_extend preceding field packed preceding_reference field_reference + ⦃ _ => True ⦄ := by + unfold layout.composition_checks.check_extend + step with composition_matches_spec preceding preceding_reference as ⟨preceding_matches, hp⟩ + split + · rename_i py + obtain ⟨preceding_valid, _, preceding_view⟩ := matches_value preceding preceding_reference (hp.mp py) + have preceding_align := congrArg LayoutMath.LayoutValue.align preceding_view + change preceding.align.val.val = preceding_reference.align.val at preceding_align + step with composition_matches_spec field field_reference as ⟨field_matches, hf⟩ + split + · rename_i fy + obtain ⟨field_valid, field_canonical, field_view⟩ := matches_value field field_reference (hf.mp fy) + have field_align := congrArg LayoutMath.LayoutValue.align field_view + change field.align.val.val = field_reference.align.val at field_align + step with composition_reference_extend_spec preceding_reference field_reference packed as ⟨expected, he⟩ + cases expected with + | none => simp + | some expected => + obtain ⟨preceding_domain, field_domain, packed_domain, fits, expected_view, validity⟩ := he expected rfl + step with extend_value_spec preceding field packed + (by simpa only [preceding_align] using preceding_domain) + (by simpa only [field_align] using field_domain) packed_domain field_canonical + (by simpa only [preceding_view, field_view] using fits) + as ⟨actual, actual_view, actual_canonical⟩ + have same : layoutValue actual = value expected := by + rw [actual_view, preceding_view, field_view, expected_view] + have matched_result := matches_of_value actual expected actual_canonical (validity field_valid) same + step with composition_matches_spec actual expected as ⟨checked, hc⟩ + have yes : checked = true := hc.mpr matched_result + simp [yes, massert] + · simp + · simp + +end Zerocopy.Proofs.Raw + +namespace Zerocopy.Proofs + +theorem composition_pad_checks_spec : Specs.composition_pad_checks_spec := by + intro runtime_layout reference + repeat intro + apply WP.spec_mono (Raw.composition_pad_checks runtime_layout reference) + intro _ _ + exact ⟨(), rfl, trivial⟩ + +theorem composition_extend_checks_spec : Specs.composition_extend_checks_spec := by + intro preceding field packed preceding_reference field_reference + repeat intro + apply WP.spec_mono (Raw.composition_extend_checks preceding field packed preceding_reference field_reference) + intro _ _ + exact ⟨(), rfl, trivial⟩ + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RequiredModelContracts.lean b/verification/aeneas/lean/RequiredModelContracts.lean index c6fd3536fd..efb0a1c6e8 100644 --- a/verification/aeneas/lean/RequiredModelContracts.lean +++ b/verification/aeneas/lean/RequiredModelContracts.lean @@ -9,6 +9,7 @@ those terms. -/ module public import RequiredModelContracts.Util public import RepresentationLaws +public import ModelProjectionLaws @[expose] public section /-! @@ -82,6 +83,53 @@ attribute [contract_simps] encoding_decoder_admitted_iff trailing_decoder_admitt exact ⟨Nat.pos_of_isPowerOfTwo value.align_pow2, value.align_pow2, value.phase_lt, hraw.symm, hcanonical.1, hcanonical.2⟩ +@[contract_simps] theorem required_extend (self field : layout.DstLayout) + (packed : Option NonZeroUsize) (run : Result layout.DstLayout) + (provided : Specs.extend_spec_contract self field packed run) : + Obligations.extend_spec_contract self field packed run := by + intro size selfValid fieldValid packedValid hs ha hf hp fits + obtain ⟨selfModel, selfDecoded⟩ := (layout_decoder_admitted_iff self).mpr selfValid + obtain ⟨fieldModel, fieldDecoded⟩ := (layout_decoder_admitted_iff field).mpr fieldValid + have packedAccepted : isValid packed := by simpa using packedValid + obtain ⟨packedModel, packedDecoded⟩ := packedAccepted + have selfView := layoutValue_decode self selfModel selfDecoded + have fieldView := layoutValue_decode field fieldModel fieldDecoded + have packedView := packingValue_decode packed packedModel packedDecoded + have selfAlign : selfModel.align.value = self.align.val.val := + congrArg LayoutMath.LayoutValue.align selfView + have fieldAlign : fieldModel.align.value = field.align.val.val := + congrArg LayoutMath.LayoutValue.align fieldView + have modelPacked : ∀ a ∈ packedModel, alignmentDomain a.value := + (packing_alignment_decode packed packedModel packedDecoded).mpr hp + have modelFits : (ModelViews.layoutValue selfModel).extendFits + (ModelViews.layoutValue fieldModel) (ModelViews.packingValue packedModel) Usize.max := by + rw [selfView, fieldView, packedView] + exact (layout_extendFits_iff self field packed size hs).mpr fits + have fieldCanonical : canonicalLayout field := by + cases info : field.size_info with + | Sized _ => simp only [canonicalLayout, info] + | SliceDst _ => + simpa only [sizeInfoValid, trailingValid, encodingValid, + scalar_valid_iff, true_and, canonicalLayout, info] using fieldValid.2 + apply WP.spec_mono (provided selfModel selfDecoded fieldModel fieldDecoded + packedModel packedDecoded (by simpa only [selfAlign] using ha) + (by simpa only [fieldAlign] using hf) modelPacked modelFits) + rintro result ⟨value, decoded, facts⟩ + have valid := (layout_decoder_admitted_iff result).mp ⟨value, decoded⟩ + have resultCanonical : canonicalLayout result := by + cases info : result.size_info with + | Sized _ => simp only [canonicalLayout, info] + | SliceDst _ => + simpa only [sizeInfoValid, trailingValid, encodingValid, + scalar_valid_iff, true_and, canonicalLayout, info] using valid.2 + refine ⟨valid, ?_⟩ + change ModelViews.layoutValue value = + (ModelViews.layoutValue selfModel).extend + (ModelViews.layoutValue fieldModel) (ModelViews.packingValue packedModel) at facts + rw [layoutValue_decode result value decoded, selfView, fieldView, packedView] at facts + exact (layout_extend_iff self field result packed size hs + fieldCanonical resultCanonical).mp facts + @[contract_simps] theorem required_try_nonzero (self : layout.SizeInfo Usize) (run : Result (Option (layout.SizeInfo NonZeroUsize))) (provided : Specs.try_nonzero_spec_contract self run) : diff --git a/verification/aeneas/lean/RequiredModelContracts/CompositionChecks.lean b/verification/aeneas/lean/RequiredModelContracts/CompositionChecks.lean new file mode 100644 index 0000000000..922c105830 --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/CompositionChecks.lean @@ -0,0 +1,70 @@ +/- 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 RequiredModelContracts +public import Obligations.CompositionChecks +@[expose] public section + +/-! +These adapters recover the independent successful-execution expectations from +an arbitrary supplied specification outcome. Every numeric reference value +decodes; its runtime admission guard belongs to the Rust harness itself. +-/ +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +/- Structural decoding imposes no hidden restriction on the numeric witnesses. -/ +theorem composition_reference_admitted (reference : layout.composition_checks.ReferenceLayout) : + isValid reference := by + cases reference with + | mk align size unpadded => + cases size with + | Fixed bytes => + exact ⟨⟨unsignedWord align, .Fixed (unsignedWord bytes), unpadded⟩, rfl⟩ + | Tail tail => + exact ⟨⟨unsignedWord align, + .Tail ⟨unsignedWord tail.offset, unsignedWord tail.elem_size, unsignedWord tail.base, + unsignedWord tail.round_align, unsignedWord tail.phase⟩, unpadded⟩, rfl⟩ + +theorem composition_options_admitted (words : Option NonZeroUsize) + (positive : ∀ a ∈ words, 0 < a.val.val) : isValid words := by + rw [option_valid_iff] + intro a member + exact (nonzero_valid_iff a).mpr (positive a member) + +@[contract_simps] theorem required_composition_pad_checks (runtime_layout : layout.DstLayout) + (reference : layout.composition_checks.ReferenceLayout) (run : Result Unit) + (provided : Specs.composition_pad_checks_spec_contract runtime_layout reference run) : + Obligations.composition_pad_checks_spec_contract runtime_layout reference run := by + intro validity + obtain ⟨runtime_value, runtime_decode⟩ := (layout_decoder_admitted_iff runtime_layout).mpr validity + obtain ⟨reference_value, reference_decode⟩ := composition_reference_admitted reference + apply WP.spec_mono (provided runtime_value runtime_decode reference_value reference_decode) + intro _ _ + trivial + +@[contract_simps] theorem required_composition_extend_checks (preceding field : layout.DstLayout) + (packed : Option NonZeroUsize) + (preceding_reference field_reference : layout.composition_checks.ReferenceLayout) + (run : Result Unit) (provided : Specs.composition_extend_checks_spec_contract preceding field packed + preceding_reference field_reference run) : + Obligations.composition_extend_checks_spec_contract preceding field packed + preceding_reference field_reference run := by + intro preceding_valid field_valid packed_positive + obtain ⟨preceding_value, preceding_decode⟩ := (layout_decoder_admitted_iff preceding).mpr preceding_valid + obtain ⟨field_value, field_decode⟩ := (layout_decoder_admitted_iff field).mpr field_valid + obtain ⟨packed_value, packed_decode⟩ := composition_options_admitted packed packed_positive + obtain ⟨preceding_reference_value, preceding_reference_decode⟩ := composition_reference_admitted preceding_reference + obtain ⟨field_reference_value, field_reference_decode⟩ := composition_reference_admitted field_reference + apply WP.spec_mono (provided preceding_value preceding_decode field_value field_decode packed_value packed_decode + preceding_reference_value preceding_reference_decode field_reference_value field_reference_decode) + intro _ _ + trivial + +end Zerocopy.Proofs diff --git a/zerocopy/src/layout/composition_checks.rs b/zerocopy/src/layout/composition_checks.rs new file mode 100644 index 0000000000..be7f3184ab --- /dev/null +++ b/zerocopy/src/layout/composition_checks.rs @@ -0,0 +1,233 @@ +// SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT +// +// Copyright 2026 The Fuchsia Authors +// +// Licensed under the 2-Clause BSD 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. + +//! A separate numeric reference for layout extension and final padding. +//! +//! The reference keeps alignment and phase as separate integers. It uses +//! remainders and checked arithmetic, and never calls the production layout, +//! rounding, or padding helpers. The assertions compare every observable field, +//! including physical slice offset and the compressed size expression. +//! +//! Runtime witnesses avoid decoding a production rounding word in the reference. +//! Every nonzero rounding word has such a witness: its greatest power of two is +//! the alignment, and subtracting that alignment gives a smaller phase. The +//! assertions quantify over arbitrary witnesses and check their correspondence +//! before calling the production operation. + +// Explicit matches expose overflow paths without depending on Option's Try +// trait, which the pinned extraction does not model. +#![allow(clippy::arithmetic_side_effects, clippy::indexing_slicing, clippy::question_mark)] + +use super::{DstLayout, NonZeroUsize, SizeInfo}; + +#[derive(Copy, Clone)] +struct ReferenceTail { + offset: usize, + elem_size: usize, + base: usize, + round_align: usize, + phase: usize, +} + +#[derive(Copy, Clone)] +#[allow(variant_size_differences)] +enum ReferenceSize { + Fixed(usize), + Tail(ReferenceTail), +} + +#[derive(Copy, Clone)] +struct ReferenceLayout { + align: usize, + size: ReferenceSize, + unpadded: bool, +} + +/// The exact numeric observation compared with the stored representation. +/// A phase must be smaller than its power-of-two alignment; the checked sum +/// prevents the witness relation from hiding a machine-word overflow. +fn matches_reference(runtime_layout: DstLayout, reference: ReferenceLayout) -> bool { + runtime_layout.align.get() == reference.align + && runtime_layout.statically_shallow_unpadded == reference.unpadded + && match (runtime_layout.size_info, reference.size) { + (SizeInfo::Sized { size }, ReferenceSize::Fixed(expected)) => size == expected, + (SizeInfo::SliceDst(actual), ReferenceSize::Tail(expected)) => { + expected.round_align.is_power_of_two() + && expected.phase < expected.round_align + && actual.offset == expected.offset + && actual.elem_size == expected.elem_size + && actual.size_base == expected.base + && match expected.round_align.checked_add(expected.phase) { + Some(encoded) => actual.size_rounding_align_and_phase.0.get() == encoded, + None => false, + } + } + _ => false, + } +} + +/// Round up by the least padding that makes the result divisible by alignment. +fn reference_round_up(bytes: usize, align: usize) -> Option { + if align == 0 { + return None; + } + let padding = (align - bytes % align) % align; + bytes.checked_add(padding) +} + +/// Mirrors the production debug-assertion domain without imposing a size bound. +fn extension_alignment(align: usize) -> bool { + align.is_power_of_two() && align <= 1 << 29 +} + +/// Append a field, retaining its complete inner size expression. +/// `None` means an alignment check failed, the preceding layout was unsized, +/// or an intermediate required by production overflowed. There is no extra +/// headroom or `isize` restriction. +fn reference_extend( + preceding: ReferenceLayout, + field: ReferenceLayout, + packed: Option, +) -> Option { + if !extension_alignment(preceding.align) || !extension_alignment(field.align) { + return None; + } + let field_align = match packed { + Some(cap) => { + if !extension_alignment(cap.get()) { + return None; + } + if field.align < cap.get() { + field.align + } else { + cap.get() + } + } + None => field.align, + }; + reference_extend_at(preceding, field, field_align) +} + +// Keep placement separate from alignment admission so the reference has one +// arithmetic path for packed and unpacked records. +fn reference_extend_at( + preceding: ReferenceLayout, + field: ReferenceLayout, + field_align: usize, +) -> Option { + let bytes = match preceding.size { + ReferenceSize::Fixed(bytes) => bytes, + ReferenceSize::Tail(_) => return None, + }; + let offset = match reference_round_up(bytes, field_align) { + Some(offset) => offset, + None => return None, + }; + let size = match field.size { + ReferenceSize::Fixed(bytes) => match offset.checked_add(bytes) { + Some(size) => ReferenceSize::Fixed(size), + None => return None, + }, + ReferenceSize::Tail(tail) => { + let slice_offset = match offset.checked_add(tail.offset) { + Some(offset) => offset, + None => return None, + }; + let base = match offset.checked_add(tail.base) { + Some(base) => base, + None => return None, + }; + ReferenceSize::Tail(ReferenceTail { offset: slice_offset, base, ..tail }) + } + }; + Some(ReferenceLayout { + align: if preceding.align > field_align { preceding.align } else { field_align }, + size, + unpadded: preceding.unpadded & field.unpadded & (offset == bytes), + }) +} + +/// Add final padding without discarding an inner DST's rounding. +fn reference_pad(reference: ReferenceLayout) -> Option { + if !reference.align.is_power_of_two() { + return None; + } + let (size, no_static_padding) = match reference.size { + ReferenceSize::Fixed(bytes) => match reference_round_up(bytes, reference.align) { + Some(rounded) => (ReferenceSize::Fixed(rounded), rounded == bytes), + None => return None, + }, + ReferenceSize::Tail(tail) => { + if !tail.round_align.is_power_of_two() || tail.phase >= tail.round_align { + return None; + } + let (base, round_align, phase) = if tail.round_align >= reference.align { + let base = match reference_round_up(tail.base, reference.align) { + Some(base) => base, + None => return None, + }; + (base, tail.round_align, tail.phase) + } else { + let rounded_base = match reference_round_up(tail.base, tail.round_align) { + Some(base) => base, + None => return None, + }; + let fixed = match rounded_base.checked_add(tail.phase) { + Some(fixed) => fixed, + None => return None, + }; + let phase = fixed % reference.align; + (fixed - phase, reference.align, phase) + }; + (ReferenceSize::Tail(ReferenceTail { base, round_align, phase, ..tail }), true) + } + }; + Some(ReferenceLayout { size, unpadded: reference.unpadded & no_static_padding, ..reference }) +} + +/// Check extension against every stored reference observation on the exact +/// checked-arithmetic domain where the production operation can succeed. +/// +/// ```aeneas +/// spec composition_extend_checks_spec +/// ensures _ => True +/// ``` +fn check_extend( + preceding: DstLayout, + field: DstLayout, + packed: Option, + preceding_reference: ReferenceLayout, + field_reference: ReferenceLayout, +) { + if matches_reference(preceding, preceding_reference) + && matches_reference(field, field_reference) + { + if let Some(expected) = reference_extend(preceding_reference, field_reference, packed) { + let actual = preceding.extend(field, packed); + assert!(matches_reference(actual, expected)); + } + } +} + +/// Check trailing padding, including both relative-alignment branches for DSTs. +/// +/// ```aeneas +/// spec composition_pad_checks_spec +/// ensures _ => True +/// ``` +fn check_pad(runtime_layout: DstLayout, reference: ReferenceLayout) { + if matches_reference(runtime_layout, reference) { + if let Some(expected) = reference_pad(reference) { + let actual = runtime_layout.pad_to_align(); + assert!(matches_reference(actual, expected)); + } + } +} diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs index ce7a76ce7c..a6160edee2 100644 --- a/zerocopy/src/layout/mod.rs +++ b/zerocopy/src/layout/mod.rs @@ -18,6 +18,9 @@ mod primitive_checks; #[allow(dead_code)] mod tail_checks; +#[allow(dead_code)] +mod composition_checks; + use core::{mem, num::NonZeroUsize}; use crate::util; @@ -1296,6 +1299,18 @@ impl DstLayout { #[cfg_attr(kani, kani::ensures(|&result| { Some(result) == proofs::extended_layout(self, field, repr_packed) }))] + /// + /// ```aeneas + /// spec extend_spec + /// requires hself : self.align.value.isPowerOfTwo ∧ self.align.value ≤ 2 ^ 29 + /// requires hfield : field.align.value.isPowerOfTwo ∧ field.align.value ≤ 2 ^ 29 + /// requires hpacked : ∀ a ∈ repr_packed, a.value.isPowerOfTwo ∧ a.value ≤ 2 ^ 29 + /// requires hfit : (ModelViews.layoutValue self).extendFits + /// (ModelViews.layoutValue field) (ModelViews.packingValue repr_packed) Usize.max + /// ensures r => ModelViews.layoutValue r = + /// (ModelViews.layoutValue self).extend + /// (ModelViews.layoutValue field) (ModelViews.packingValue repr_packed) + /// ``` pub const fn extend(self, field: DstLayout, repr_packed: Option) -> Self { #[cfg(kani)] #[kani::proof_for_contract(DstLayout::extend)] @@ -1470,6 +1485,14 @@ impl DstLayout { #[inline] #[cfg_attr(kani, kani::requires(proofs::padded_layout(self).is_some()))] #[cfg_attr(kani, kani::ensures(|&result| Some(result) == proofs::padded_layout(self)))] + /// + /// ```aeneas + /// spec pad_to_align_spec + /// requires ha : (self.align : Nat).isPowerOfTwo + /// requires hfit : (ModelViews.layoutValue self).padFits Usize.max + /// ensures result => + /// ModelViews.layoutValue result = (ModelViews.layoutValue self).pad + /// ``` pub const fn pad_to_align(self) -> Self { #[cfg(kani)] #[kani::proof_for_contract(DstLayout::pad_to_align)]