Skip to content

Prove exact trailing sizes, padding and capacity #3752

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
joshlf wants to merge 1 commit into
base: Glbefkopwxutlxlg5qgtbtb3p6a5o73ow
Choose a base branch
from
Open

Prove exact trailing sizes, padding and capacity #3752

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion verification/aeneas/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -121,7 +121,7 @@ zerocopy's unsafe pointer operations are sound.

## Scope and proofs

Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs), [nested reference](../../zerocopy/src/layout/nested_reference.rs), [primitive assertions](../../zerocopy/src/layout/primitive_checks.rs).
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).

Extraction starts from the function and nominal-type owners of every present
`aeneas` fence in `zerocopy/src`, including their dependencies. Every present
Expand All @@ -137,6 +137,7 @@ added without extending the specification set.
| `DstLayout::{assume_shallow_unpadded,new_zst,for_type,for_unpadded_type,for_slice}` | Exact alignment, size-information fields, and recorded shallow-padding flags under explicit input premises. |
| `SizeInfo::try_to_nonzero_elem_size`, `max_elems_for_bytes` | Exact zero handling, preserved representation fields, and greatest fitting element count. |
| `DstLayout::requires_static_padding` | Exact negation of the recorded shallow-unpadded flag. |
| Trailing size, padding, and capacity | Exact size-offset and capacity formulas, checked-size overflow, and wrapping padding; successful sizes and physical padding refine the independent recursive semantics. |

Every registered function uses total `spec`: accepted raw representations,
supplied mathematical ghosts, and explicit requirements imply successful
Expand Down Expand Up @@ -165,6 +166,9 @@ the unpadded flag; realizability, alignment and fit conditions remain explicit.
Generic size/alignment reads are external data inputs, not correctness axioms.
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.

Plain arithmetic clauses use mathematical word values carrying machine bounds
and NonZero positivity. Their Nat/Int arithmetic does not wrap; explicit raw
clauses preserve the extracted representation vocabulary while retaining
Expand Down
263 changes: 229 additions & 34 deletions verification/aeneas/golden/Funs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -643,14 +643,14 @@ def byteorder.verification.set_u32_be
byteorder.U32.get byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder value1

/-- [zerocopy::layout::POINTER_WIDTH_BITS]
Source: 'src/layout/mod.rs', lines 23:0-23:62 -/
Source: 'src/layout/mod.rs', lines 26:0-26: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 103:4-122:5 -/
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) :
Expand All @@ -671,7 +671,7 @@ def layout.RoundingAlignAndPhase.new
| some encoded1 => ok { _0 := encoded1 }

/-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::components]:
Source: 'src/layout/mod.rs', lines 136:4-163:5 -/
Source: 'src/layout/mod.rs', lines 139:4-166:5 -/
def layout.RoundingAlignAndPhase.components
(self : layout.RoundingAlignAndPhase) :
Result ((core.num.nonzero.NonZero Std.Usize
Expand Down Expand Up @@ -699,7 +699,7 @@ def layout.RoundingAlignAndPhase.components
ok (align1, phase)

/-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::align]:
Source: 'src/layout/mod.rs', lines 176:4-185:5 -/
Source: 'src/layout/mod.rs', lines 179:4-188:5 -/
def layout.RoundingAlignAndPhase.align
(self : layout.RoundingAlignAndPhase) :
Result (core.num.nonzero.NonZero Std.Usize
Expand All @@ -708,8 +708,126 @@ def layout.RoundingAlignAndPhase.align
let (nz, _) ← layout.RoundingAlignAndPhase.components self
ok nz

/-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
Source: 'src/util/mod.rs', lines 261:0-279:1 -/
def util.round_down_to_next_multiple_of_alignment
(n : Std.Usize)
(align : core.num.nonzero.NonZero Std.Usize
core.num.niche_types.NonZeroUsizeInner) :
Result Std.Usize
:= do
let align1 ←
core.num.nonzero.NonZero.get
Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
let b ← core.num.Usize.is_power_of_two align1
massert b
let i ← align1 - 1#usize
let mask ← lift (~~~ i)
ok (n &&& mask)

/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout<E>}::size_offset]:
Source: 'src/layout/mod.rs', lines 268:4-281:5 -/
def layout.TrailingSliceLayout.size_offset
{E : Type} (self : layout.TrailingSliceLayout E) : Result Std.Usize := do
let (size_align, size_phase) ←
layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase
let aligned_base ←
util.round_down_to_next_multiple_of_alignment self.size_base size_align
ok (aligned_base ||| size_phase)

/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout<E>}::max_trailing_bytes]:
Source: 'src/layout/mod.rs', lines 304:4-393:5 -/
def layout.TrailingSliceLayout.max_trailing_bytes
{E : Type} (self : layout.TrailingSliceLayout E)
(available_bytes : Std.Usize) :
Result (Option Std.Usize)
:= do
let (size_align, size_phase) ←
layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase
let rounded_phase ←
if size_phase = 0#usize
then ok 0#usize
else
core.num.nonzero.NonZero.get
Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner size_align
let o ← lift (Usize.checked_add self.size_base rounded_phase)
match o with
| none => ok none
| some size =>
let o1 ← lift (Usize.checked_sub available_bytes size)
match o1 with
| none => ok none
| some bytes =>
let aligned_bytes ←
util.round_down_to_next_multiple_of_alignment bytes size_align
let initial_padding ← rounded_phase - size_phase
let trailing_bytes ← lift (aligned_bytes ||| initial_padding)
ok (some trailing_bytes)

/-- [zerocopy::util::padding_needed_for]:
Source: 'src/util/mod.rs', lines 169:0-229:1 -/
def util.padding_needed_for
(len : Std.Usize)
(align : core.num.nonzero.NonZero Std.Usize
core.num.niche_types.NonZeroUsizeInner) :
Result Std.Usize
:= do
let i ←
core.num.nonzero.NonZero.get
Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
let mask ← i - 1#usize
let i1 ← lift (core.num.Usize.wrapping_sub len 1#usize)
let i2 ← lift (~~~ i1)
ok (i2 &&& mask)

/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout<usize>}::padding_for_elems]:
Source: 'src/layout/mod.rs', lines 418:4-473:5 -/
def layout.TrailingSliceLayoutUsize.padding_for_elems
(self : layout.TrailingSliceLayout Std.Usize) (elems : Std.Usize) :
Result Std.Usize
:= do
let (size_align, size_phase) ←
layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase
let i ←
core.num.nonzero.NonZero.get
Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner size_align
let size_mask ← i - 1#usize
let elem_remainder ← lift (self.elem_size &&& size_mask)
let i1 ← lift (core.num.Usize.wrapping_mul elems elem_remainder)
let trailing_remainder ← lift (i1 &&& size_mask)
let rounding_input ←
lift (core.num.Usize.wrapping_add size_phase trailing_remainder)
let rounding_padding ← util.padding_needed_for rounding_input size_align
let i2 ← lift (core.num.Usize.wrapping_add self.size_base size_phase)
let i3 ← lift (core.num.Usize.wrapping_sub i2 self.offset)
ok (core.num.Usize.wrapping_add i3 rounding_padding)

/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout<usize>}::size_for_elems]:
Source: 'src/layout/mod.rs', lines 491:4-555:5 -/
def layout.TrailingSliceLayoutUsize.size_for_elems
(self : layout.TrailingSliceLayout Std.Usize) (elems : Std.Usize) :
Result (Option Std.Usize)
:= do
let o ←
layout.TrailingSliceLayout.max_trailing_bytes self core.num.Usize.MAX
match o with
| none => ok none
| some bytes =>
let o1 ← lift (Usize.checked_mul self.elem_size elems)
match o1 with
| none => ok none
| some bytes1 =>
if bytes1 > bytes
then ok none
else
let trailing_end ←
lift (core.num.Usize.wrapping_add self.offset bytes1)
let i ← layout.TrailingSliceLayoutUsize.padding_for_elems self elems
let size ← lift (core.num.Usize.wrapping_add trailing_end i)
ok (some size)

/-- [zerocopy::layout::{zerocopy::layout::SizeInfo<usize>}::try_to_nonzero_elem_size]:
Source: 'src/layout/mod.rs', lines 791:4-819:5 -/
Source: 'src/layout/mod.rs', lines 817:4-845:5 -/
def layout.SizeInfoUsize.try_to_nonzero_elem_size
(self : layout.SizeInfo Std.Usize) :
Result (Option (layout.SizeInfo (core.num.nonzero.NonZero Std.Usize
Expand All @@ -734,7 +852,7 @@ def layout.SizeInfoUsize.try_to_nonzero_elem_size
}))

/-- [zerocopy::layout::max_elems_for_bytes]:
Source: 'src/layout/mod.rs', lines 847:0-862:1 -/
Source: 'src/layout/mod.rs', lines 873:0-888:1 -/
def layout.max_elems_for_bytes
(bytes : Std.Usize)
(elem_size : core.num.nonzero.NonZero Std.Usize
Expand All @@ -751,7 +869,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 882:4-885:6 -/
Source: 'src/layout/mod.rs', lines 908:4-911:6 -/
@[global_simps, irreducible]
def layout.DstLayout.MIN_ALIGN
:
Expand All @@ -766,13 +884,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 951:4-960:5 -/
Source: 'src/layout/mod.rs', lines 977:4-986: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 989:4-1009:5
Source: 'src/layout/mod.rs', lines 1015:4-1035:5
Visibility: public -/
def layout.DstLayout.new_zst
(repr_align : Option (core.num.nonzero.NonZero Std.Usize
Expand All @@ -796,7 +914,7 @@ def layout.DstLayout.new_zst
}

/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_type]:
Source: 'src/layout/mod.rs', lines 1033:4-1058:5
Source: 'src/layout/mod.rs', lines 1059:4-1084:5
Visibility: public -/
def layout.DstLayout.for_type (T : Type) : Result layout.DstLayout := do
let i ← core.mem.align_of T
Expand All @@ -815,15 +933,15 @@ 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 1088:4-1102:5
Source: 'src/layout/mod.rs', lines 1114:4-1128:5
Visibility: public -/
def layout.DstLayout.for_unpadded_type
(T : Type) : Result layout.DstLayout := do
let dl ← layout.DstLayout.for_type T
layout.DstLayout.assume_shallow_unpadded dl

/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_slice]:
Source: 'src/layout/mod.rs', lines 1127:4-1163:5 -/
Source: 'src/layout/mod.rs', lines 1153:4-1189:5 -/
def layout.DstLayout.for_slice (T : Type) : Result layout.DstLayout := do
let i ← core.mem.align_of T
let o ←
Expand All @@ -849,7 +967,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 1554:4-1563:5
Source: 'src/layout/mod.rs', lines 1580:4-1589:5
Visibility: public -/
def layout.DstLayout.requires_static_padding
(self : layout.DstLayout) : Result Bool := do
Expand Down Expand Up @@ -1062,38 +1180,115 @@ def layout.primitive_checks.check_empty_layout
massert empty.statically_shallow_unpadded
else ok ()

/-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
Source: 'src/util/mod.rs', lines 261:0-279:1 -/
def util.round_down_to_next_multiple_of_alignment
(n : Std.Usize)
/-- [zerocopy::layout::tail_checks::same_optional_usize]:
Source: 'src/layout/tail_checks.rs', lines 29:0-35:1 -/
def layout.tail_checks.same_optional_usize
(left : Option Std.Usize) (right : Option Std.Usize) : Result Bool := do
match left with
| none => match right with
| none => ok true
| some _ => ok false
| some left1 =>
match right with
| none => ok false
| some right1 => ok (left1 = right1)

/-- [zerocopy::layout::tail_checks::reference_round_up]:
Source: 'src/layout/tail_checks.rs', lines 38:0-42:1 -/
def layout.tail_checks.reference_round_up
(bytes : Std.Usize)
(align : core.num.nonzero.NonZero Std.Usize
core.num.niche_types.NonZeroUsizeInner) :
Result Std.Usize
Result (Option Std.Usize)
:= do
let align1 ←
let i ←
core.num.nonzero.NonZero.get
Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
let b ← core.num.Usize.is_power_of_two align1
massert b
let i ← align1 - 1#usize
let mask ← lift (~~~ i)
ok (n &&& mask)
let remainder ← bytes % i
let padding ← if remainder = 0#usize
then ok 0#usize
else i - remainder
ok (Usize.checked_add bytes padding)

/-- [zerocopy::layout::tail_checks::reference_size]:
Source: 'src/layout/tail_checks.rs', lines 44:0-60:1 -/
def layout.tail_checks.reference_size
(tail : layout.TrailingSliceLayout Std.Usize)
(align : core.num.nonzero.NonZero Std.Usize
core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
(elems : Std.Usize) :
Result (Option Std.Usize)
:= do
let o ← lift (Usize.checked_mul elems tail.elem_size)
match o with
| none => ok none
| some bytes =>
let o1 ← lift (Usize.checked_add phase bytes)
match o1 with
| none => ok none
| some input =>
let o2 ← layout.tail_checks.reference_round_up input align
match o2 with
| none => ok none
| some rounded => ok (Usize.checked_add tail.size_base rounded)

/-- [zerocopy::util::padding_needed_for]:
Source: 'src/util/mod.rs', lines 169:0-229:1 -/
def util.padding_needed_for
(len : Std.Usize)
/-- [zerocopy::layout::tail_checks::reference_capacity]:
Source: 'src/layout/tail_checks.rs', lines 63:0-76:1 -/
def layout.tail_checks.reference_capacity
(tail : layout.TrailingSliceLayout Std.Usize)
(align : core.num.nonzero.NonZero Std.Usize
core.num.niche_types.NonZeroUsizeInner) :
Result Std.Usize
core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
(budget : Std.Usize) :
Result (Option Std.Usize)
:= do
let o ← lift (Usize.checked_sub budget tail.size_base)
match o with
| none => ok none
| some after_base =>
let i ←
core.num.nonzero.NonZero.get
Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
let i1 ← after_base % i
let rounded_budget ← after_base - i1
ok (Usize.checked_sub rounded_budget phase)

/-- [zerocopy::layout::tail_checks::trailing_arithmetic_check]:
Source: 'src/layout/tail_checks.rs', lines 88:0-111:1 -/
def layout.tail_checks.trailing_arithmetic_check
(tail : layout.TrailingSliceLayout Std.Usize)
(align : core.num.nonzero.NonZero Std.Usize
core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
(elems : Std.Usize) (budget : Std.Usize) :
Result Unit
:= 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)
let b ← core.num.Usize.is_power_of_two i
if b
then
if phase < i
then
let o ← lift (Usize.checked_add i phase)
let i1 ←
core.num.nonzero.NonZero.get
Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner
tail.size_rounding_align_and_phase._0
let b1 ← layout.tail_checks.same_optional_usize o (some i1)
if b1
then
let o1 ← layout.TrailingSliceLayoutUsize.size_for_elems tail elems
let o2 ← layout.tail_checks.reference_size tail align phase elems
let b2 ← layout.tail_checks.same_optional_usize o1 o2
massert b2
let o3 ← layout.TrailingSliceLayout.max_trailing_bytes tail budget
let o4 ←
layout.tail_checks.reference_capacity tail align phase budget
let b3 ← layout.tail_checks.same_optional_usize o3 o4
massert b3
else ok ()
else ok ()
else ok ()

/-- [zerocopy::util::checks::check_arithmetic]:
Source: 'src/util/checks.rs', lines 38:0-46:1 -/
Expand Down
Loading
Loading