From c02e275edb3cd91d53db87176ca1be5b92bf2bec Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Fri, 2 Oct 2026 10:26:14 -0400 Subject: [PATCH] Specify rounding encodings as alignment and phase The stored nonzero word encodes alignment plus phase, but specs written against that word obscure the operations' meaning. Define a bounded mathematical pair inline on RoundingAlignAndPhase and decode its recursively validated field into a power-of-two alignment and smaller phase. Construct the model from its data fields, completing the omitted proof fields in the decoder's context. Prove exactly which words decode and that successful decoding is equivalent to the stored word equaling alignment plus phase. State constructor and accessor specs in terms of that pair. Retain broader raw lemmas and independent expected contracts to preserve their original representation guarantees. gherrit-pr-id: Grj7aviyzvieawpdu72r5yprrid63scsz Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/README.md | 5 + verification/aeneas/golden/Funs.lean | 66 +++++++ .../aeneas/golden/FunsExternal_Template.lean | 7 + verification/aeneas/golden/Types.lean | 6 + verification/aeneas/lean/LayoutModel.lean | 29 +++ verification/aeneas/lean/MathViews.lean | 22 +++ verification/aeneas/lean/ModelSupport.lean | 56 ++++++ verification/aeneas/lean/Obligations.lean | 30 +++ verification/aeneas/lean/Proofs.lean | 45 ++--- .../aeneas/lean/Proofs/Contracts.lean | 84 ++++++++ .../aeneas/lean/Proofs/Raw/Encoding.lean | 186 ++++++++++++++++++ .../aeneas/lean/RepresentationLaws.lean | 71 +++++++ .../aeneas/lean/RequiredModelContracts.lean | 56 ++++++ .../aeneas/lean/Zerocopy/FunsExternal.lean | 8 + .../aeneas/projections/ModelShapes.lean | 9 + verification/aeneas/projections/Models.lean | 7 + verification/aeneas/projections/Specs.lean | 29 ++- .../aeneas/projections/TraitLaws.lean | 2 +- zerocopy/src/layout/mod.rs | 35 +++- 19 files changed, 721 insertions(+), 32 deletions(-) create mode 100644 verification/aeneas/lean/LayoutModel.lean create mode 100644 verification/aeneas/lean/ModelSupport.lean create mode 100644 verification/aeneas/lean/Proofs/Contracts.lean create mode 100644 verification/aeneas/lean/Proofs/Raw/Encoding.lean create mode 100644 verification/aeneas/lean/RepresentationLaws.lean diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 69e1ebca9e..a73f43c719 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -341,6 +341,11 @@ The mathematical layout semantics proves normalization across arbitrary nesting and metadata values. These algebraic laws do not themselves verify a Rust layout method. +The nominal rounding wrapper decodes to `RoundingValue`, a power-of-two +alignment and bounded phase with machine-fit proofs. Ordinary representation +laws establish acceptance of every positive stored word and exact reconstruction +from that pair. Zero is rejected by the native NonZero child decoder. + 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 c706647675..4527531d04 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -650,6 +650,72 @@ def byteorder.verification.set_u32_be value n byteorder.U32.get byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder value1 +/-- [zerocopy::layout::POINTER_WIDTH_BITS] + Source: 'src/layout/mod.rs', lines 17:0-17: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 -/ +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::RoundingAlignAndPhase}::components]: + Source: 'src/layout/mod.rs', lines 130:4-157:5 -/ +def layout.RoundingAlignAndPhase.components + (self : layout.RoundingAlignAndPhase) : + Result ((core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) × Std.Usize) + := do + let i ← layout.POINTER_WIDTH_BITS + let i1 ← i - 1#usize + let i2 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner self._0 + let i3 ← lift (core.num.Usize.leading_zeros i2) + let i4 ← lift (UScalar.cast .Usize i3) + let shift ← i1 - i4 + let align ← 1#usize <<< shift + let o ← + core.num.nonzero.NonZero.new + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + match o with + | none => fail panic + | some align1 => + let i5 ← + core.num.nonzero.NonZero.get + Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align1 + let phase ← lift (i2 ^^^ i5) + ok (align1, phase) + +/-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::align]: + Source: 'src/layout/mod.rs', lines 170:4-179:5 -/ +def layout.RoundingAlignAndPhase.align + (self : layout.RoundingAlignAndPhase) : + Result (core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner) + := do + let (nz, _) ← layout.RoundingAlignAndPhase.components self + ok nz + /-- [zerocopy::FromZeros::new_zeroed]: Source: 'src/lib.rs', lines 3827:4-3833:5 Visibility: public -/ diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean index 278da9ebb6..ec8aee01f2 100644 --- a/verification/aeneas/golden/FunsExternal_Template.lean +++ b/verification/aeneas/golden/FunsExternal_Template.lean @@ -35,6 +35,13 @@ open Zerocopy @[rust_fun "core::intrinsics::transmute"] axiom core.intrinsics.transmute {Src : Type} (Dst : Type) : Src → Result Dst +/-- [core::mem::size_of]: + Source: '/rustc/library/core/src/mem/mod.rs', lines 375:0-375:34 + Name pattern: [core::mem::size_of] + Visibility: public -/ +@[rust_fun "core::mem::size_of"] +axiom core.mem.size_of (T : Type) : Result Std.Usize + /-- [core::mem::zeroed]: Source: '/rustc/library/core/src/mem/mod.rs', lines 755:0-755:36 Name pattern: [core::mem::zeroed] diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index 752b98e928..cc14d69a72 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -177,6 +177,12 @@ structure byteorder.F64 (O : Type) where _0 : Array Std.U8 8#usize _1 : core.marker.PhantomData O +/-- [zerocopy::layout::RoundingAlignAndPhase] + Source: 'src/layout/mod.rs', lines 78:0-78:54 -/ +structure layout.RoundingAlignAndPhase where + _0 : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner + /-- [zerocopy::wrappers::read_only_def::ReadOnly] Source: 'src/wrappers.rs', lines 630:4-634:5 Visibility: public -/ diff --git a/verification/aeneas/lean/LayoutModel.lean b/verification/aeneas/lean/LayoutModel.lean new file mode 100644 index 0000000000..d2859cdab2 --- /dev/null +++ b/verification/aeneas/lean/LayoutModel.lean @@ -0,0 +1,29 @@ +/- 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 Zerocopy.Funs +public import SpecPrelude +public import LayoutMath +@[expose] public section + +/-! +Extracted trailing records contain machine words and compressed rounding +encodings. This module interprets those records as an unbounded complete-size +formula and a separately observed physical slice offset. Its definitions do +not call an extracted operation or assume that an operation is correct. + +Keeping physical offset separate from normalized base and phase is essential: +inner padding can make them differ. Operation proofs use these observations +to connect extracted arithmetic with the independent layout mathematics. +-/ +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs + + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/MathViews.lean b/verification/aeneas/lean/MathViews.lean index c8d6ed7771..81ad558122 100644 --- a/verification/aeneas/lean/MathViews.lean +++ b/verification/aeneas/lean/MathViews.lean @@ -34,6 +34,9 @@ set_option linter.unusedSimpArgs false -- Raw observations remain available independently of function contracts. -- They record the full positive encoding domain, including arbitrary stored -- words, and do not register a separately selectable validity interpretation. +def encodingValid (code : layout.RoundingAlignAndPhase) : Prop := + 0 < code._0.val.val + @[contract_simps] theorem admission_eq {Raw : Type u} (provider : RustModel Raw) (raw : Raw) : (∃ value, provider.decode raw = some value) = @isValid Raw provider raw := rfl @@ -68,12 +71,22 @@ set_option linter.unusedSimpArgs false @[simp, contract_simps] theorem bool_valid_iff (x : Bool) : isValid x ↔ True := by simp [isValid, RustModel.decode, modelBool] +@[simp, contract_simps] theorem encoding_valid_iff (code : layout.RoundingAlignAndPhase) : + isValid code ↔ encodingValid code := by + by_cases hp : 0 < code._0.val.val <;> + simp [isValid, RustModel.decode, layout.RoundingAlignAndPhase.aeneasModel, + layout.RoundingAlignAndPhase.decode, layout.RoundingAlignAndPhase.decodeFields, + modelNonZeroUScalar, hp, encodingValid] + @[contract_simps] theorem scalar_admitted_iff (x : UScalar ty) : (∃ value, RustModel.decode x = some value) ↔ True := scalar_valid_iff x @[contract_simps] theorem nonzero_admitted_iff (x : NonZeroUsize) : (∃ value, RustModel.decode x = some value) ↔ 0 < x.val.val := nonzero_valid_iff x +@[contract_simps] theorem encoding_admitted_iff (x : layout.RoundingAlignAndPhase) : + (∃ value, RustModel.decode x = some value) ↔ encodingValid x := encoding_valid_iff x + @[contract_simps] theorem bool_admitted_iff (x : Bool) : (∃ value, RustModel.decode x = some value) ↔ True := bool_valid_iff x @@ -86,11 +99,20 @@ set_option linter.unusedSimpArgs false -- A named decoder can also occur after a surrounding structural traversal -- exposes the retained dictionary. These are the same admission equivalences. +@[contract_simps] theorem encoding_decoder_admitted_iff (raw : layout.RoundingAlignAndPhase) : + (∃ value, layout.RoundingAlignAndPhase.decode raw = some value) ↔ + encodingValid raw := encoding_valid_iff raw + @[contract_simps] theorem normalized_nat_pos_iff (n : Nat) : Nat.le (Nat.succ 0) n ↔ 0 < n := Nat.succ_le_iff attribute [contract_simps] option_valid_iff prod_valid_iff result_valid_iff attribute [contract_simps] and_true true_and and_self true_implies forall_true_iff +attribute [contract_simps] encodingValid + +@[simp, contract_simps] theorem rounding_model_decode_eq + (raw : layout.RoundingAlignAndPhase) : + RustModel.decode raw = layout.RoundingAlignAndPhase.decode raw := rfl end Zerocopy.Proofs diff --git a/verification/aeneas/lean/ModelSupport.lean b/verification/aeneas/lean/ModelSupport.lean new file mode 100644 index 0000000000..8359dac865 --- /dev/null +++ b/verification/aeneas/lean/ModelSupport.lean @@ -0,0 +1,56 @@ +/- 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 ModelShapes +import all Mathlib.Data.Nat.Log +import all Init.Data.Nat.Power2.Basic +@[expose] public section + +/-! +The inline rounding decoder constructs a constrained alignment/phase pair. +These ordinary arithmetic lemmas explain why a positive word has the required +components, and why those components are unique. This module imports model +shapes rather than full providers, so it can be available while decoders are +being elaborated. It supplies reusable facts, not a separate certification +duty that every mathematical model must satisfy. +-/ +open Aeneas Aeneas.Std AeneasSpecs + +namespace Zerocopy.RoundingFacts + +/-- A positive word has a unique highest power-of-two bit. -/ +theorem bounds (word : Nat) (positive : 0 < word) : + 2 ^ Nat.log2 word ≤ word ∧ word < 2 ^ (Nat.log2 word + 1) := + (Nat.log2_eq_iff (by omega)).mp rfl + +theorem reconstruction (word : Nat) (positive : 0 < word) : + 2 ^ Nat.log2 word + (word - 2 ^ Nat.log2 word) = word := by + have := bounds word positive + omega + +/-- These are the exact components of every positive encoding, not a restricted +constructor-only subset of the representation domain. -/ +theorem components_unique (word align phase : Nat) + (pow2 : align.isPowerOfTwo) (phase_lt : phase < align) + (encoding : word = align + phase) : + align = 2 ^ Nat.log2 word ∧ phase = word - 2 ^ Nat.log2 word := by + obtain ⟨k, rfl⟩ := pow2 + have positive : 0 < word := by have := Nat.two_pow_pos k; omega + have hk : Nat.log2 word = k := + (Nat.log2_eq_iff (by omega)).mpr (by rw [Nat.pow_succ]; omega) + rw [hk] + omega + +/-- Proof irrelevance makes equality depend only on the observed pair. -/ +@[ext] theorem value_ext + {a b : layout.RoundingAlignAndPhase.RoundingValue} + (ha : a.align = b.align) (hp : a.phase = b.phase) : a = b := by + cases a; cases b; simp_all + +end Zerocopy.RoundingFacts diff --git a/verification/aeneas/lean/Obligations.lean b/verification/aeneas/lean/Obligations.lean index e4d32f4ce8..19453e6e6c 100644 --- a/verification/aeneas/lean/Obligations.lean +++ b/verification/aeneas/lean/Obligations.lean @@ -11,6 +11,7 @@ public import Zerocopy.Funs public import SpecPrelude public import MathViews public import Arithmetic +public import LayoutModel @[expose] public section /-! @@ -77,6 +78,35 @@ def round_down_spec : Prop := ∀ (n : Usize) (align : NonZeroUsize), round_down_spec_contract n align (util.round_down_to_next_multiple_of_alignment n align) +def encoding_new_spec_contract (a : NonZeroUsize) (p : Usize) + (run : Result layout.RoundingAlignAndPhase) : Prop := + 0 < a.val.val → a.val.val.isPowerOfTwo → p.val < a.val.val → + ∃ code, run = .ok code ∧ encodingValid code ∧ code._0.val.val = a.val.val + p.val + +def encoding_new_spec : Prop := + ∀ (a : NonZeroUsize) (p : Usize), + encoding_new_spec_contract a p (layout.RoundingAlignAndPhase.new a p) + +def encoding_components_spec_contract (code : layout.RoundingAlignAndPhase) + (run : Result (NonZeroUsize × Usize)) : Prop := + 0 < code._0.val.val → + run ⦃ (a, p) => + 0 < a.val.val ∧ a.val.val.isPowerOfTwo ∧ p.val < a.val.val ∧ a.val.val + p.val = code._0.val.val ∧ + a.val.val = 2 ^ code._0.val.val.log2 ∧ p.val = code._0.val.val - 2 ^ code._0.val.val.log2 ⦄ + +def encoding_components_spec : Prop := + ∀ (code : layout.RoundingAlignAndPhase), + encoding_components_spec_contract code (layout.RoundingAlignAndPhase.components code) + +def encoding_align_spec_contract (code : layout.RoundingAlignAndPhase) + (run : Result NonZeroUsize) : Prop := + 0 < code._0.val.val → + ∃ a, run = .ok a ∧ 0 < a.val.val ∧ a.val.val = 2 ^ code._0.val.val.log2 + +def encoding_align_spec : Prop := + ∀ (code : layout.RoundingAlignAndPhase), + encoding_align_spec_contract code (layout.RoundingAlignAndPhase.align code) + end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs.lean b/verification/aeneas/lean/Proofs.lean index 73b1676b10..8770d7e502 100644 --- a/verification/aeneas/lean/Proofs.lean +++ b/verification/aeneas/lean/Proofs.lean @@ -7,40 +7,27 @@ This file may not be copied, modified, or distributed except according to those terms. -/ module -public import Specs +public import Proofs.Contracts public import Proofs.Util -public import Aeneas -public import Loops -public import LayoutMath -import all Mathlib.Data.Nat.Log -import all Init.Data.Nat.Power2.Basic @[expose] public section /-! -This is the import root for contracts proved about actual Aeneas function -definitions. Proofs.Util supplies the arithmetic theorems: its Raw namespace -steps through the extracted computations, then canonical theorems prove the -generated Specs propositions, including input and result decoding. +This module proves contracts about the actual Aeneas function definitions. +The Raw namespace steps through extracted control flow and machine +arithmetic. Those lemmas deliberately retain useful representation domains, +even when an inline specification admits a smaller domain through automatic +decoding. + +The canonical theorems outside Raw prove the generated Specs propositions. +They use the raw lemmas, decode accepted inputs, and establish that the +actual returned representation decodes and has the requested mathematical +properties. WP.spec_mono transfers a proved computation to a new +postcondition; it cannot replace that computation. Registered specifications +let later proofs reuse a callee's theorem instead of unfolding its +implementation each time. Aeneas Result describes execution success, panic, or divergence. Rust Option -and Rust Result values may themselves be successful payloads. These cases -have different meanings and must remain distinct in function contracts. +and Rust Result values may themselves be successful payloads. The proof must +keep these cases distinct. -/ open Aeneas Aeneas.Std -namespace Zerocopy.Proofs.Raw - -set_option linter.unusedVariables false - - -end Zerocopy.Proofs.Raw - -namespace Zerocopy.Proofs -open AeneasSpecs - - -end Zerocopy.Proofs - -namespace Zerocopy.Proofs -open AeneasSpecs - -end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Proofs/Contracts.lean b/verification/aeneas/lean/Proofs/Contracts.lean new file mode 100644 index 0000000000..05c6b9e850 --- /dev/null +++ b/verification/aeneas/lean/Proofs/Contracts.lean @@ -0,0 +1,84 @@ +/- 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.Encoding +@[expose] public section + +open Aeneas Aeneas.Std + +namespace Zerocopy.Proofs +open AeneasSpecs + +-- Unfold only representation domains. The model calls and authored outcome +-- predicates remain the independently verified raw contracts below. +macro "representation_simps" : tactic => + `(tactic| + (simp only [WP.spec_equiv_exists] + simp (config := { index := false }) only [contract_simps] + simp only [← WP.spec_equiv_exists])) + +/- Connect the constructor's power-of-two and phase checks to exact encoding. +The canonical form also proves decoding of the actual returned word. +-/ +theorem encoding_new_spec : Zerocopy.Specs.encoding_new_spec := by + intro align phase av ha pv hp hpow hphase + have hav := (decodeNonZeroUScalar_iff align av).mp ha + have hpv := (decodeUScalar_iff phase pv).mp hp + apply WP.spec_mono (Raw.encoding_new_spec align phase + (by simpa only [hav] using hpow) (by simpa only [hav, hpv] using hphase)) + intro encoded he + have hfit : av.value + pv.value ≤ Usize.max := by + rw [← hav, ← hpv, ← he] + scalar_tac + let value : layout.RoundingAlignAndPhase.RoundingValue := + ⟨av.value, pv.value, hpow, hphase, hfit⟩ + refine ⟨value, (rounding_decode_iff encoded value).mpr ?_, rfl, rfl⟩ + simpa only [roundingRepresents, value, hav, hpv] using he +register_spec_step encoding_new_spec + +/- Prove the implementation's bit scan recovers the alignment and phase of every +positive stored word, not only words built by the constructor. +-/ +theorem encoding_components_spec : Zerocopy.Specs.encoding_components_spec := by + intro self value decoded + have hn := (encoding_valid_iff self).mp ⟨value, decoded⟩ + have hvalue := rounding_decode_components self value decoded + apply WP.spec_mono (Raw.encoding_components_spec self hn) + rintro ⟨align, phase⟩ facts + let av : NonZeroUsizeValue := + ⟨unsignedWord align.val, Nat.pos_of_isPowerOfTwo facts.1⟩ + have ha : modelNonZeroUsize.decode align = some av := + (decodeNonZeroUScalar_iff align av).mpr rfl + refine ⟨(av, unsignedWord phase), ?_, ?_⟩ + · simp only [RustModel.decode, + dif_pos (Nat.pos_of_isPowerOfTwo facts.1)] + rfl + · exact ⟨facts.2.2.2.1.trans hvalue.1.symm, + facts.2.2.2.2.trans hvalue.2.symm⟩ +register_spec_step encoding_components_spec + +/- Reuse the components theorem for the getter that discards phase. +-/ +theorem encoding_align_spec : Zerocopy.Specs.encoding_align_spec := by + intro self value decoded + have hn := (encoding_valid_iff self).mp ⟨value, decoded⟩ + have hvalue := rounding_decode_components self value decoded + apply WP.spec_mono (Raw.encoding_align_spec self hn) + intro align he + have hp : 0 < align.val.val := by rw [he]; exact Nat.two_pow_pos _ + let av : NonZeroUsizeValue := ⟨unsignedWord align.val, hp⟩ + exact ⟨av, (decodeNonZeroUScalar_iff align av).mpr rfl, he.trans hvalue.1.symm⟩ +register_spec_step encoding_align_spec + +end Zerocopy.Proofs + +namespace Zerocopy.Proofs +open AeneasSpecs + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Proofs/Raw/Encoding.lean b/verification/aeneas/lean/Proofs/Raw/Encoding.lean new file mode 100644 index 0000000000..eb0718d347 --- /dev/null +++ b/verification/aeneas/lean/Proofs/Raw/Encoding.lean @@ -0,0 +1,186 @@ +/- 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 Proofs.Util +public import Aeneas +public import Loops +public import RepresentationLaws +public import LayoutMath +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 +/- Read the pinned platform's pointer width through its modeled primitive. This +establishes the runtime constant used by encoding and packing arithmetic. +-/ +theorem pointer_width_spec : + layout.POINTER_WIDTH_BITS + ⦃ w => w.val = System.Platform.numBits ⦄ := by + unfold layout.POINTER_WIDTH_BITS + simp only [core.mem.size_of, ite_true, bind_ok] + have hv : ({ bv := BitVec.ofNat _ (System.Platform.numBits / 8) } : Usize).val = + System.Platform.numBits / 8 := by + change (System.Platform.numBits / 8) % 2 ^ System.Platform.numBits = _ + rcases System.Platform.numBits_eq with h | h <;> simp only [h] <;> decide + step as ⟨w, hw⟩ + · rw [hv] + rcases System.Platform.numBits_eq with h | h <;> + simp only [Usize.max, Usize.numBits, UScalarTy.Usize_numBits_eq, h, + UScalar.val] <;> decide + · rw [hv] at hw + rcases System.Platform.numBits_eq with h | h <;> + simp only [h] at hw ⊢ <;> omega + +/- Connect the constructor's power-of-two and phase checks to exact encoding. +The canonical form also proves decoding of the actual returned word. +-/ +theorem encoding_new_spec : + ∀ (align : NonZeroUsize) (phase : Usize), ∀ (ha : (align.val.val.isPowerOfTwo : Prop)), ∀ (hp : (phase.val < align.val.val : Prop)), + @Zerocopy.layout.RoundingAlignAndPhase.new align phase ⦃ encoded => encoded._0.val.val = align.val.val + phase.val ⦄ := by + intro align phase ha hp + unfold layout.RoundingAlignAndPhase.new + 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 [ha] using hb + exact Eq.mpr hb' trivial + simp only [massert, hbt, if_true, bind_ok, UScalar.lt_equiv, hp, lift] + obtain ⟨k, hk⟩ := ha + have hor : (align.val ||| phase).val = align.val.val + phase.val := by + rw [UScalar.val_or, hk] + have h := Nat.two_pow_add_eq_or_of_lt (show phase.val < 2 ^ k by omega) 1 + simpa only [Nat.mul_one] using h.symm + have hnz : align.val ||| phase ≠ 0#usize := by + intro hz + have hz' := congrArg UScalar.val hz + rw [hor] at hz' + have hpos := Nat.two_pow_pos k + change align.val.val + phase.val = 0 at hz' + omega + simp only [core.num.nonzero.NonZero.new, cast_eq, hnz, ↓reduceDIte, ↓reduceIte, + bind_ok, WP.spec_ok] + exact hor + +/- Remove the highest bit from align + phase when phase uses only lower bits. +The decoder implementation uses XOR; the mathematical model uses subtraction. +-/ +theorem highest_bit_xor (k p : Nat) (hp : p < 2 ^ k) : (2 ^ k + p) ^^^ 2 ^ k = p := by + have hjoin : 2 ^ k + p = 2 ^ k ||| p := by + simpa only [Nat.mul_one] using Nat.two_pow_add_eq_or_of_lt hp 1 + rw [hjoin] + apply Nat.eq_of_testBit_eq + intro i + rw [Nat.testBit_xor, Nat.testBit_or] + by_cases hi : i = k + · subst i + rw [Nat.testBit_two_pow_self, Nat.testBit_lt_two_pow hp] + rfl + · rw [Nat.testBit_two_pow_of_ne (Ne.symm hi)] + simp + +/- Prove the implementation's bit scan recovers the alignment and phase of every +positive stored word, not only words built by the constructor. +-/ +theorem encoding_components_spec : + ∀ (self : layout.RoundingAlignAndPhase), ∀ (hn : (0 < self._0.val.val : Prop)), + @Zerocopy.layout.RoundingAlignAndPhase.components self ⦃ (align, phase) => + align.val.val.isPowerOfTwo ∧ phase.val < align.val.val ∧ + align.val.val + phase.val = self._0.val.val ∧ + align.val.val = 2 ^ Nat.log2 self._0.val.val ∧ + phase.val = self._0.val.val - 2 ^ Nat.log2 self._0.val.val ⦄ := by + intro self hn + let k := Nat.log2 self._0.val.val + have hbound := (Nat.log2_eq_iff (show self._0.val.val ≠ 0 by omega)).mp (show Nat.log2 self._0.val.val = k from rfl) + have hsize := UScalar.hSize self._0.val + rw [UScalar.size, UScalarTy.Usize_numBits_eq] at hsize + have hk : k < System.Platform.numBits := by + dsimp [k] + rw [Nat.log2_eq_log_two] + apply Nat.log_lt_of_lt_pow (by omega) + exact hsize + have hbits : 32 ≤ System.Platform.numBits := by + rcases System.Platform.numBits_eq with h | h <;> omega + have hnzbv : self._0.val.bv ≠ 0 := by + intro h + have := congrArg BitVec.toNat h + change self._0.val.val = 0 at this + omega + have hlz : (core.num.Usize.leading_zeros self._0.val).val = System.Platform.numBits - k - 1 := by + change (BitVec.leadingZeros self._0.val.bv) % 2 ^ 32 = _ + unfold BitVec.leadingZeros + rw [if_neg hnzbv] + change (System.Platform.numBits - Nat.log 2 self._0.val.val - 1) % 2 ^ 32 = _ + rw [← Nat.log2_eq_log_two] + apply Nat.mod_eq_of_lt + rcases System.Platform.numBits_eq with h | h <;> rw [h] <;> omega + have hcast : (UScalar.cast .Usize (core.num.Usize.leading_zeros self._0.val)).val = + System.Platform.numBits - k - 1 := by + rw [UScalar.cast_val_eq, hlz, UScalarTy.Usize_numBits_eq] + apply Nat.mod_eq_of_lt + rcases System.Platform.numBits_eq with h | h <;> rw [h] <;> omega + unfold layout.RoundingAlignAndPhase.components + step with pointer_width_spec as ⟨w, hw⟩ + have hone : (1#usize).val = 1 := by simp + have hwpos : (1#usize).val ≤ w.val := by rw [hone, hw]; omega + step with Usize.sub_spec hwpos as ⟨w1, hw1, _⟩ + simp only [core.num.nonzero.NonZero.get, bind_ok, lift] + have hsub : (UScalar.cast .Usize (core.num.Usize.leading_zeros self._0.val)).val ≤ w1.val := by + rw [hcast, hw1, hw] + omega + step with Usize.sub_spec hsub as ⟨shift, hshift, _⟩ + have hshift' : shift.val = k := by rw [hcast, hw1, hw] at hshift; omega + step with Usize.ShiftLeft_spec 1#usize shift (by rw [hshift']; exact hk) as ⟨a, ha, _⟩ + have ha' : a.val = 2 ^ k := by + rw [hshift'] at ha + simp only [Nat.shiftLeft_eq, Nat.one_mul] at ha + have hp : 2 ^ k < Usize.size := by + rw [Usize.size, Usize.numBits, UScalarTy.Usize_numBits_eq] + omega + simpa only [Nat.mod_eq_of_lt hp] using ha + have haz : a ≠ 0#usize := by + intro hz + have hz' := congrArg UScalar.val hz + rw [ha'] at hz' + change 2 ^ k = 0 at hz' + have := Nat.two_pow_pos k + omega + simp only [core.num.nonzero.NonZero.new, cast_eq, haz, ↓reduceDIte, + ↓reduceIte, bind_ok, WP.spec_ok] + have hp : self._0.val.val - 2 ^ k < 2 ^ k := by + rw [Nat.pow_succ] at hbound + omega + have hx : (self._0.val ^^^ a).val = self._0.val.val - 2 ^ k := by + rw [UScalar.val_xor, ha'] + have heq : self._0.val.val = 2 ^ k + (self._0.val.val - 2 ^ k) := by omega + rw [heq] + simpa only [Nat.add_sub_cancel_left] using highest_bit_xor k _ hp + refine ⟨?_, ?_, ?_, ha', ?_⟩ + · exact ⟨k, ha'⟩ + · rw [hx, ha'] + exact hp + · rw [hx, ha'] + omega + · exact hx + +/- Reuse the components theorem for the getter that discards phase. +-/ +theorem encoding_align_spec : + ∀ (self : layout.RoundingAlignAndPhase), ∀ (hn : (0 < self._0.val.val : Prop)), + @Zerocopy.layout.RoundingAlignAndPhase.align self ⦃ align => align.val.val = 2 ^ Nat.log2 self._0.val.val ⦄ := by + intro self hn + unfold layout.RoundingAlignAndPhase.align + step with encoding_components_spec self hn as ⟨a, p, _, _, _, ha, _⟩ + simpa only [WP.spec_ok] using ha + +end Zerocopy.Proofs.Raw diff --git a/verification/aeneas/lean/RepresentationLaws.lean b/verification/aeneas/lean/RepresentationLaws.lean new file mode 100644 index 0000000000..3c110a6e11 --- /dev/null +++ b/verification/aeneas/lean/RepresentationLaws.lean @@ -0,0 +1,71 @@ +/- 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 MathViews +public import ModelSupport +@[expose] public section + +/-! +Rounding operation proofs need to relate an observed pair to its stored word. +The lemmas here expose that particular decoder's equations and positive +domain. They are useful because this encoding is reversible; the integration +does not require every model to be reversible or to retain every +representation detail. A coarse model can be appropriate when its operation +contracts need no more. Decoder construction proves the model's constraints, +while these lemmas describe what this decoder actually computes. +-/ +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +/-- The stored word represents exactly the sum of the observed pair. -/ +def roundingRepresents (raw : layout.RoundingAlignAndPhase) + (value : layout.RoundingAlignAndPhase.RoundingValue) : Prop := + raw._0.val.val = value.align + value.phase + +theorem rounding_decode_positive (raw : layout.RoundingAlignAndPhase) + (positive : 0 < raw._0.val.val) : + ∃ value, layout.RoundingAlignAndPhase.decode raw = some value := + (encoding_valid_iff raw).mpr positive + +theorem rounding_decode_components (raw : layout.RoundingAlignAndPhase) + (value : layout.RoundingAlignAndPhase.RoundingValue) + (h : layout.RoundingAlignAndPhase.decode raw = some value) : + value.align = 2 ^ Nat.log2 raw._0.val.val ∧ + value.phase = raw._0.val.val - 2 ^ Nat.log2 raw._0.val.val := by + have positive : 0 < raw._0.val.val := + (encoding_valid_iff raw).mp ⟨value, h⟩ + simp [layout.RoundingAlignAndPhase.decode, layout.RoundingAlignAndPhase.decodeFields, + RustModel.decode, positive, unsignedWord] at h + cases h + exact ⟨rfl, rfl⟩ + +theorem rounding_decode_iff (raw : layout.RoundingAlignAndPhase) + (value : layout.RoundingAlignAndPhase.RoundingValue) : + layout.RoundingAlignAndPhase.decode raw = some value ↔ roundingRepresents raw value := by + constructor + · intro h + obtain ⟨ha, hp⟩ := rounding_decode_components raw value h + have positive := (encoding_valid_iff raw).mp ⟨value, h⟩ + unfold roundingRepresents + rw [ha, hp] + exact (RoundingFacts.reconstruction _ positive).symm + · intro h + have positive : 0 < raw._0.val.val := by + have := Nat.pos_of_isPowerOfTwo value.align_pow2 + unfold roundingRepresents at h + omega + obtain ⟨actual, decoded⟩ := rounding_decode_positive raw positive + obtain ⟨ha, hp⟩ := rounding_decode_components raw actual decoded + have unique := RoundingFacts.components_unique raw._0.val.val value.align value.phase + value.align_pow2 value.phase_lt h + have equal : actual = value := RoundingFacts.value_ext + (ha.trans unique.1.symm) (hp.trans unique.2.symm) + simpa only [equal] using decoded + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RequiredModelContracts.lean b/verification/aeneas/lean/RequiredModelContracts.lean index f845f2fb68..a3051dee3c 100644 --- a/verification/aeneas/lean/RequiredModelContracts.lean +++ b/verification/aeneas/lean/RequiredModelContracts.lean @@ -8,6 +8,7 @@ those terms. -/ module public import RequiredModelContracts.Util +public import RepresentationLaws @[expose] public section /-! @@ -25,4 +26,59 @@ proved implications available to check_contract's bounded normalization. open Aeneas Aeneas.Std AeneasSpecs namespace Zerocopy.Proofs +attribute [contract_simps] encoding_decoder_admitted_iff + +@[contract_simps] theorem required_encoding_new (align : NonZeroUsize) (phase : Usize) + (run : Result layout.RoundingAlignAndPhase) + (provided : Specs.encoding_new_spec_contract align phase run) : + Obligations.encoding_new_spec_contract align phase run := by + intro positive pow2 below + let av : NonZeroUsizeValue := ⟨unsignedWord align.val, positive⟩ + have admitted := (decodeNonZeroUScalar_iff align av).mpr rfl + have result := provided av admitted (unsignedWord phase) rfl pow2 below + simp only [WP.spec_equiv_exists] at result + obtain ⟨raw, call, value, decoded, ha, hp⟩ := result + refine ⟨raw, call, ?_, ?_⟩ + · exact (encoding_valid_iff raw).mp ⟨value, decoded⟩ + · have represents := (rounding_decode_iff raw value).mp decoded + simpa only [roundingRepresents, ha, hp, av, unsignedWord] using represents + +@[contract_simps] theorem required_encoding_align (raw : layout.RoundingAlignAndPhase) + (run : Result NonZeroUsize) + (provided : Specs.encoding_align_spec_contract raw run) : + Obligations.encoding_align_spec_contract raw run := by + intro positive + obtain ⟨value, decoded⟩ := rounding_decode_positive raw positive + have result := provided value decoded + simp only [WP.spec_equiv_exists] at result + obtain ⟨align, call, av, admitted, facts⟩ := result + have same := (decodeNonZeroUScalar_iff align av).mp admitted + exact ⟨align, call, by rw [same]; exact av.positive, + same.trans (facts.trans (rounding_decode_components raw value decoded).1)⟩ + +@[contract_simps] theorem required_encoding_components (raw : layout.RoundingAlignAndPhase) + (run : Result (NonZeroUsize × Usize)) + (provided : Specs.encoding_components_spec_contract raw run) : + Obligations.encoding_components_spec_contract raw run := by + intro positive + obtain ⟨value, decoded⟩ := rounding_decode_positive raw positive + apply WP.spec_mono (provided value decoded) + rintro ⟨align, phase⟩ ⟨pair, admitted, ha, hp⟩ + have positiveAlign : 0 < align.val.val := + (nonzero_valid_iff align).mp ((prod_valid_iff (align, phase)).mp ⟨pair, admitted⟩).1 + have pairEq : ((⟨unsignedWord align.val, positiveAlign⟩ : NonZeroUsizeValue), + unsignedWord phase) = pair := by + simpa only [RustModel.decode, dif_pos positiveAlign, Option.some.injEq] using admitted + cases pairEq + dsimp only [unsignedWord] at ha hp + have hraw := (rounding_decode_iff raw value).mp decoded + have hcanonical := rounding_decode_components raw value decoded + change 0 < align.val.val ∧ align.val.val.isPowerOfTwo ∧ + phase.val < align.val.val ∧ align.val.val + phase.val = raw._0.val.val ∧ + align.val.val = 2 ^ raw._0.val.val.log2 ∧ + phase.val = raw._0.val.val - 2 ^ raw._0.val.val.log2 + rw [ha, hp] + exact ⟨Nat.pos_of_isPowerOfTwo value.align_pow2, value.align_pow2, value.phase_lt, + hraw.symm, hcanonical.1, hcanonical.2⟩ + end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Zerocopy/FunsExternal.lean b/verification/aeneas/lean/Zerocopy/FunsExternal.lean index 89b3bc79de..559024360d 100644 --- a/verification/aeneas/lean/Zerocopy/FunsExternal.lean +++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean @@ -159,6 +159,14 @@ def core.intrinsics.transmute {Src : Type} (Dst : Type) {T Inner : Type} (_inst : core.num.nonzero.ZeroablePrimitive T Inner) (x : core.num.nonzero.NonZero T Inner) : Result T := .ok x.val +-- Extraction uses size_of only for usize to calculate its bit width. Other +-- types remain unsupported rather than receiving arbitrary layout values. +@[simp] noncomputable def core.mem.size_of (T : Type) : Result Usize := by + classical + exact if T = Usize then + .ok { bv := BitVec.ofNat _ (System.Platform.numBits / 8) } + else .fail .panic + -- The extracted call sites instantiate this primitive only at Usize. Other -- types are unsupported, so the model cannot promise a recoverable panic. @[simp] noncomputable def core.num.nonzero.NonZero.new diff --git a/verification/aeneas/projections/ModelShapes.lean b/verification/aeneas/projections/ModelShapes.lean index f895a7a7e7..c4f02965d4 100644 --- a/verification/aeneas/projections/ModelShapes.lean +++ b/verification/aeneas/projections/ModelShapes.lean @@ -44,6 +44,15 @@ derive_model_shape Zerocopy.byteorder.F32 with 1 type parameters derive_model_shape Zerocopy.byteorder.F64 with 1 type parameters +aeneas_model_shape Zerocopy.layout.RoundingAlignAndPhase with 0 type parameters begin +model RoundingValue where + align : Nat + phase : Nat + align_pow2 : align.isPowerOfTwo + phase_lt : phase < align + fits : align + phase ≤ Usize.max +end + derive_model_shape Zerocopy.wrappers.read_only_def.ReadOnly with 1 type parameters derive_model_shape Zerocopy.pointer.invariant.Initialized with 0 type parameters diff --git a/verification/aeneas/projections/Models.lean b/verification/aeneas/projections/Models.lean index 9549d5bc97..b2c5c98358 100644 --- a/verification/aeneas/projections/Models.lean +++ b/verification/aeneas/projections/Models.lean @@ -9,6 +9,7 @@ those terms. -/ module public import ModelShapes public import DeriveModels +public import ModelSupport @[expose] public section open Aeneas Aeneas.Std AeneasSpecs @@ -58,6 +59,12 @@ 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.RoundingAlignAndPhase with 0 type parameters decode self => + let word := self._0.value + let align := 2 ^ Nat.log2 word + { align := align, phase := word - align, .. } +check_model_binding Zerocopy.layout.RoundingAlignAndPhase with 0 type parameters + derive_rust_model Zerocopy.wrappers.read_only_def.ReadOnly with 1 type parameters with_physical 0 check_model_binding Zerocopy.wrappers.read_only_def.ReadOnly with 1 type parameters diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index 828f957bfc..3b46caa8e8 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/verification/aeneas/projections/Specs.lean @@ -11,7 +11,7 @@ public import Zerocopy.Funs public import SpecPrelude public import SpecsSyntax public import Models -public import Arithmetic +public import LayoutModel public import TraitLaws @[expose] public section @@ -123,6 +123,33 @@ 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.RoundingAlignAndPhase.new with 0 type parameters +aeneas_spec_begin +spec encoding_new_spec + for @Zerocopy.layout.RoundingAlignAndPhase.new with 0 type parameters + requires ha : (align : Nat).isPowerOfTwo + requires hp : (phase : Nat) < (align : Nat) + ensures encoded => encoded.align = (align : Nat) ∧ encoded.phase = (phase : Nat) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.encoding_new_spec for Zerocopy.layout.RoundingAlignAndPhase.new with 2 + +check_model_inputs Zerocopy.layout.RoundingAlignAndPhase.components with 0 type parameters +aeneas_spec_begin +spec encoding_components_spec + for @Zerocopy.layout.RoundingAlignAndPhase.components with 0 type parameters + ensures (align, phase) => + align.value = self.align ∧ phase.value = self.phase +aeneas_spec_end +check_spec_binding Zerocopy.Specs.encoding_components_spec for Zerocopy.layout.RoundingAlignAndPhase.components with 1 + +check_model_inputs Zerocopy.layout.RoundingAlignAndPhase.align with 0 type parameters +aeneas_spec_begin +spec encoding_align_spec + for @Zerocopy.layout.RoundingAlignAndPhase.align with 0 type parameters + ensures align => (align : Nat) = self.align +aeneas_spec_end +check_spec_binding Zerocopy.Specs.encoding_align_spec for Zerocopy.layout.RoundingAlignAndPhase.align with 1 + default_trait_body Zerocopy.FromZeros.new_zeroed.default for Zerocopy.FromZeros with 1 type parameters check_model_inputs Zerocopy.FromZeros.new_zeroed.default with 1 type parameters aeneas_spec_begin diff --git a/verification/aeneas/projections/TraitLaws.lean b/verification/aeneas/projections/TraitLaws.lean index 1abd631a86..5bdff2c8c2 100644 --- a/verification/aeneas/projections/TraitLaws.lean +++ b/verification/aeneas/projections/TraitLaws.lean @@ -9,7 +9,7 @@ those terms. -/ module public import Zerocopy.Funs public import TraitLawsSupport -public import Arithmetic +public import LayoutModel @[expose] public section open Aeneas Aeneas.Std namespace Zerocopy.TraitLaws diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs index d20ae69d15..51b007e692 100644 --- a/zerocopy/src/layout/mod.rs +++ b/zerocopy/src/layout/mod.rs @@ -58,6 +58,19 @@ pub(crate) enum SizeInfo { /// ```text /// encoded = align + phase /// ``` +/// +/// ```aeneas +/// model RoundingValue where +/// align : Nat +/// phase : Nat +/// align_pow2 : align.isPowerOfTwo +/// phase_lt : phase < align +/// fits : align + phase ≤ Usize.max +/// decode self => +/// let word := self._0.value +/// let align := 2 ^ Nat.log2 word +/// { align := align, phase := word - align, .. } +/// ``` #[cfg_attr(any(kani, test), derive(Debug, PartialEq, Eq))] #[repr(transparent)] #[derive(Copy, Clone)] @@ -69,11 +82,18 @@ impl RoundingAlignAndPhase { /// /// # Panics /// - /// Panics if `align` is not a power of two and `phase` is not less than + /// Panics if `align` is not a power of two or `phase` is not less than /// `align`. #[inline(always)] #[cfg_attr(kani, kani::requires(align.is_power_of_two() && phase < align.get()))] #[cfg_attr(kani, kani::ensures(|result| result.0.get() == align.get() + phase))] + /// + /// ```aeneas + /// spec encoding_new_spec + /// requires ha : (align : Nat).isPowerOfTwo + /// requires hp : (phase : Nat) < (align : Nat) + /// ensures encoded => encoded.align = (align : Nat) ∧ encoded.phase = (phase : Nat) + /// ``` pub(crate) const fn new(align: NonZeroUsize, phase: usize) -> Self { #[cfg(kani)] #[kani::proof_for_contract(RoundingAlignAndPhase::new)] @@ -101,6 +121,12 @@ impl RoundingAlignAndPhase { align.is_power_of_two() && phase < align.get() && align.get().checked_add(phase) == Some(self.0.get()) }))] + /// + /// ```aeneas + /// spec encoding_components_spec + /// ensures (align, phase) => + /// align.value = self.align ∧ phase.value = self.phase + /// ``` pub(crate) const fn components(self) -> (NonZeroUsize, usize) { #[cfg(kani)] #[kani::proof_for_contract(RoundingAlignAndPhase::components)] @@ -111,6 +137,7 @@ impl RoundingAlignAndPhase { // `leading_zeros <= POINTER_WIDTH_BITS - 1` because the encoded value // is non-zero. Converting `leading_zeros` to `usize` cannot truncate // because it is at most the number of bits in a `usize`. + // Keep the primitive usize operation visible to Aeneas. #[allow( clippy::arithmetic_side_effects, clippy::as_conversions, @@ -135,6 +162,11 @@ impl RoundingAlignAndPhase { align.is_power_of_two() && align.get() <= self.0.get() && self.0.get() - align.get() < align.get() }))] + /// + /// ```aeneas + /// spec encoding_align_spec + /// ensures align => (align : Nat) = self.align + /// ``` pub(crate) const fn align(self) -> NonZeroUsize { #[cfg(kani)] #[kani::proof_for_contract(RoundingAlignAndPhase::align)] @@ -2434,6 +2466,7 @@ mod tests { assert_eq!(max.components().1, max_phase); assert_eq!(mem::size_of::(), 4 * mem::size_of::()); + assert_eq!(mem::size_of::(), mem::size_of::()); } #[test]