Compare nested DST sizes with a recursive Rust oracle

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

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

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

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

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