From 37524f6dc865efd4ff846615e3a6b9770140ee7b Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Fri, 2 Oct 2026 10:26:14 -0400 Subject: [PATCH] Model alignment and phase encoding as a bounded mathematical pair Retain the nominal Rust wrapper and define its mathematical model inline. Decode its already-positive NonZero field into alignment and phase with power-of-two, phase-bound and representability proofs. Prove the accepted domain, representation relation and round trips independently of method proofs. Encoding and decoding specifications use the mathematical pair; broad Raw lemmas preserve the original representation guarantees. Construct the rounding model using only its data fields; decoder-scoped completion proves its unchanged constraints in the construction context. Independent meaning, admission and round-trip guarantees remain explicit. Retain code-generation failure diagnostics that show the expected and actual snapshots and report every benchmark worker failure. Validation: fresh pinned extraction, complete golden comparison, separate golden/live builds, independent required contracts and axiom audits. gherrit-pr-id: Gng7s74f35a4f6jjd5xjjmvxbwqqnnx7q Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/README.md | 30 ++- verification/aeneas/golden/Funs.lean | 66 +++++ .../aeneas/golden/FunsExternal_Template.lean | 18 ++ 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 | 243 +++++++++++++++++- .../aeneas/lean/RepresentationLaws.lean | 71 +++++ .../aeneas/lean/RequiredModelContracts.lean | 56 ++++ .../aeneas/lean/Zerocopy/FunsExternal.lean | 17 ++ zerocopy/src/layout/mod.rs | 35 ++- 13 files changed, 662 insertions(+), 17 deletions(-) create mode 100644 verification/aeneas/lean/LayoutModel.lean create mode 100644 verification/aeneas/lean/ModelSupport.lean create mode 100644 verification/aeneas/lean/RepresentationLaws.lean diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index d3cd54e975..46b8f19d5c 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -68,8 +68,9 @@ each tool answers a different question: The extracted model and the mathematical model have different purposes. The first represents the computation we prove properties about; the second supplies -the vocabulary in which we state those properties. For example, a Rust nonzero word -is interpreted as a natural number with machine bounds and a proof of positivity. Plain clauses use mathematical values; `(raw)` +the vocabulary in which we state those properties. For example, Rust stores +rounding alignment and phase in one nonzero word, while its mathematical model +exposes two natural numbers. Plain clauses use mathematical values; `(raw)` clauses use extracted representations. Both execute the same extracted function on its original arguments and require the actual returned value to decode. @@ -134,6 +135,7 @@ added without extending the specification set. | `min` | Returns the mathematical minimum, selects an input, and bounds both inputs from below. | | `padding_needed_for` | For power-of-two alignment, returns padding below it and exactly `(align - len % align) % align`, the least padding making the sum aligned, with zero padding exactly when the input is aligned. | | `round_down_to_next_multiple_of_alignment` | For power-of-two alignment, returns exactly `n - n % align`, the greatest aligned value at most `n`; the next multiple exceeds `n`. | +| Alignment/phase encoder and decoders | Power-of-two alignment, bounded phase, and exact encoding round-trip. | Every registered function uses total `spec`: accepted raw representations, supplied mathematical ghosts, and explicit requirements imply successful @@ -151,6 +153,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 NonZero positivity. Their Nat/Int arithmetic does not wrap; explicit raw clauses preserve the extracted representation vocabulary while retaining @@ -336,7 +343,7 @@ comparison is part of the automatic-decoding audit. Generated modules follow the proof-construction dependency: ```text -raw Types + ModelPrelude → ModelShapes → Models → Specs + Proofs +raw Types + ModelPrelude → ModelShapes → ModelSupport → Models → Specs + Proofs ``` `ModelShapes` declares nominal mathematical fields and inline model types in @@ -472,14 +479,17 @@ modules must not create import cycles through generated `Required` or `Check`. Model fields declare ordinary Lean constraints. A decoder can supply only its data and use native `..` to omit proof fields: -For a hypothetical type with a machine-word field `word`: - ```lean -model SuccessorValue where - value : Nat - positive : 0 < value +model RoundingValue where + align : Nat + phase : Nat + align_pow2 : align.isPowerOfTwo + phase_lt : phase < align + fits : align + phase ≤ Usize.max decode self => - { value := self.word.value + 1, .. } + let word := self._0.value + let align := 2 ^ Nat.log2 word + { align := align, phase := word - align, .. } ``` Both `decode` and `decode?` implicitly use `model_value` completion on the whole @@ -560,7 +570,7 @@ After a Lake build, inspect an effective compiled specification with: ```sh python3 -B verification/aeneas/workspace.py inspect verification/aeneas/lean \ - --root "$PWD" --spec max_spec + --root "$PWD" --spec encoding_components_spec ``` This reads compiled declarations without running another build. It displays the diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index 6bee28d103..f8dad1e701 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -642,6 +642,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::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/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean index ccb87a43d6..03f8eb3085 100644 --- a/verification/aeneas/golden/FunsExternal_Template.lean +++ b/verification/aeneas/golden/FunsExternal_Template.lean @@ -28,6 +28,13 @@ set_option maxHeartbeats 1000000 set_option maxRecDepth 2048 open Zerocopy +/-- [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::num::niche_types::{impl core::clone::Clone for core::num::niche_types::NonZeroUsizeInner}::clone]: Source: '/rustc/library/core/src/num/niche_types.rs', lines 17:17-17:22 Name pattern: [core::num::niche_types::{core::clone::Clone}::clone] @@ -39,6 +46,17 @@ axiom core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone core.num.niche_types.NonZeroUsizeInner → Result core.num.niche_types.NonZeroUsizeInner +/-- [core::num::nonzero::{core::num::nonzero::NonZero}::new]: + Source: '/rustc/library/core/src/num/nonzero.rs', lines 388:4-388:42 + Name pattern: [core::num::nonzero::{core::num::nonzero::NonZero<@T, @Clause0_NonZeroInner>}::new] + Visibility: public -/ +@[rust_fun + "core::num::nonzero::{core::num::nonzero::NonZero<@T, @Clause0_NonZeroInner>}::new"] +axiom core.num.nonzero.NonZero.new + {T : Type} {Clause0_NonZeroInner : Type} (ZeroablePrimitiveInst : + core.num.nonzero.ZeroablePrimitive T Clause0_NonZeroInner) : + T → Result (Option (core.num.nonzero.NonZero T Clause0_NonZeroInner)) + /-- [core::num::nonzero::{core::num::nonzero::NonZero}::get]: Source: '/rustc/library/core/src/num/nonzero.rs', lines 467:4-467:31 Name pattern: [core::num::nonzero::{core::num::nonzero::NonZero<@T, @Clause0_NonZeroInner>}::get] diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index 2a68dbe0e2..a53b231469 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -99,4 +99,10 @@ structure byteorder.U32 (O : Type) where _0 : Array Std.U8 4#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 + end Zerocopy 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..89ff7b9e67 100644 --- a/verification/aeneas/lean/Proofs.lean +++ b/verification/aeneas/lean/Proofs.lean @@ -11,32 +11,263 @@ 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 /-! -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 +/- 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 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 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 c820466380..52612ebaa5 100644 --- a/verification/aeneas/lean/Zerocopy/FunsExternal.lean +++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean @@ -22,3 +22,20 @@ def core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone @[simp] def core.num.nonzero.NonZero.get {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. +@[simp] noncomputable def core.num.nonzero.NonZero.new + {T Inner : Type} (_inst : core.num.nonzero.ZeroablePrimitive T Inner) + (x : T) : Result (Option (core.num.nonzero.NonZero T Inner)) := by + classical + exact if h : T = Usize then + if (cast h x : Usize) = 0#usize then .ok none else .ok (some ⟨x⟩) + else .fail .panic diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs index 09788f176e..c99b48969f 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)] @@ -2320,6 +2352,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]