From 1151d61bad558c0c21bbcf7263df78b5e5fec437 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Fri, 2 Oct 2026 10:54:19 -0400 Subject: [PATCH] Prove DstLayout padding and field extension Relate the production pad_to_align and extend methods to mathematical layout operations. Packing limits placement alignment while retaining the field's complete size, including its internal padding. Use mathematical clauses for the operation specs and prove that they retain the independent guarantees about alignment, normalized payload, physical fields and padding flags. Keep representation and fit conditions explicit. Add total Rust harnesses comparing every stored field and both padding branches with independent remainder-based checked arithmetic. The resulting proofs establish the conditional layout behavior without requiring review of intermediate Lean proof steps. gherrit-pr-id: Ggsdoapsrkoab2sezv6aidvmzy46fo7pu Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/README.md | 5 +- 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 + .../aeneas/lean/Proofs/CompositionChecks.lean | 104 +++ .../aeneas/lean/Proofs/Contracts.lean | 126 ++- .../aeneas/lean/Proofs/Raw/Composition.lean | 155 ++++ .../aeneas/lean/Proofs/Raw/Construction.lean | 99 +++ .../aeneas/lean/Proofs/Raw/Layout.lean | 178 ++++ .../aeneas/lean/Proofs/Raw/Trailing.lean | 7 + .../aeneas/lean/RequiredModelContracts.lean | 48 ++ .../CompositionChecks.lean | 70 ++ .../aeneas/projections/ModelShapes.lean | 6 + verification/aeneas/projections/Models.lean | 9 + verification/aeneas/projections/Specs.lean | 42 + zerocopy/src/layout/composition_checks.rs | 233 ++++++ zerocopy/src/layout/mod.rs | 23 + 21 files changed, 2593 insertions(+), 110 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/Proofs/Raw/Composition.lean create mode 100644 verification/aeneas/lean/Proofs/Raw/Construction.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 ad00a17773..b09e07e5b0 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -268,7 +268,7 @@ whole-program unsafe-code certification. ## 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. The current @@ -361,6 +361,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, for NonZero, positivity. They coerce to `Nat` or `Int` without unwrapping raw fields. Binding `let N : Nat := n` makes addition and remainder ordinary diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index 0a043cfe75..bb2d15bdca 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -650,36 +650,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 311:0-317: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 295:0-301: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 175:0-235: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 267:0-285: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 @@ -706,8 +1194,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 @@ -716,25 +1350,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 267:0-285: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) ← @@ -744,7 +1361,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) : @@ -772,24 +1389,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 175:0-235: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 @@ -811,7 +1412,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) @@ -835,7 +1436,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 @@ -860,7 +1461,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 @@ -877,7 +1478,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 : @@ -892,13 +1493,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 @@ -922,7 +1523,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 @@ -941,7 +1542,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 @@ -949,7 +1550,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 ← @@ -975,7 +1576,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 @@ -2895,46 +3496,6 @@ def core.cell.UnsafeCell.Insts.ZerocopyIntoBytes {T : Type} (IntoBytesInst : IntoBytesInst } -/-- [zerocopy::util::max]: - Source: 'src/util/mod.rs', lines 295:0-301: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 311:0-317: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::owned_transmute::to_bytes_native]: Source: 'src/util/owned_transmute.rs', lines 30:0-34:1 -/ def util.owned_transmute.to_bytes_native diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index 034e0b4350..cd19cd1994 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -177,14 +177,39 @@ structure byteorder.F64 (O : Type) where _0 : Array Std.U8 8#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 @@ -192,14 +217,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/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/Proofs/Contracts.lean b/verification/aeneas/lean/Proofs/Contracts.lean index e26c49d111..1e39b28417 100644 --- a/verification/aeneas/lean/Proofs/Contracts.lean +++ b/verification/aeneas/lean/Proofs/Contracts.lean @@ -8,7 +8,7 @@ those terms. -/ module public import Proofs.Raw.Trailing -public import Proofs.Raw.Layout +public import Proofs.Raw.Construction @[expose] public section open Aeneas Aeneas.Std @@ -263,6 +263,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 @@ -281,4 +378,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/Raw/Composition.lean b/verification/aeneas/lean/Proofs/Raw/Composition.lean new file mode 100644 index 0000000000..c82c2964da --- /dev/null +++ b/verification/aeneas/lean/Proofs/Raw/Composition.lean @@ -0,0 +1,155 @@ +/- 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.Raw.Layout +import all Mathlib.Data.Nat.Log +import all Init.Data.Nat.Power2.Basic +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw + +set_option linter.unusedVariables false +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⟩ + +end Zerocopy.Proofs.Raw diff --git a/verification/aeneas/lean/Proofs/Raw/Construction.lean b/verification/aeneas/lean/Proofs/Raw/Construction.lean new file mode 100644 index 0000000000..c84832cfae --- /dev/null +++ b/verification/aeneas/lean/Proofs/Raw/Construction.lean @@ -0,0 +1,99 @@ +/- 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.Raw.Composition +import all Mathlib.Data.Nat.Log +import all Init.Data.Nat.Power2.Basic +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw + +set_option linter.unusedVariables false +/- 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 diff --git a/verification/aeneas/lean/Proofs/Raw/Layout.lean b/verification/aeneas/lean/Proofs/Raw/Layout.lean index eaceac2fca..1567d1ae96 100644 --- a/verification/aeneas/lean/Proofs/Raw/Layout.lean +++ b/verification/aeneas/lean/Proofs/Raw/Layout.lean @@ -131,4 +131,182 @@ 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 + end Zerocopy.Proofs.Raw diff --git a/verification/aeneas/lean/Proofs/Raw/Trailing.lean b/verification/aeneas/lean/Proofs/Raw/Trailing.lean index 8ec9476d24..b325790be0 100644 --- a/verification/aeneas/lean/Proofs/Raw/Trailing.lean +++ b/verification/aeneas/lean/Proofs/Raw/Trailing.lean @@ -276,4 +276,11 @@ theorem size_for_elems_spec : p.val + self.offset.val + elems.val * self.elem_size.val by omega, hp, word_mod_of_le _ hfit] +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) + end Zerocopy.Proofs.Raw 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..e38dabb013 --- /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_nonzero_unsigned_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/verification/aeneas/projections/ModelShapes.lean b/verification/aeneas/projections/ModelShapes.lean index 987bf9d0ba..a350e0329e 100644 --- a/verification/aeneas/projections/ModelShapes.lean +++ b/verification/aeneas/projections/ModelShapes.lean @@ -44,6 +44,12 @@ derive_model_shape Zerocopy.byteorder.F32 with 1 type parameters derive_model_shape Zerocopy.byteorder.F64 with 1 type parameters +derive_model_shape Zerocopy.layout.composition_checks.ReferenceTail with 0 type parameters + +derive_model_shape Zerocopy.layout.composition_checks.ReferenceSize with 0 type parameters + +derive_model_shape Zerocopy.layout.composition_checks.ReferenceLayout with 0 type parameters + aeneas_model_shape Zerocopy.layout.RoundingAlignAndPhase with 0 type parameters begin model RoundingValue where align : Nat diff --git a/verification/aeneas/projections/Models.lean b/verification/aeneas/projections/Models.lean index 3c408a9a59..e1982fca2c 100644 --- a/verification/aeneas/projections/Models.lean +++ b/verification/aeneas/projections/Models.lean @@ -59,6 +59,15 @@ check_model_binding Zerocopy.byteorder.F32 with 1 type parameters derive_rust_model Zerocopy.byteorder.F64 with 1 type parameters with_physical 0 check_model_binding Zerocopy.byteorder.F64 with 1 type parameters +derive_rust_model Zerocopy.layout.composition_checks.ReferenceTail with 0 type parameters +check_model_binding Zerocopy.layout.composition_checks.ReferenceTail with 0 type parameters + +derive_rust_model Zerocopy.layout.composition_checks.ReferenceSize with 0 type parameters +check_model_binding Zerocopy.layout.composition_checks.ReferenceSize with 0 type parameters + +derive_rust_model Zerocopy.layout.composition_checks.ReferenceLayout with 0 type parameters +check_model_binding Zerocopy.layout.composition_checks.ReferenceLayout with 0 type parameters + derive_rust_model Zerocopy.layout.RoundingAlignAndPhase with 0 type parameters decode self => let word := self._0.value let align := 2 ^ Nat.log2 word diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index b7282fb76c..9a35ca9bf9 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/verification/aeneas/projections/Specs.lean @@ -123,6 +123,22 @@ spec set_u32_be_spec aeneas_spec_end check_spec_binding Zerocopy.Specs.set_u32_be_spec for Zerocopy.byteorder.verification.set_u32_be with 2 +check_model_inputs Zerocopy.layout.composition_checks.check_extend with 0 type parameters +aeneas_spec_begin +spec composition_extend_checks_spec + for @Zerocopy.layout.composition_checks.check_extend with 0 type parameters + ensures _ => True +aeneas_spec_end +check_spec_binding Zerocopy.Specs.composition_extend_checks_spec for Zerocopy.layout.composition_checks.check_extend with 5 + +check_model_inputs Zerocopy.layout.composition_checks.check_pad with 0 type parameters +aeneas_spec_begin +spec composition_pad_checks_spec + for @Zerocopy.layout.composition_checks.check_pad with 0 type parameters + ensures _ => True +aeneas_spec_end +check_spec_binding Zerocopy.Specs.composition_pad_checks_spec for Zerocopy.layout.composition_checks.check_pad with 2 + check_model_inputs Zerocopy.layout.RoundingAlignAndPhase.new with 0 type parameters aeneas_spec_begin spec encoding_new_spec @@ -265,6 +281,32 @@ spec for_slice_spec (size align : Usize) aeneas_spec_end check_spec_binding Zerocopy.Specs.for_slice_spec for Zerocopy.layout.DstLayout.for_slice with 1 +check_model_inputs Zerocopy.layout.DstLayout.extend with 0 type parameters +aeneas_spec_begin +spec extend_spec + for @Zerocopy.layout.DstLayout.extend with 0 type parameters + 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) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.extend_spec for Zerocopy.layout.DstLayout.extend with 3 + +check_model_inputs Zerocopy.layout.DstLayout.pad_to_align with 0 type parameters +aeneas_spec_begin +spec pad_to_align_spec + for @Zerocopy.layout.DstLayout.pad_to_align with 0 type parameters + requires ha : (self.align : Nat).isPowerOfTwo + requires hfit : (ModelViews.layoutValue self).padFits Usize.max + ensures result => + ModelViews.layoutValue result = (ModelViews.layoutValue self).pad +aeneas_spec_end +check_spec_binding Zerocopy.Specs.pad_to_align_spec for Zerocopy.layout.DstLayout.pad_to_align with 1 + check_model_inputs Zerocopy.layout.DstLayout.requires_static_padding with 0 type parameters aeneas_spec_begin spec requires_static_padding_spec 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 5a205a6eef..dd46318db2 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(all(kani, kani_slow))] #[kani::proof_for_contract(DstLayout::pad_to_align)]