From d44db53761f15febf8e8b00b1ae4987372307600 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Fri, 2 Oct 2026 10:36:20 -0400 Subject: [PATCH] Compare nested DST sizes with a recursive Rust oracle Check runtime nested-DST sizes against an independently implemented recursive Rust oracle, including padding inside packed fields. Extract and prove the independent checked Rust reference for arbitrary nested record descriptions and metadata. Use its remainder-based rounding in compiler regression tests, without sharing the production padding utility. Validation: fresh pinned extraction and complete-model golden comparison; independent golden/live Lean builds, required-contract checks, and the transitive axiom audit. gherrit-pr-id: Guzdt7nfgmmi7y3e4taezg43ssexn4hrf Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/README.md | 2 +- verification/aeneas/golden/Funs.lean | 123 ++++- verification/aeneas/golden/Types.lean | 9 +- verification/aeneas/lean/LayoutModel.lean | 182 ++++++++ verification/aeneas/lean/Obligations.lean | 23 + verification/aeneas/lean/Proofs.lean | 1 + .../aeneas/lean/Proofs/NestedReference.lean | 419 ++++++++++++++++++ zerocopy/src/layout/mod.rs | 7 +- zerocopy/src/layout/nested_reference.rs | 120 +++++ 9 files changed, 878 insertions(+), 8 deletions(-) create mode 100644 verification/aeneas/lean/Proofs/NestedReference.lean create mode 100644 zerocopy/src/layout/nested_reference.rs diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 46b8f19d5c..1d8ee8b4b8 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -120,7 +120,7 @@ zerocopy's unsafe pointer operations are sound. ## Scope and proofs -Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs). +Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs), [nested reference](../../zerocopy/src/layout/nested_reference.rs). Extraction starts from the function and nominal-type owners of every present `aeneas` fence in `zerocopy/src`, including their dependencies. Every present diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index f8dad1e701..051c3f642f 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -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 17:0-17:62 -/ + Source: 'src/layout/mod.rs', lines 20:0-20: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 97:4-116:5 -/ + Source: 'src/layout/mod.rs', lines 100:4-119:5 -/ def layout.RoundingAlignAndPhase.new (align : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) : @@ -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 130:4-157:5 -/ + Source: 'src/layout/mod.rs', lines 133:4-160:5 -/ def layout.RoundingAlignAndPhase.components (self : layout.RoundingAlignAndPhase) : Result ((core.num.nonzero.NonZero Std.Usize @@ -699,7 +699,7 @@ def layout.RoundingAlignAndPhase.components ok (align1, phase) /-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::align]: - Source: 'src/layout/mod.rs', lines 170:4-179:5 -/ + Source: 'src/layout/mod.rs', lines 173:4-182:5 -/ def layout.RoundingAlignAndPhase.align (self : layout.RoundingAlignAndPhase) : Result (core.num.nonzero.NonZero Std.Usize @@ -708,6 +708,121 @@ def layout.RoundingAlignAndPhase.align let (nz, _) ← layout.RoundingAlignAndPhase.components self ok nz +/-- [zerocopy::layout::nested_reference::round_up]: + Source: 'src/layout/nested_reference.rs', lines 46:0-56:1 -/ +def layout.nested_reference.round_up + (size : Std.Usize) (align : Std.Usize) : Result (Option Std.Usize) := do + if align = 0#usize + then ok none + else + let remainder ← size % align + if remainder = 0#usize + then ok (some size) + else let i ← align - remainder + ok (Usize.checked_add size i) + +/-- [zerocopy::layout::nested_reference::apply_layer]: + Source: 'src/layout/nested_reference.rs', lines 58:0-80:1 -/ +def layout.nested_reference.apply_layer + (layer : layout.nested_reference.NestedLayer) (size : Std.Usize) + (alignment : Std.Usize) : + Result (Option (Std.Usize × Std.Usize)) + := do + let b ← core.num.Usize.is_power_of_two layer.packed + if b + then + let b1 ← core.num.Usize.is_power_of_two layer.min_align + if b1 + then + if layer.min_align > layer.packed + then ok none + else + let field_align ← + if alignment < layer.packed + then ok alignment + else ok layer.packed + let o ← + layout.nested_reference.round_up layer.prefix_bytes field_align + match o with + | none => ok none + | some offset => + let alignment1 ← + if layer.min_align < field_align + then ok field_align + else ok layer.min_align + let o1 ← lift (Usize.checked_add offset size) + match o1 with + | none => ok none + | some size1 => + let o2 ← layout.nested_reference.round_up size1 alignment1 + match o2 with + | none => ok none + | some size2 => ok (some (size2, alignment1)) + else ok none + else ok none + +/-- [zerocopy::layout::nested_reference::size_for_metadata]: loop body 0: + Source: 'src/layout/nested_reference.rs', lines 108:4-115:5 -/ +@[rust_loop_body] +def layout.nested_reference.size_for_metadata_loop.body + (leading : Slice layout.nested_reference.NestedLayer) + (state : Option (Std.Usize × Std.Usize)) (i : Std.Usize) : + Result (ControlFlow ((Option (Std.Usize × Std.Usize)) × Std.Usize) (Option + (Std.Usize × Std.Usize))) + := do + if i != 0#usize + then + let i1 ← i - 1#usize + let layer ← Slice.index_usize leading i1 + match state with + | none => ok (cont (none, i1)) + | some p => + let (size, alignment) := p + let state1 ← layout.nested_reference.apply_layer layer size alignment + ok (cont (state1, i1)) + else ok (done state) + +/-- [zerocopy::layout::nested_reference::size_for_metadata]: loop 0: + Source: 'src/layout/nested_reference.rs', lines 108:4-115:5 -/ +@[rust_loop] +def layout.nested_reference.size_for_metadata_loop + (leading : Slice layout.nested_reference.NestedLayer) + (state : Option (Std.Usize × Std.Usize)) (i : Std.Usize) : + Result (Option (Std.Usize × Std.Usize)) + := do + loop + (fun (state1, i1) => layout.nested_reference.size_for_metadata_loop.body + leading state1 i1) + (state, i) + +/-- [zerocopy::layout::nested_reference::size_for_metadata]: + Source: 'src/layout/nested_reference.rs', lines 94:0-120:1 -/ +def layout.nested_reference.size_for_metadata + (leading : Slice layout.nested_reference.NestedLayer) (elem_size : Std.Usize) + (leaf_align : Std.Usize) (elems : Std.Usize) : + Result (Option Std.Usize) + := do + let b ← core.num.Usize.is_power_of_two leaf_align + if b + then + let i ← elem_size % leaf_align + if i != 0#usize + then ok none + else + let o ← lift (Usize.checked_mul elem_size elems) + let state ← + match o with + | none => ok none + | some size => ok (some (size, leaf_align)) + let i1 := Slice.len leading + let state1 ← + layout.nested_reference.size_for_metadata_loop leading state i1 + match state1 with + | none => ok none + | some p => let (size, _) := p + ok (some size) + else ok none + /-- [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 diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index a53b231469..1d882da79b 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -100,9 +100,16 @@ structure byteorder.U32 (O : Type) where _1 : core.marker.PhantomData O /-- [zerocopy::layout::RoundingAlignAndPhase] - Source: 'src/layout/mod.rs', lines 78:0-78:54 -/ + Source: 'src/layout/mod.rs', lines 81:0-81:54 -/ structure layout.RoundingAlignAndPhase where _0 : core.num.nonzero.NonZero Std.Usize core.num.niche_types.NonZeroUsizeInner +/-- [zerocopy::layout::nested_reference::NestedLayer] + Source: 'src/layout/nested_reference.rs', lines 27:0-31:1 -/ +structure layout.nested_reference.NestedLayer where + packed : Std.Usize + min_align : Std.Usize + prefix_bytes : Std.Usize + end Zerocopy diff --git a/verification/aeneas/lean/LayoutModel.lean b/verification/aeneas/lean/LayoutModel.lean index d2859cdab2..adc6a518f7 100644 --- a/verification/aeneas/lean/LayoutModel.lean +++ b/verification/aeneas/lean/LayoutModel.lean @@ -27,3 +27,185 @@ namespace Zerocopy.Proofs end Zerocopy.Proofs + +namespace Zerocopy.Proofs.NestedReference + +/- The independent recursive rule uses unbounded arithmetic and complete +inner-field sizes. Layers are ordered from outermost to innermost. These +definitions do not call an extracted implementation or manipulate its +normalized base and phase. +-/ +def layerValid (layer : layout.nested_reference.NestedLayer) : Prop := + layer.packed.val.isPowerOfTwo ∧ layer.min_align.val.isPowerOfTwo ∧ + layer.min_align.val ≤ layer.packed.val + +def valid (layers : List layout.nested_reference.NestedLayer) + (elem alignment : Nat) : Prop := + alignment.isPowerOfTwo ∧ elem % alignment = 0 ∧ ∀ layer ∈ layers, layerValid layer + +def step (layer : layout.nested_reference.NestedLayer) (inner : Nat × Nat) : Nat × Nat := + let placementAlign := min inner.2 layer.packed.val + let alignment := max layer.min_align.val placementAlign + (LayoutMath.roundUp (LayoutMath.roundUp layer.prefix_bytes.val placementAlign + inner.1) alignment, + alignment) + +def state (layers : List layout.nested_reference.NestedLayer) + (elem alignment metadata : Nat) : Nat × Nat := + layers.foldr step (metadata * elem, alignment) + +theorem state_cons (layer : layout.nested_reference.NestedLayer) + (layers : List layout.nested_reference.NestedLayer) (elem alignment metadata : Nat) : + state (layer :: layers) elem alignment metadata = + step layer (state layers elem alignment metadata) := rfl + +theorem step_contains_inner (layer : layout.nested_reference.NestedLayer) (inner : Nat × Nat) : + inner.1 ≤ (step layer inner).1 := by + simp only [step, LayoutMath.roundUp] + omega + +theorem step_alignment_power (layer : layout.nested_reference.NestedLayer) + (inner : Nat × Nat) (hl : layerValid layer) (ha : inner.2.isPowerOfTwo) : + (step layer inner).2.isPowerOfTwo := by + simp only [step] + have hm : (min inner.2 layer.packed.val).isPowerOfTwo := by + by_cases h : inner.2 ≤ layer.packed.val + · simpa only [Nat.min_eq_left h] using ha + · simpa only [Nat.min_eq_right (by omega : layer.packed.val ≤ inner.2)] using hl.1 + by_cases h : layer.min_align.val ≤ min inner.2 layer.packed.val + · simpa only [Nat.max_eq_right h] using hm + · simpa only [Nat.max_eq_left (by omega : min inner.2 layer.packed.val ≤ layer.min_align.val)] + using hl.2.1 + +theorem state_alignment_power (layers : List layout.nested_reference.NestedLayer) + (elem alignment metadata : Nat) (h : valid layers elem alignment) : + (state layers elem alignment metadata).2.isPowerOfTwo := by + induction layers with + | nil => exact h.1 + | cons layer layers ih => + simp only [state, List.foldr_cons] + apply step_alignment_power + · exact h.2.2 layer (by simp) + · apply ih + exact ⟨h.1, h.2.1, fun x hx => h.2.2 x (by simp [hx])⟩ + +theorem state_alignment_bound (layers : List layout.nested_reference.NestedLayer) + (elem alignment metadata bound : Nat) (ha : alignment ≤ bound) + (hl : ∀ layer ∈ layers, layer.min_align.val ≤ bound) : + (state layers elem alignment metadata).2 ≤ bound := by + induction layers with + | nil => exact ha + | cons layer layers ih => + rw [state_cons] + simp only [step] + apply max_le + · exact hl layer (by simp) + · apply le_trans (Nat.min_le_left _ _) + exact ih (fun x hx => hl x (by simp [hx])) + +theorem state_contains_suffix (layers : List layout.nested_reference.NestedLayer) + (elem alignment metadata count : Nat) : + (state (layers.drop count) elem alignment metadata).1 ≤ + (state layers elem alignment metadata).1 := by + induction layers generalizing count with + | nil => simp + | cons layer layers ih => + cases count with + | zero => simp + | succ count => + simp only [List.drop_succ_cons, state_cons] + exact le_trans (ih count) (step_contains_inner layer (state layers elem alignment metadata)) + +theorem suffix_zero_size_fits (layers : List layout.nested_reference.NestedLayer) + (elem alignment limit count : Nat) (hfit : (state layers elem alignment 0).1 ≤ limit) : + (state (layers.drop count) elem alignment 0).1 ≤ limit := + le_trans (state_contains_suffix layers elem alignment 0 count) hfit + +theorem step_contains_placed_field (layer : layout.nested_reference.NestedLayer) + (inner : Nat × Nat) : + LayoutMath.roundUp layer.prefix_bytes.val (min inner.2 layer.packed.val) + inner.1 ≤ + (step layer inner).1 := by + simp only [step, LayoutMath.roundUp] + omega + +theorem step_contains_prefix (layer : layout.nested_reference.NestedLayer) + (inner : Nat × Nat) : layer.prefix_bytes.val ≤ (step layer inner).1 := by + simp only [step, LayoutMath.roundUp] + omega + +theorem valid_cons (layer : layout.nested_reference.NestedLayer) + (layers : List layout.nested_reference.NestedLayer) (elem alignment : Nat) : + valid (layer :: layers) elem alignment ↔ layerValid layer ∧ valid layers elem alignment := by + simp only [valid, List.mem_cons, forall_eq_or_imp] + tauto + +noncomputable def checkedState (layers : List layout.nested_reference.NestedLayer) + (elem alignment metadata : Nat) : Option (Nat × Nat) := by + classical + exact if valid layers elem alignment then + if (state layers elem alignment metadata).1 ≤ Usize.max + then some (state layers elem alignment metadata) else none + else none + +noncomputable def checkedLayer (layer : layout.nested_reference.NestedLayer) + (inner : Option (Nat × Nat)) : Option (Nat × Nat) := by + classical + exact if layerValid layer then inner.bind (fun inner => + if (step layer inner).1 ≤ Usize.max then some (step layer inner) else none) else none + +theorem checkedState_cons (layer : layout.nested_reference.NestedLayer) + (layers : List layout.nested_reference.NestedLayer) (elem alignment metadata : Nat) : + checkedState (layer :: layers) elem alignment metadata = + checkedLayer layer (checkedState layers elem alignment metadata) := by + classical + by_cases hl : layerValid layer + · by_cases hv : valid layers elem alignment + · by_cases hf : (state layers elem alignment metadata).1 ≤ Usize.max + · simp only [checkedState, checkedLayer, valid_cons, hl, hv, true_and, if_true, + hf, state_cons, Option.bind_some] + · have ho : ¬(step layer (state layers elem alignment metadata)).1 ≤ Usize.max := by + have := step_contains_inner layer (state layers elem alignment metadata) + omega + simp only [checkedState, checkedLayer, valid_cons, hl, hv, true_and, if_true, + hf, if_false, state_cons, ho, Option.bind_none] + · simp only [checkedState, checkedLayer, valid_cons, hl, hv, true_and, if_false, + if_true, Option.bind_none] + · simp only [checkedState, checkedLayer, valid_cons, hl, false_and, if_false] + +theorem checkedState_some (layers : List layout.nested_reference.NestedLayer) + (elem alignment metadata : Nat) (out : Nat × Nat) + (h : checkedState layers elem alignment metadata = some out) : + valid layers elem alignment ∧ state layers elem alignment metadata = out ∧ out.1 ≤ Usize.max := by + classical + unfold checkedState at h + split at h + · rename_i hv + split at h + · rename_i hf + have heq := Option.some.inj h + exact ⟨hv, heq, heq ▸ hf⟩ + · contradiction + · contradiction + +theorem checkedState_drop (layers : List layout.nested_reference.NestedLayer) + (elem alignment metadata i : Nat) (hi : i < layers.length) : + checkedState (layers.drop i) elem alignment metadata = + checkedLayer layers[i] (checkedState (layers.drop (i + 1)) elem alignment metadata) := by + rw [List.drop_eq_getElem_cons hi, checkedState_cons] + +noncomputable def checkedSize (layers : List layout.nested_reference.NestedLayer) + (elem alignment metadata : Nat) : Option Nat := by + classical + exact if valid layers elem alignment then + if (state layers elem alignment metadata).1 ≤ Usize.max + then some (state layers elem alignment metadata).1 else none + else none + +theorem checkedSize_eq_map (layers : List layout.nested_reference.NestedLayer) + (elem alignment metadata : Nat) : + checkedSize layers elem alignment metadata = + (checkedState layers elem alignment metadata).map Prod.fst := by + classical + unfold checkedSize checkedState + split <;> (try split) <;> simp + +end Zerocopy.Proofs.NestedReference diff --git a/verification/aeneas/lean/Obligations.lean b/verification/aeneas/lean/Obligations.lean index 19453e6e6c..e2b5a5aa10 100644 --- a/verification/aeneas/lean/Obligations.lean +++ b/verification/aeneas/lean/Obligations.lean @@ -30,6 +30,29 @@ or a second proof that the compiler implements Rust correctly. open Aeneas Aeneas.Std AeneasSpecs namespace Zerocopy.Obligations open Zerocopy.Proofs + +def nested_round_up_spec_contract (size align : Usize) + (run : Result (Option Usize)) : Prop := + run ⦃ rounded => rounded.map UScalar.val = + if align.val = 0 then none + else if LayoutMath.roundUp size.val align.val ≤ Usize.max + then some (LayoutMath.roundUp size.val align.val) else none ⦄ + +def nested_round_up_spec : Prop := + ∀ size align, nested_round_up_spec_contract size align + (layout.nested_reference.round_up size align) + +def nested_reference_size_spec_contract + (leading : Slice layout.nested_reference.NestedLayer) (elem_size leaf_align elems : Usize) + (run : Result (Option Usize)) : Prop := + run ⦃ result => result.map UScalar.val = + NestedReference.checkedSize leading.val elem_size.val leaf_align.val elems.val ⦄ + +def nested_reference_size_spec : Prop := + ∀ leading elem_size leaf_align elems, + nested_reference_size_spec_contract leading elem_size leaf_align elems + (layout.nested_reference.size_for_metadata leading elem_size leaf_align elems) + abbrev NonZeroUsize := core.num.nonzero.NonZero Usize core.num.niche_types.NonZeroUsizeInner diff --git a/verification/aeneas/lean/Proofs.lean b/verification/aeneas/lean/Proofs.lean index 89ff7b9e67..bee36adb80 100644 --- a/verification/aeneas/lean/Proofs.lean +++ b/verification/aeneas/lean/Proofs.lean @@ -9,6 +9,7 @@ those terms. -/ module public import Specs public import Proofs.Util +public import Proofs.NestedReference public import Aeneas public import Loops public import RepresentationLaws diff --git a/verification/aeneas/lean/Proofs/NestedReference.lean b/verification/aeneas/lean/Proofs/NestedReference.lean new file mode 100644 index 0000000000..071f791689 --- /dev/null +++ b/verification/aeneas/lean/Proofs/NestedReference.lean @@ -0,0 +1,419 @@ +/- 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 Specs +public import Loops +public import Obligations +public import ModelLemmas +import all Init.Data.Nat.Power2.Basic +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs.Raw + +def nestedStateView (state : Usize × Usize) : Nat × Nat := (state.1.val, state.2.val) + +theorem nested_round_up_spec (size align : Usize) : + layout.nested_reference.round_up size align + ⦃ rounded => rounded.map UScalar.val = + if align.val = 0 then none + else if LayoutMath.roundUp size.val align.val ≤ Usize.max + then some (LayoutMath.roundUp size.val align.val) else none ⦄ := by + unfold layout.nested_reference.round_up + by_cases hz : align = 0#usize + · subst align + simp + · simp only [hz, if_false] + have ha : 0 < align.val := by + have hn : align.val ≠ 0 := by + intro h + apply hz + exact UScalar.eq_of_val_eq (by simpa using h) + omega + step with Usize.rem_spec size (y := align) (by omega) as ⟨remainder, hr⟩ + by_cases hrz : remainder = 0#usize + · have hr0 : size.val % align.val = 0 := by + have h := congrArg UScalar.val hrz + simpa only [hr, show (0#usize).val = 0 by simp] using h + simp only [hrz, if_true, WP.spec_ok, Option.map_some, + show ¬align.val = 0 by omega, if_false, LayoutMath.roundUp_eq _ _ hr0, + show size.val ≤ Usize.max by scalar_tac, if_true] + · simp only [hrz, if_false] + have hrem := Nat.mod_lt size.val ha + step with Usize.sub_spec (x := align) (y := remainder) (by rw [hr]; omega) + as ⟨padding, hp, _⟩ + have hrpos : 0 < size.val % align.val := by + have hn : remainder.val ≠ 0 := by + intro h + apply hrz + exact UScalar.eq_of_val_eq (by simpa using h) + omega + have hp' : padding.val = (align.val - size.val % align.val) % align.val := by + have hm : (align.val - size.val % align.val) % align.val = + align.val - size.val % align.val := Nat.mod_eq_of_lt (by omega) + rw [hp, hr, hm] + have hchecked := Usize.checked_add_bv_spec size padding + cases hc : Usize.checked_add size padding <;> + simp only [hc] at hchecked + · have hn : ¬LayoutMath.roundUp size.val align.val ≤ Usize.max := by + unfold LayoutMath.roundUp + omega + simp only [Option.map_none, show ¬align.val = 0 by omega, if_false, hn] + · rename_i rounded + have hs : LayoutMath.roundUp size.val align.val ≤ Usize.max := by + unfold LayoutMath.roundUp + omega + simp only [Option.map_some, show ¬align.val = 0 by omega, if_false, hs, if_true] + congr 1 + unfold LayoutMath.roundUp + omega + +theorem nested_apply_layer_spec (layer : layout.nested_reference.NestedLayer) + (size alignment : Usize) (ha : alignment.val.isPowerOfTwo) : + layout.nested_reference.apply_layer layer size alignment + ⦃ result => result.map nestedStateView = + NestedReference.checkedLayer layer (some (size.val, alignment.val)) ⦄ := by + classical + unfold layout.nested_reference.apply_layer + step as ⟨packedPow, hp⟩ + cases packedPow with + | false => + have hn : ¬layer.packed.val.isPowerOfTwo := by + intro h + have := (Iff.of_eq hp).mpr h + contradiction + have hl : ¬NestedReference.layerValid layer := by + intro h + exact hn h.1 + simp only [Bool.false_eq_true, if_false, WP.spec_ok, Option.map_none, + NestedReference.checkedLayer, hl, if_false] + | true => + have hp' : layer.packed.val.isPowerOfTwo := (Iff.of_eq hp).mp rfl + simp only [if_true] + step as ⟨minimumPow, hm⟩ + cases minimumPow with + | false => + have hn : ¬layer.min_align.val.isPowerOfTwo := by + intro h + have := (Iff.of_eq hm).mpr h + contradiction + have hl : ¬NestedReference.layerValid layer := by + intro h + exact hn h.2.1 + simp only [Bool.false_eq_true, if_false, WP.spec_ok, Option.map_none, + NestedReference.checkedLayer, hl, if_false] + | true => + have hm' : layer.min_align.val.isPowerOfTwo := (Iff.of_eq hm).mp rfl + simp only [if_true, UScalar.lt_equiv] + split + · rename_i hlarge + have hl : ¬NestedReference.layerValid layer := by + intro h + exact not_lt_of_ge h.2.2 hlarge + simp only [WP.spec_ok, Option.map_none, NestedReference.checkedLayer, hl, if_false] + · rename_i hsmall + have hl : NestedReference.layerValid layer := ⟨hp', hm', by omega⟩ + let field := min alignment layer.packed + have hfieldRaw : (if alignment < layer.packed then Result.ok alignment else .ok layer.packed) = + Result.ok field := by + by_cases h : alignment < layer.packed + · simp only [h, if_true, field, min_eq_left (le_of_lt h)] + · simp only [h, if_false, field, min_eq_right (le_of_not_gt h)] + have hfield : (if alignment.val < layer.packed.val then Result.ok alignment else .ok layer.packed) = + Result.ok field := by simpa only [UScalar.lt_equiv] using hfieldRaw + simp only [hfield, bind_ok] + have hf : field.val = min alignment.val layer.packed.val := Arithmetic.coe_min _ _ + have hfp : field.val.isPowerOfTwo := by + rw [hf] + by_cases h : alignment.val ≤ layer.packed.val + · simpa only [Nat.min_eq_left h] using ha + · simpa only [Nat.min_eq_right (by omega : layer.packed.val ≤ alignment.val)] using hp' + have hfpos := Nat.pos_of_isPowerOfTwo hfp + step with nested_round_up_spec layer.prefix_bytes field as ⟨offset, hoffset⟩ + change offset.map UScalar.val = if field.val = 0 then none else + if LayoutMath.roundUp layer.prefix_bytes.val field.val ≤ Usize.max then + some (LayoutMath.roundUp layer.prefix_bytes.val field.val) else none at hoffset + simp only [show ¬field.val = 0 by omega, if_false] at hoffset + let outer := max layer.min_align field + have houtRaw : (if layer.min_align < field then Result.ok field else .ok layer.min_align) = + Result.ok outer := by + by_cases h : layer.min_align < field + · simp only [h, if_true, outer, max_eq_right (le_of_lt h)] + · simp only [h, if_false, outer, max_eq_left (le_of_not_gt h)] + have hout : (if layer.min_align.val < field.val then Result.ok field else .ok layer.min_align) = + Result.ok outer := by simpa only [UScalar.lt_equiv] using houtRaw + have ho : outer.val = max layer.min_align.val field.val := Arithmetic.coe_max _ _ + have hopos : 0 < outer.val := by + rw [ho] + have := Nat.le_max_right layer.min_align.val field.val + omega + let target := NestedReference.step layer (size.val, alignment.val) + have htarget : target = + (LayoutMath.roundUp (LayoutMath.roundUp layer.prefix_bytes.val field.val + size.val) + outer.val, outer.val) := by + simp only [target, NestedReference.step, hf, ho] + have hcontains : LayoutMath.roundUp layer.prefix_bytes.val field.val ≤ target.1 := by + rw [htarget] + simp only [LayoutMath.roundUp] + omega + have hmodel : NestedReference.checkedLayer layer (some (size.val, alignment.val)) = + if target.1 ≤ Usize.max then some target else none := by + simp only [NestedReference.checkedLayer, hl, if_true, Option.bind_some] + rfl + simp only [hmodel] + cases offset with + | none => + have hnot : ¬LayoutMath.roundUp layer.prefix_bytes.val field.val ≤ Usize.max := by + split at hoffset <;> simp_all + have hn : ¬target.1 ≤ Usize.max := by omega + simp only [WP.spec_ok, Option.map_none, hn, if_false] + | some offset => + have hv : offset.val = LayoutMath.roundUp layer.prefix_bytes.val field.val := by + split at hoffset <;> simp_all + simp only [hout, bind_ok] + step as ⟨unpadded, hu⟩ + cases unpadded with + | none => + have hsum : Usize.max < offset.val + size.val := hu + have hn : ¬target.1 ≤ Usize.max := by + rw [htarget] + simp only [LayoutMath.roundUp] at hv ⊢ + omega + simp only [WP.spec_ok, Option.map_none, hn, if_false] + | some unpadded => + have husize : unpadded.val = offset.val + size.val := hu.2.1 + step with nested_round_up_spec unpadded outer as ⟨rounded, hr⟩ + change rounded.map UScalar.val = if outer.val = 0 then none else + if LayoutMath.roundUp unpadded.val outer.val ≤ Usize.max then + some (LayoutMath.roundUp unpadded.val outer.val) else none at hr + simp only [show ¬outer.val = 0 by omega, if_false] at hr + have hround : LayoutMath.roundUp unpadded.val outer.val = target.1 := by + rw [husize, hv, htarget] + rw [hround] at hr + cases rounded with + | none => + have hn : ¬target.1 ≤ Usize.max := by split at hr <;> simp_all + simp only [WP.spec_ok, Option.map_none, hn, if_false] + | some rounded => + have ht : target.1 ≤ Usize.max := by split at hr <;> simp_all + have hsize : rounded.val = target.1 := by split at hr <;> simp_all + have halign : outer.val = target.2 := by rw [htarget] + simp only [WP.spec_ok, Option.map_some, nestedStateView, ht, if_true, hsize, halign, + Prod.mk.eta] + +/-- The reverse loop retains complete recursive size at every layer. Its +termination measure is the remaining layer index; no bound limits nesting. -/ +theorem nested_reference_loop_spec + (leading : Slice layout.nested_reference.NestedLayer) (elem alignment metadata : Nat) + (state : Option (Usize × Usize)) (i : Usize) + (hi : i.val ≤ leading.val.length) + (hv : state.map nestedStateView = + NestedReference.checkedState (leading.val.drop i.val) elem alignment metadata) : + layout.nested_reference.size_for_metadata_loop leading state i + ⦃ out => out.map nestedStateView = + NestedReference.checkedState leading.val elem alignment metadata ⦄ := by + unfold layout.nested_reference.size_for_metadata_loop + apply loop.spec_decr_nat + (fun s : Option (Usize × Usize) × Usize => s.2.val) + (fun s => s.2.val ≤ leading.val.length ∧ s.1.map nestedStateView = + NestedReference.checkedState (leading.val.drop s.2.val) elem alignment metadata) + · rintro ⟨state, idx⟩ ⟨hi, hv⟩ + dsimp only at hi hv ⊢ + unfold layout.nested_reference.size_for_metadata_loop.body + simp only [bne_iff_ne] + split + · rename_i hn + have hpos : 0 < idx.val := by + have hz : idx.val ≠ 0 := by + intro h + apply hn + exact UScalar.eq_of_val_eq (by simpa using h) + omega + step with Usize.sub_spec (x := idx) (y := 1#usize) (by simp; omega) + as ⟨j, hj, _⟩ + have hj' : j.val + 1 = idx.val := by + change j.val = idx.val - 1 at hj + omega + have hjlt : j.val < leading.val.length := by omega + step with Slice.index_usize_spec leading j hjlt as ⟨layer, hlayer⟩ + have hmath : NestedReference.checkedState (leading.val.drop j.val) elem alignment metadata = + NestedReference.checkedLayer layer + (NestedReference.checkedState (leading.val.drop idx.val) elem alignment metadata) := by + rw [NestedReference.checkedState_drop leading.val elem alignment metadata j.val hjlt, + hj', hlayer] + cases state with + | none => + have hnext : (none : Option (Usize × Usize)).map nestedStateView = + NestedReference.checkedState (leading.val.drop j.val) elem alignment metadata := by + rw [hmath, ← hv] + simp [NestedReference.checkedLayer] + apply WP.spec.ret + change j.val ≤ leading.val.length ∧ + (none : Option (Usize × Usize)).map nestedStateView = + NestedReference.checkedState (leading.val.drop j.val) elem alignment metadata ∧ + j.val < idx.val + exact ⟨by omega, hnext, by omega⟩ + | some pair => + have heq : NestedReference.checkedState (leading.val.drop idx.val) elem alignment metadata = + some (nestedStateView pair) := hv.symm + obtain ⟨hvalid, heq, hfit⟩ := NestedReference.checkedState_some + (leading.val.drop idx.val) elem alignment metadata (nestedStateView pair) heq + have hpower : pair.2.val.isPowerOfTwo := by + have hp := NestedReference.state_alignment_power (leading.val.drop idx.val) + elem alignment metadata hvalid + rw [heq] at hp + exact hp + rcases pair with ⟨size, currentAlignment⟩ + step with nested_apply_layer_spec layer size currentAlignment hpower as ⟨next, hnext⟩ + have hview : next.map nestedStateView = + NestedReference.checkedState (leading.val.drop j.val) elem alignment metadata := by + rw [hmath, ← hv] + exact hnext + exact ⟨by omega, hview, by omega⟩ + · rename_i hz + have heq : idx.val = 0 := by + have h : idx = 0#usize := not_ne_iff.mp hz + simpa using congrArg UScalar.val h + simpa only [heq, List.drop_zero, WP.spec_ok] using hv + · exact ⟨hi, hv⟩ + +theorem nested_reference_size_spec + (leading : Slice layout.nested_reference.NestedLayer) (elem_size leaf_align elems : Usize) : + layout.nested_reference.size_for_metadata leading elem_size leaf_align elems + ⦃ result => result.map UScalar.val = + NestedReference.checkedSize leading.val elem_size.val leaf_align.val elems.val ⦄ := by + classical + unfold layout.nested_reference.size_for_metadata + step as ⟨leafPow, hp⟩ + cases leafPow with + | false => + have hn : ¬leaf_align.val.isPowerOfTwo := by + intro h + have := (Iff.of_eq hp).mpr h + contradiction + have hv : ¬NestedReference.valid leading.val elem_size.val leaf_align.val := by + intro h + exact hn h.1 + simp only [Bool.false_eq_true, if_false, WP.spec_ok, Option.map_none, + NestedReference.checkedSize, hv, if_false] + | true => + have hpow : leaf_align.val.isPowerOfTwo := (Iff.of_eq hp).mp rfl + have hpos := Nat.pos_of_isPowerOfTwo hpow + simp only [if_true] + step with Usize.rem_spec elem_size (y := leaf_align) (by omega) as ⟨remainder, hr⟩ + simp only [bne_iff_ne] + split + · rename_i hn + have hv : ¬NestedReference.valid leading.val elem_size.val leaf_align.val := by + intro h + apply hn + exact UScalar.eq_of_val_eq (by simpa only [hr, show (0#usize).val = 0 by simp] using h.2.1) + simp only [WP.spec_ok, Option.map_none, NestedReference.checkedSize, hv, if_false] + · rename_i hz + have hzero : elem_size.val % leaf_align.val = 0 := by + have h : remainder = 0#usize := not_ne_iff.mp hz + simpa only [hr, show (0#usize).val = 0 by simp] using congrArg UScalar.val h + step as ⟨product, hproduct⟩ + let start : Option (Usize × Usize) := match product with + | none => none + | some size => some (size, leaf_align) + have hinit : start.map nestedStateView = + NestedReference.checkedState (leading.val.drop (Slice.len leading).val) + elem_size.val leaf_align.val elems.val := by + have hvalid : NestedReference.valid [] elem_size.val leaf_align.val := + ⟨hpow, hzero, by simp⟩ + simp only [Slice.len_val, Slice.length, List.drop_length, NestedReference.checkedState, + hvalid, if_true, NestedReference.state, List.foldr_nil] + cases product with + | none => + have hn : ¬elems.val * elem_size.val ≤ Usize.max := by + simp only [] at hproduct + rw [Nat.mul_comm] + omega + simp only [start, Option.map_none, hn, if_false] + | some size => + have hv : size.val = elems.val * elem_size.val := by + simp only [] at hproduct + rw [Nat.mul_comm] + exact hproduct.2.1 + have hf : elems.val * elem_size.val ≤ Usize.max := by + simp only [] at hproduct + rw [Nat.mul_comm] + exact hproduct.1 + simp only [start, Option.map_some, nestedStateView, hv, hf, if_true] + have hrun := nested_reference_loop_spec leading elem_size.val leaf_align.val elems.val + start (Slice.len leading) (by simp only [Slice.len_val, Slice.length, le_refl]) hinit + cases product <;> simp only [start] at hrun ⊢ + all_goals + step with hrun as ⟨out, hout⟩ + have hfinal : (match out with | none => none | some pair => some pair.1).map UScalar.val = + NestedReference.checkedSize leading.val elem_size.val leaf_align.val elems.val := by + rw [NestedReference.checkedSize_eq_map, ← hout] + cases out <;> rfl + cases out with + | none => simpa only [WP.spec_ok] using hfinal + | some pair => + rcases pair with ⟨size, alignment⟩ + dsimp only + exact WP.spec.ret hfinal + +end Zerocopy.Proofs.Raw + +namespace Zerocopy.Proofs +open AeneasSpecs + +theorem nested_round_up_spec : Zerocopy.Specs.nested_round_up_spec := by + intro size align sizeValue hsize alignValue halign + apply WP.spec_mono (Raw.nested_round_up_spec size align) + intro rounded hr + refine ⟨rounded.map unsignedWord, ?_, hr⟩ + cases rounded <;> rfl +register_spec_step nested_round_up_spec + +theorem nested_reference_size_spec : Zerocopy.Specs.nested_reference_size_spec := by + intro leading elem_size leaf_align elems layers hl elemValue he alignmentValue ha metadataValue hn + apply WP.spec_mono (Raw.nested_reference_size_spec leading elem_size leaf_align elems) + intro result hr + refine ⟨result.map unsignedWord, ?_, hr⟩ + cases result <;> rfl +register_spec_step nested_reference_size_spec + +/-- No descriptor bit pattern is excluded by a hidden decoder guard. -/ +theorem nested_layer_decoder_total (raw : layout.nested_reference.NestedLayer) : + isValid raw := by + refine ⟨⟨unsignedWord raw.packed, unsignedWord raw.min_align, + unsignedWord raw.prefix_bytes⟩, ?_⟩ + rfl + +theorem nested_layers_decoder_total (raw : Slice layout.nested_reference.NestedLayer) : + isValid raw := + (slice_valid_iff raw).mpr (fun layer _ => nested_layer_decoder_total layer) + +@[contract_simps] theorem nested_reference_size_spec_implies_required + (leading : Slice layout.nested_reference.NestedLayer) (elem_size leaf_align elems : Usize) + (run : Result (Option Usize)) + (provided : Zerocopy.Specs.nested_reference_size_spec_contract leading elem_size leaf_align elems run) : + Zerocopy.Obligations.nested_reference_size_spec_contract leading elem_size leaf_align elems run := by + obtain ⟨layers, hlayers⟩ := nested_layers_decoder_total leading + have execution := provided layers hlayers (unsignedWord elem_size) rfl + (unsignedWord leaf_align) rfl (unsignedWord elems) rfl + apply WP.spec_mono execution + rintro result ⟨decoded, hdecoded, hr⟩ + exact hr + +@[contract_simps] theorem nested_round_up_spec_implies_required + (size align : Usize) (run : Result (Option Usize)) + (provided : Zerocopy.Specs.nested_round_up_spec_contract size align run) : + Zerocopy.Obligations.nested_round_up_spec_contract size align run := by + have execution := provided (unsignedWord size) rfl (unsignedWord align) rfl + apply WP.spec_mono execution + rintro rounded ⟨decoded, hdecoded, hr⟩ + exact hr + +end Zerocopy.Proofs diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs index c99b48969f..9ad84757f8 100644 --- a/zerocopy/src/layout/mod.rs +++ b/zerocopy/src/layout/mod.rs @@ -9,6 +9,9 @@ // This file may not be copied, modified, or distributed except according to // those terms. +#[allow(dead_code)] +mod nested_reference; + use core::{mem, num::NonZeroUsize}; use crate::util; @@ -2044,7 +2047,7 @@ mod tests { // [2]. Here `prefix` is the end of the preceding fields. // // [6] https://doc.rust-lang.org/1.93.0/reference/type-layout.html#reprc-structs - let offset = prefix.checked_add(util::padding_needed_for(prefix, field_align))?; + let offset = nested_reference::round_up(prefix, field_align.get())?; // `repr(C)` uses the greatest field alignment [6], and an // explicit alignment can only raise it [2]. Here `align` @@ -2056,7 +2059,7 @@ mod tests { // Advance past the complete field, then round to the struct's // alignment, following `repr(C)`'s final sizing steps [6]. size = offset.checked_add(size)?; - size = size.checked_add(util::padding_needed_for(size, alignment))?; + size = nested_reference::round_up(size, alignment.get())?; } // Each enclosing size is at least its field's size. Thus any // checked multiplication or addition that overflowed above would diff --git a/zerocopy/src/layout/nested_reference.rs b/zerocopy/src/layout/nested_reference.rs new file mode 100644 index 0000000000..f13b4e0e10 --- /dev/null +++ b/zerocopy/src/layout/nested_reference.rs @@ -0,0 +1,120 @@ +// 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. + +//! Independent arithmetic for nested `repr(C)` slice DSTs. +//! +//! The layers run from outermost to innermost. Packing caps placement +//! alignment, while every containing layer retains its field's complete size. +//! These descriptors also model arithmetic combinations Rust rejects as types, +//! including simultaneous packing and explicit alignment. No pointer or +//! allocation operation consumes these synthetic layouts. + +// The pinned extraction does not model Option's Try trait. Explicit matches +// also leave the overflow paths visible in this independent reference. +#![allow(clippy::question_mark, clippy::manual_map)] + +/// One containing record, before placing its final field. +/// +/// Plain words make the descriptor's mathematical decoding total. The Rust +/// functions below check the domain explicitly, including zero alignments. +#[derive(Copy, Clone)] +#[cfg_attr(test, derive(Debug))] +pub(super) struct NestedLayer { + pub(super) packed: usize, + pub(super) min_align: usize, + pub(super) prefix_bytes: usize, +} + +/// Returns the least multiple of `align` at least `size`, if representable. +/// +/// Zero alignment returns `None`. The remainder rule is independent of the +/// production padding utility and works for every positive alignment. +/// +/// ```aeneas +/// spec nested_round_up_spec +/// ensures(raw) rounded => rounded.map UScalar.val = +/// if align.val = 0 then none +/// else if LayoutMath.roundUp size.val align.val ≤ Usize.max +/// then some (LayoutMath.roundUp size.val align.val) else none +/// ``` +#[allow(clippy::arithmetic_side_effects)] +pub(super) fn round_up(size: usize, align: usize) -> Option { + if align == 0 { + return None; + } + let remainder = size % align; + if remainder == 0 { + Some(size) + } else { + size.checked_add(align - remainder) + } +} + +fn apply_layer(layer: NestedLayer, size: usize, alignment: usize) -> Option<(usize, usize)> { + if !layer.packed.is_power_of_two() + || !layer.min_align.is_power_of_two() + || layer.min_align > layer.packed + { + return None; + } + let field_align = if alignment < layer.packed { alignment } else { layer.packed }; + let offset = match round_up(layer.prefix_bytes, field_align) { + Some(offset) => offset, + None => return None, + }; + let alignment = if layer.min_align < field_align { field_align } else { layer.min_align }; + let unpadded_size = match offset.checked_add(size) { + Some(size) => size, + None => return None, + }; + let size = match round_up(unpadded_size, alignment) { + Some(size) => size, + None => return None, + }; + Some((size, alignment)) +} + +/// Computes complete recursive size at any element count. +/// +/// `None` means an invalid descriptor or `usize` overflow. An element size of +/// zero is valid at every power-of-two alignment. Sizes above `isize::MAX` +/// remain valid arithmetic results; no allocation is performed here. +/// +/// ```aeneas +/// spec nested_reference_size_spec +/// ensures(raw) result => result.map UScalar.val = +/// NestedReference.checkedSize leading.val elem_size.val leaf_align.val elems.val +/// ``` +#[allow(clippy::arithmetic_side_effects, clippy::indexing_slicing)] +pub(super) fn size_for_metadata( + leading: &[NestedLayer], + elem_size: usize, + leaf_align: usize, + elems: usize, +) -> Option { + if !leaf_align.is_power_of_two() || elem_size % leaf_align != 0 { + return None; + } + let mut state = match elem_size.checked_mul(elems) { + Some(size) => Some((size, leaf_align)), + None => None, + }; + let mut i = leading.len(); + while i != 0 { + i -= 1; + let layer = leading[i]; + state = match state { + Some((size, alignment)) => apply_layer(layer, size, alignment), + None => None, + }; + } + match state { + Some((size, _)) => Some(size), + None => None, + } +}