From 8f23e4679a1550d0f32213f4e2dea9087b48c9c7 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Wed, 7 Oct 2026 06:40:34 -0400 Subject: [PATCH] Prove U16 and U32 byte-order reads, writes and updates Expose concrete calls to the production byteorder wrappers so annotation discovery does not depend on expanding their implementation macros. Add twelve total specifications covering reads, writes and setter/getter composition for U16 and U32 in both byte orders. Connect the extracted bit-vector operations to the shared radix-256 byte model. Independently check positional sums, every output byte and numerical value preservation. Model PhantomData structurally and admit only the opaque Formatter type needed by unused dictionaries, without assuming any formatting behavior. gherrit-pr-id: Gessib3piua3c4koztpng6i7m52bxi73s Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/README.md | 26 + verification/aeneas/golden/Funs.lean | 578 ++++++++++++++++++ verification/aeneas/golden/Types.lean | 60 ++ verification/aeneas/lean/BytesAdapter.lean | 60 ++ verification/aeneas/lean/Check.lean | 17 +- verification/aeneas/lean/DeriveModels.lean | 4 + verification/aeneas/lean/ModelPrelude.lean | 16 +- .../aeneas/lean/Obligations/Byteorder.lean | 117 ++++ .../aeneas/lean/Proofs/Byteorder.lean | 275 +++++++++ .../RequiredModelContracts/Byteorder.lean | 194 ++++++ .../aeneas/projections/ModelShapes.lean | 10 + verification/aeneas/projections/Models.lean | 15 + verification/aeneas/projections/Specs.lean | 104 ++++ zerocopy/src/byteorder.rs | 165 +++++ 14 files changed, 1637 insertions(+), 4 deletions(-) create mode 100644 verification/aeneas/lean/BytesAdapter.lean create mode 100644 verification/aeneas/lean/Obligations/Byteorder.lean create mode 100644 verification/aeneas/lean/Proofs/Byteorder.lean create mode 100644 verification/aeneas/lean/RequiredModelContracts/Byteorder.lean diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 5319434f5a..7723598880 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -211,6 +211,7 @@ added without extending the specification set. | Rust function | Checked property | | --- | --- | +| Byteorder U16/U32 read, write, and set (both endiannesses) | Exact integer value, every encoded byte, and setter/getter equality for every typed input. | | `max` | Terminates successfully and returns the mathematical maximum. | | `min` | Terminates successfully and returns the mathematical minimum. | | `padding_needed_for` | For any positive alignment, succeeds with padding strictly below that alignment. | @@ -826,3 +827,28 @@ provided useful prior evidence: Those older experiments are not assumed to describe the current release's runtime. This integration was validated with the pinned October 1 bundle and fresh translations of the current checkout. + +## Shared integer and byte mathematics + +`anneal/lean/Rust/Bytes.lean` defines unsigned byte encoding and decoding with +ordinary natural-number arithmetic, independently of Aeneas. It proves lengths, +bounds, truncation, and round trips for arbitrary byte counts. Anneal v1, v2, +and this integration share that package; each consumer supplies its own bridge +to the representation it verifies. + +The inline contracts in `byteorder::verification` exercise the production +U16/U32 `from_bytes`, `get`, `new`, `Into`, and `set` paths for both byte orders. +`BytesAdapter.lean` connects Aeneas's bit-vector codecs with the shared radix-256 +model. Independent required contracts spell out positional byte sums and each +output digit, so the same decoder helper cannot define both sides of the check. +There are no extra preconditions on these fixed arrays or unsigned integers. +This trial covers value computations; it does not verify signed conversions, +floating-point operations, pointer access, or the full byteorder API. + +The extracted ByteOrder trait dictionaries carry formatting methods even when +these computations never format anything. Aeneas leaves `Formatter` as an +opaque `Type`. The axiom audit admits that exact monomorphic data carrier after +checking its signature; no formatting proposition or behavior is assumed. A +change to a proposition or a function fails the audit. The PhantomData model +likewise records its zero runtime fields, with a Lean shape theorem that fails +if extraction adds fields; it makes no ownership or provenance claim. diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index a5dfa5edf3..551879d8e5 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -64,6 +64,584 @@ def Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner : innerCopyInst := core.num.niche_types.NonZeroUsizeInner.Insts.CoreMarkerCopy } +/-- Trait implementation: [zerocopy::byteorder::private::{impl zerocopy::byteorder::private::Sealed for zerocopy::byteorder::BigEndian}] + Source: 'src/byteorder.rs', lines 97:4-97:39 -/ +@[reducible] +def byteorder.BigEndian.Insts.ZerocopyByteorderPrivateSealed : + byteorder.private.Sealed byteorder.BigEndian := { +} + +/-- Trait implementation: [zerocopy::byteorder::private::{impl zerocopy::byteorder::private::Sealed for zerocopy::byteorder::LittleEndian}] + Source: 'src/byteorder.rs', lines 98:4-98:42 -/ +@[reducible] +def byteorder.LittleEndian.Insts.ZerocopyByteorderPrivateSealed : + byteorder.private.Sealed byteorder.LittleEndian := { +} + +/-- [zerocopy::byteorder::{impl core::clone::Clone for zerocopy::byteorder::BigEndian}::clone]: + Source: 'src/byteorder.rs', lines 113:15-113:20 + Visibility: public -/ +def byteorder.BigEndian.Insts.CoreCloneClone.clone + (self : byteorder.BigEndian) : Result byteorder.BigEndian := do + ok self + +/-- Trait implementation: [zerocopy::byteorder::{impl core::clone::Clone for zerocopy::byteorder::BigEndian}] + Source: 'src/byteorder.rs', lines 113:15-113:20 -/ +@[reducible] +def byteorder.BigEndian.Insts.CoreCloneClone : core.clone.Clone + byteorder.BigEndian := { + clone := byteorder.BigEndian.Insts.CoreCloneClone.clone +} + +/-- Trait implementation: [zerocopy::byteorder::{impl core::marker::Copy for zerocopy::byteorder::BigEndian}] + Source: 'src/byteorder.rs', lines 113:9-113:13 -/ +@[reducible] +def byteorder.BigEndian.Insts.CoreMarkerCopy : core.marker.Copy + byteorder.BigEndian := { + cloneInst := byteorder.BigEndian.Insts.CoreCloneClone +} + +/-- [zerocopy::byteorder::{impl core::fmt::Debug for zerocopy::byteorder::BigEndian}::fmt]: + Source: 'src/byteorder.rs', lines 113:22-113:27 + Visibility: public -/ +def byteorder.BigEndian.Insts.CoreFmtDebug.fmt + (self : byteorder.BigEndian) (f : core.fmt.Formatter) : + Result ((core.result.Result Unit core.fmt.Error) × core.fmt.Formatter) + := do + fail panic + +/-- Trait implementation: [zerocopy::byteorder::{impl core::fmt::Debug for zerocopy::byteorder::BigEndian}] + Source: 'src/byteorder.rs', lines 113:22-113:27 -/ +@[reducible] +def byteorder.BigEndian.Insts.CoreFmtDebug : core.fmt.Debug byteorder.BigEndian + := { + fmt := byteorder.BigEndian.Insts.CoreFmtDebug.fmt +} + +/-- [zerocopy::byteorder::{impl core::cmp::PartialEq for zerocopy::byteorder::BigEndian}::eq]: + Source: 'src/byteorder.rs', lines 113:33-113:42 + Visibility: public -/ +def byteorder.BigEndian.Insts.CoreCmpPartialEqBigEndian.eq + (self : byteorder.BigEndian) (other : byteorder.BigEndian) : + Result Bool + := do + fail panic + +/-- Trait implementation: [zerocopy::byteorder::{impl core::cmp::PartialEq for zerocopy::byteorder::BigEndian}] + Source: 'src/byteorder.rs', lines 113:33-113:42 -/ +@[reducible] +def byteorder.BigEndian.Insts.CoreCmpPartialEqBigEndian : core.cmp.PartialEq + byteorder.BigEndian byteorder.BigEndian := { + eq := byteorder.BigEndian.Insts.CoreCmpPartialEqBigEndian.eq +} + +/-- Trait implementation: [zerocopy::byteorder::{impl core::cmp::Eq for zerocopy::byteorder::BigEndian}] + Source: 'src/byteorder.rs', lines 113:29-113:31 -/ +@[reducible] +def byteorder.BigEndian.Insts.CoreCmpEq : core.cmp.Eq byteorder.BigEndian := { + partialEqInst := byteorder.BigEndian.Insts.CoreCmpPartialEqBigEndian +} + +/-- [zerocopy::byteorder::{impl core::cmp::PartialOrd for zerocopy::byteorder::BigEndian}::partial_cmp]: + Source: 'src/byteorder.rs', lines 113:49-113:59 + Visibility: public -/ +def byteorder.BigEndian.Insts.CoreCmpPartialOrdBigEndian.partial_cmp + (self : byteorder.BigEndian) (other : byteorder.BigEndian) : + Result (Option Ordering) + := do + fail panic + +/-- Trait implementation: [zerocopy::byteorder::{impl core::cmp::PartialOrd for zerocopy::byteorder::BigEndian}] + Source: 'src/byteorder.rs', lines 113:49-113:59 -/ +@[reducible] +def byteorder.BigEndian.Insts.CoreCmpPartialOrdBigEndian : core.cmp.PartialOrd + byteorder.BigEndian byteorder.BigEndian := { + partialEqInst := byteorder.BigEndian.Insts.CoreCmpPartialEqBigEndian + partial_cmp := + byteorder.BigEndian.Insts.CoreCmpPartialOrdBigEndian.partial_cmp +} + +/-- [zerocopy::byteorder::{impl core::cmp::Ord for zerocopy::byteorder::BigEndian}::cmp]: + Source: 'src/byteorder.rs', lines 113:44-113:47 + Visibility: public -/ +def byteorder.BigEndian.Insts.CoreCmpOrd.cmp + (self : byteorder.BigEndian) (other : byteorder.BigEndian) : + Result Ordering + := do + fail panic + +/-- Trait implementation: [zerocopy::byteorder::{impl core::cmp::Ord for zerocopy::byteorder::BigEndian}] + Source: 'src/byteorder.rs', lines 113:44-113:47 -/ +@[reducible] +def byteorder.BigEndian.Insts.CoreCmpOrd : core.cmp.Ord byteorder.BigEndian + := { + eqInst := byteorder.BigEndian.Insts.CoreCmpEq + partialOrdInst := byteorder.BigEndian.Insts.CoreCmpPartialOrdBigEndian + cmp := byteorder.BigEndian.Insts.CoreCmpOrd.cmp +} + +/-- [zerocopy::byteorder::{impl core::hash::Hash for zerocopy::byteorder::BigEndian}::hash]: + Source: 'src/byteorder.rs', lines 113:61-113:65 + Visibility: public -/ +def byteorder.BigEndian.Insts.CoreHashHash.hash + {__H : Type} (corehashHasherInst : core.hash.Hasher __H) + (self : byteorder.BigEndian) (state : __H) : + Result __H + := do + fail panic + +/-- Trait implementation: [zerocopy::byteorder::{impl core::hash::Hash for zerocopy::byteorder::BigEndian}] + Source: 'src/byteorder.rs', lines 113:61-113:65 -/ +@[reducible] +def byteorder.BigEndian.Insts.CoreHashHash : core.hash.Hash byteorder.BigEndian + := { + hash := fun {H : Type} (corehashHasherInst : core.hash.Hasher H) => + byteorder.BigEndian.Insts.CoreHashHash.hash corehashHasherInst +} + +/-- [zerocopy::byteorder::{impl core::fmt::Display for zerocopy::byteorder::BigEndian}::fmt]: + Source: 'src/byteorder.rs', lines 122:4-124:5 + Visibility: public -/ +def byteorder.BigEndian.Insts.CoreFmtDisplay.fmt + (self : byteorder.BigEndian) (f : core.fmt.Formatter) : + Result ((core.result.Result Unit core.fmt.Error) × core.fmt.Formatter) + := do + fail panic + +/-- Trait implementation: [zerocopy::byteorder::{impl core::fmt::Display for zerocopy::byteorder::BigEndian}] + Source: 'src/byteorder.rs', lines 120:0-125:1 -/ +@[reducible] +def byteorder.BigEndian.Insts.CoreFmtDisplay : core.fmt.Display + byteorder.BigEndian := { + fmt := byteorder.BigEndian.Insts.CoreFmtDisplay.fmt +} + +/-- [zerocopy::byteorder::{impl zerocopy::byteorder::ByteOrder for zerocopy::byteorder::BigEndian}::ORDER] + Source: 'src/byteorder.rs', lines 117:4-117:42 + Visibility: public -/ +@[global_simps, irreducible] +def byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder.ORDER + : byteorder.Order := + byteorder.Order.BigEndian + +/-- Trait implementation: [zerocopy::byteorder::{impl zerocopy::byteorder::ByteOrder for zerocopy::byteorder::BigEndian}] + Source: 'src/byteorder.rs', lines 116:0-118:1 -/ +@[reducible] +def byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder : byteorder.ByteOrder + byteorder.BigEndian := { + ORDER := ok byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder.ORDER + coremarkerCopyInst := byteorder.BigEndian.Insts.CoreMarkerCopy + corecloneCloneInst := byteorder.BigEndian.Insts.CoreCloneClone + corefmtDebugInst := byteorder.BigEndian.Insts.CoreFmtDebug + corefmtDisplayInst := byteorder.BigEndian.Insts.CoreFmtDisplay + corecmpEqInst := byteorder.BigEndian.Insts.CoreCmpEq + corecmpPartialEqInst := byteorder.BigEndian.Insts.CoreCmpPartialEqBigEndian + corecmpOrdInst := byteorder.BigEndian.Insts.CoreCmpOrd + corecmpPartialOrdInst := byteorder.BigEndian.Insts.CoreCmpPartialOrdBigEndian + corehashHashInst := byteorder.BigEndian.Insts.CoreHashHash + privateSealedInst := byteorder.BigEndian.Insts.ZerocopyByteorderPrivateSealed +} + +/-- [zerocopy::byteorder::{impl core::clone::Clone for zerocopy::byteorder::LittleEndian}::clone]: + Source: 'src/byteorder.rs', lines 130:15-130:20 + Visibility: public -/ +def byteorder.LittleEndian.Insts.CoreCloneClone.clone + (self : byteorder.LittleEndian) : Result byteorder.LittleEndian := do + ok self + +/-- Trait implementation: [zerocopy::byteorder::{impl core::clone::Clone for zerocopy::byteorder::LittleEndian}] + Source: 'src/byteorder.rs', lines 130:15-130:20 -/ +@[reducible] +def byteorder.LittleEndian.Insts.CoreCloneClone : core.clone.Clone + byteorder.LittleEndian := { + clone := byteorder.LittleEndian.Insts.CoreCloneClone.clone +} + +/-- Trait implementation: [zerocopy::byteorder::{impl core::marker::Copy for zerocopy::byteorder::LittleEndian}] + Source: 'src/byteorder.rs', lines 130:9-130:13 -/ +@[reducible] +def byteorder.LittleEndian.Insts.CoreMarkerCopy : core.marker.Copy + byteorder.LittleEndian := { + cloneInst := byteorder.LittleEndian.Insts.CoreCloneClone +} + +/-- [zerocopy::byteorder::{impl core::fmt::Debug for zerocopy::byteorder::LittleEndian}::fmt]: + Source: 'src/byteorder.rs', lines 130:22-130:27 + Visibility: public -/ +def byteorder.LittleEndian.Insts.CoreFmtDebug.fmt + (self : byteorder.LittleEndian) (f : core.fmt.Formatter) : + Result ((core.result.Result Unit core.fmt.Error) × core.fmt.Formatter) + := do + fail panic + +/-- Trait implementation: [zerocopy::byteorder::{impl core::fmt::Debug for zerocopy::byteorder::LittleEndian}] + Source: 'src/byteorder.rs', lines 130:22-130:27 -/ +@[reducible] +def byteorder.LittleEndian.Insts.CoreFmtDebug : core.fmt.Debug + byteorder.LittleEndian := { + fmt := byteorder.LittleEndian.Insts.CoreFmtDebug.fmt +} + +/-- [zerocopy::byteorder::{impl core::cmp::PartialEq for zerocopy::byteorder::LittleEndian}::eq]: + Source: 'src/byteorder.rs', lines 130:33-130:42 + Visibility: public -/ +def byteorder.LittleEndian.Insts.CoreCmpPartialEqLittleEndian.eq + (self : byteorder.LittleEndian) (other : byteorder.LittleEndian) : + Result Bool + := do + fail panic + +/-- Trait implementation: [zerocopy::byteorder::{impl core::cmp::PartialEq for zerocopy::byteorder::LittleEndian}] + Source: 'src/byteorder.rs', lines 130:33-130:42 -/ +@[reducible] +def byteorder.LittleEndian.Insts.CoreCmpPartialEqLittleEndian : + core.cmp.PartialEq byteorder.LittleEndian byteorder.LittleEndian := { + eq := byteorder.LittleEndian.Insts.CoreCmpPartialEqLittleEndian.eq +} + +/-- Trait implementation: [zerocopy::byteorder::{impl core::cmp::Eq for zerocopy::byteorder::LittleEndian}] + Source: 'src/byteorder.rs', lines 130:29-130:31 -/ +@[reducible] +def byteorder.LittleEndian.Insts.CoreCmpEq : core.cmp.Eq byteorder.LittleEndian + := { + partialEqInst := byteorder.LittleEndian.Insts.CoreCmpPartialEqLittleEndian +} + +/-- [zerocopy::byteorder::{impl core::cmp::PartialOrd for zerocopy::byteorder::LittleEndian}::partial_cmp]: + Source: 'src/byteorder.rs', lines 130:49-130:59 + Visibility: public -/ +def byteorder.LittleEndian.Insts.CoreCmpPartialOrdLittleEndian.partial_cmp + (self : byteorder.LittleEndian) (other : byteorder.LittleEndian) : + Result (Option Ordering) + := do + fail panic + +/-- Trait implementation: [zerocopy::byteorder::{impl core::cmp::PartialOrd for zerocopy::byteorder::LittleEndian}] + Source: 'src/byteorder.rs', lines 130:49-130:59 -/ +@[reducible] +def byteorder.LittleEndian.Insts.CoreCmpPartialOrdLittleEndian : + core.cmp.PartialOrd byteorder.LittleEndian byteorder.LittleEndian := { + partialEqInst := byteorder.LittleEndian.Insts.CoreCmpPartialEqLittleEndian + partial_cmp := + byteorder.LittleEndian.Insts.CoreCmpPartialOrdLittleEndian.partial_cmp +} + +/-- [zerocopy::byteorder::{impl core::cmp::Ord for zerocopy::byteorder::LittleEndian}::cmp]: + Source: 'src/byteorder.rs', lines 130:44-130:47 + Visibility: public -/ +def byteorder.LittleEndian.Insts.CoreCmpOrd.cmp + (self : byteorder.LittleEndian) (other : byteorder.LittleEndian) : + Result Ordering + := do + fail panic + +/-- Trait implementation: [zerocopy::byteorder::{impl core::cmp::Ord for zerocopy::byteorder::LittleEndian}] + Source: 'src/byteorder.rs', lines 130:44-130:47 -/ +@[reducible] +def byteorder.LittleEndian.Insts.CoreCmpOrd : core.cmp.Ord + byteorder.LittleEndian := { + eqInst := byteorder.LittleEndian.Insts.CoreCmpEq + partialOrdInst := byteorder.LittleEndian.Insts.CoreCmpPartialOrdLittleEndian + cmp := byteorder.LittleEndian.Insts.CoreCmpOrd.cmp +} + +/-- [zerocopy::byteorder::{impl core::hash::Hash for zerocopy::byteorder::LittleEndian}::hash]: + Source: 'src/byteorder.rs', lines 130:61-130:65 + Visibility: public -/ +def byteorder.LittleEndian.Insts.CoreHashHash.hash + {__H : Type} (corehashHasherInst : core.hash.Hasher __H) + (self : byteorder.LittleEndian) (state : __H) : + Result __H + := do + fail panic + +/-- Trait implementation: [zerocopy::byteorder::{impl core::hash::Hash for zerocopy::byteorder::LittleEndian}] + Source: 'src/byteorder.rs', lines 130:61-130:65 -/ +@[reducible] +def byteorder.LittleEndian.Insts.CoreHashHash : core.hash.Hash + byteorder.LittleEndian := { + hash := fun {H : Type} (corehashHasherInst : core.hash.Hasher H) => + byteorder.LittleEndian.Insts.CoreHashHash.hash corehashHasherInst +} + +/-- [zerocopy::byteorder::{impl core::fmt::Display for zerocopy::byteorder::LittleEndian}::fmt]: + Source: 'src/byteorder.rs', lines 139:4-141:5 + Visibility: public -/ +def byteorder.LittleEndian.Insts.CoreFmtDisplay.fmt + (self : byteorder.LittleEndian) (f : core.fmt.Formatter) : + Result ((core.result.Result Unit core.fmt.Error) × core.fmt.Formatter) + := do + fail panic + +/-- Trait implementation: [zerocopy::byteorder::{impl core::fmt::Display for zerocopy::byteorder::LittleEndian}] + Source: 'src/byteorder.rs', lines 137:0-142:1 -/ +@[reducible] +def byteorder.LittleEndian.Insts.CoreFmtDisplay : core.fmt.Display + byteorder.LittleEndian := { + fmt := byteorder.LittleEndian.Insts.CoreFmtDisplay.fmt +} + +/-- [zerocopy::byteorder::{impl zerocopy::byteorder::ByteOrder for zerocopy::byteorder::LittleEndian}::ORDER] + Source: 'src/byteorder.rs', lines 134:4-134:45 + Visibility: public -/ +@[global_simps, irreducible] +def byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder.ORDER + : byteorder.Order := + byteorder.Order.LittleEndian + +/-- Trait implementation: [zerocopy::byteorder::{impl zerocopy::byteorder::ByteOrder for zerocopy::byteorder::LittleEndian}] + Source: 'src/byteorder.rs', lines 133:0-135:1 -/ +@[reducible] +def byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder : + byteorder.ByteOrder byteorder.LittleEndian := { + ORDER := ok byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder.ORDER + coremarkerCopyInst := byteorder.LittleEndian.Insts.CoreMarkerCopy + corecloneCloneInst := byteorder.LittleEndian.Insts.CoreCloneClone + corefmtDebugInst := byteorder.LittleEndian.Insts.CoreFmtDebug + corefmtDisplayInst := byteorder.LittleEndian.Insts.CoreFmtDisplay + corecmpEqInst := byteorder.LittleEndian.Insts.CoreCmpEq + corecmpPartialEqInst := + byteorder.LittleEndian.Insts.CoreCmpPartialEqLittleEndian + corecmpOrdInst := byteorder.LittleEndian.Insts.CoreCmpOrd + corecmpPartialOrdInst := + byteorder.LittleEndian.Insts.CoreCmpPartialOrdLittleEndian + corehashHashInst := byteorder.LittleEndian.Insts.CoreHashHash + privateSealedInst := + byteorder.LittleEndian.Insts.ZerocopyByteorderPrivateSealed +} + +/-- [zerocopy::byteorder::{zerocopy::byteorder::U16}::from_bytes]: + Source: 'src/byteorder.rs', lines 570:12-572:13 + Visibility: public -/ +def byteorder.U16.from_bytes + (O : Type) (bytes : Array Std.U8 2#usize) : Result (byteorder.U16 O) := do + ok { _0 := bytes, _1 := core.marker.PhantomData.mk } + +/-- [zerocopy::byteorder::{zerocopy::byteorder::U32}::from_bytes]: + Source: 'src/byteorder.rs', lines 570:12-572:13 + Visibility: public -/ +def byteorder.U32.from_bytes + (O : Type) (bytes : Array Std.U8 4#usize) : Result (byteorder.U32 O) := do + ok { _0 := bytes, _1 := core.marker.PhantomData.mk } + +/-- [zerocopy::byteorder::{zerocopy::byteorder::U16}::new]: + Source: 'src/util/macros.rs', lines 560:21-560:88 + Visibility: public -/ +def byteorder.U16.new + {O : Type} (ByteOrderInst : byteorder.ByteOrder O) (n : Std.U16) : + Result (byteorder.U16 O) + := do + let o ← ByteOrderInst.ORDER + match o with + | byteorder.Order.BigEndian => + let bytes ← lift (core.num.U16.to_be_bytes n) + ok { _0 := bytes, _1 := core.marker.PhantomData.mk } + | byteorder.Order.LittleEndian => + let bytes ← lift (core.num.U16.to_le_bytes n) + ok { _0 := bytes, _1 := core.marker.PhantomData.mk } + +/-- [zerocopy::byteorder::{zerocopy::byteorder::U16}::set]: + Source: 'src/byteorder.rs', lines 619:12-621:13 + Visibility: public -/ +def byteorder.U16.set + {O : Type} (ByteOrderInst : byteorder.ByteOrder O) (self : byteorder.U16 O) + (n : Std.U16) : + Result (byteorder.U16 O) + := do + byteorder.U16.new ByteOrderInst n + +/-- [zerocopy::byteorder::{zerocopy::byteorder::U32}::new]: + Source: 'src/util/macros.rs', lines 560:21-560:88 + Visibility: public -/ +def byteorder.U32.new + {O : Type} (ByteOrderInst : byteorder.ByteOrder O) (n : Std.U32) : + Result (byteorder.U32 O) + := do + let o ← ByteOrderInst.ORDER + match o with + | byteorder.Order.BigEndian => + let bytes ← lift (core.num.U32.to_be_bytes n) + ok { _0 := bytes, _1 := core.marker.PhantomData.mk } + | byteorder.Order.LittleEndian => + let bytes ← lift (core.num.U32.to_le_bytes n) + ok { _0 := bytes, _1 := core.marker.PhantomData.mk } + +/-- [zerocopy::byteorder::{zerocopy::byteorder::U32}::set]: + Source: 'src/byteorder.rs', lines 619:12-621:13 + Visibility: public -/ +def byteorder.U32.set + {O : Type} (ByteOrderInst : byteorder.ByteOrder O) (self : byteorder.U32 O) + (n : Std.U32) : + Result (byteorder.U32 O) + := do + byteorder.U32.new ByteOrderInst n + +/-- [zerocopy::byteorder::{impl core::convert::From> for [u8; 2usize]}::from]: + Source: 'src/byteorder.rs', lines 631:12-633:13 + Visibility: public -/ +def ArrayU82.Insts.CoreConvertFromU16.from + {O : Type} (ByteOrderInst : byteorder.ByteOrder O) (x : byteorder.U16 O) : + Result (Array Std.U8 2#usize) + := do + ok x._0 + +/-- Trait implementation: [zerocopy::byteorder::{impl core::convert::From> for [u8; 2usize]}] + Source: 'src/byteorder.rs', lines 629:8-634:9 -/ +@[reducible] +def ArrayU82.Insts.CoreConvertFromU16 {O : Type} (ByteOrderInst : + byteorder.ByteOrder O) : core.convert.From (Array Std.U8 2#usize) + (byteorder.U16 O) := { + «from» := ArrayU82.Insts.CoreConvertFromU16.from ByteOrderInst +} + +/-- [zerocopy::byteorder::{impl core::convert::From> for [u8; 4usize]}::from]: + Source: 'src/byteorder.rs', lines 631:12-633:13 + Visibility: public -/ +def ArrayU84.Insts.CoreConvertFromU32.from + {O : Type} (ByteOrderInst : byteorder.ByteOrder O) (x : byteorder.U32 O) : + Result (Array Std.U8 4#usize) + := do + ok x._0 + +/-- Trait implementation: [zerocopy::byteorder::{impl core::convert::From> for [u8; 4usize]}] + Source: 'src/byteorder.rs', lines 629:8-634:9 -/ +@[reducible] +def ArrayU84.Insts.CoreConvertFromU32 {O : Type} (ByteOrderInst : + byteorder.ByteOrder O) : core.convert.From (Array Std.U8 4#usize) + (byteorder.U32 O) := { + «from» := ArrayU84.Insts.CoreConvertFromU32.from ByteOrderInst +} + +/-- [zerocopy::byteorder::{zerocopy::byteorder::U16}::get]: + Source: 'src/util/macros.rs', lines 560:21-560:88 + Visibility: public -/ +def byteorder.U16.get + {O : Type} (ByteOrderInst : byteorder.ByteOrder O) (self : byteorder.U16 O) : + Result Std.U16 + := do + let o ← ByteOrderInst.ORDER + match o with + | byteorder.Order.BigEndian => ok (core.num.U16.from_be_bytes self._0) + | byteorder.Order.LittleEndian => ok (core.num.U16.from_le_bytes self._0) + +/-- [zerocopy::byteorder::verification::read_u16_le]: + Source: 'src/byteorder.rs', lines 1643:4-1645:5 -/ +def byteorder.verification.read_u16_le + (bytes : Array Std.U8 2#usize) : Result Std.U16 := do + let u ← byteorder.U16.from_bytes byteorder.LittleEndian bytes + byteorder.U16.get byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder u + +/-- [zerocopy::byteorder::verification::write_u16_le]: + Source: 'src/byteorder.rs', lines 1654:4-1656:5 -/ +def byteorder.verification.write_u16_le + (n : Std.U16) : Result (Array Std.U8 2#usize) := do + let u ← + byteorder.U16.new byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder n + core.convert.IntoFrom.into (ArrayU82.Insts.CoreConvertFromU16 + byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder) u + +/-- [zerocopy::byteorder::verification::set_u16_le]: + Source: 'src/byteorder.rs', lines 1664:4-1668:5 -/ +def byteorder.verification.set_u16_le + (bytes : Array Std.U8 2#usize) (n : Std.U16) : Result Std.U16 := do + let value ← byteorder.U16.from_bytes byteorder.LittleEndian bytes + let value1 ← + byteorder.U16.set byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder + value n + byteorder.U16.get byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder + value1 + +/-- [zerocopy::byteorder::verification::read_u16_be]: + Source: 'src/byteorder.rs', lines 1677:4-1679:5 -/ +def byteorder.verification.read_u16_be + (bytes : Array Std.U8 2#usize) : Result Std.U16 := do + let u ← byteorder.U16.from_bytes byteorder.BigEndian bytes + byteorder.U16.get byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder u + +/-- [zerocopy::byteorder::verification::write_u16_be]: + Source: 'src/byteorder.rs', lines 1688:4-1690:5 -/ +def byteorder.verification.write_u16_be + (n : Std.U16) : Result (Array Std.U8 2#usize) := do + let u ← + byteorder.U16.new byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder n + core.convert.IntoFrom.into (ArrayU82.Insts.CoreConvertFromU16 + byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder) u + +/-- [zerocopy::byteorder::verification::set_u16_be]: + Source: 'src/byteorder.rs', lines 1698:4-1702:5 -/ +def byteorder.verification.set_u16_be + (bytes : Array Std.U8 2#usize) (n : Std.U16) : Result Std.U16 := do + let value ← byteorder.U16.from_bytes byteorder.BigEndian bytes + let value1 ← + byteorder.U16.set byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder + value n + byteorder.U16.get byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder value1 + +/-- [zerocopy::byteorder::{zerocopy::byteorder::U32}::get]: + Source: 'src/util/macros.rs', lines 560:21-560:88 + Visibility: public -/ +def byteorder.U32.get + {O : Type} (ByteOrderInst : byteorder.ByteOrder O) (self : byteorder.U32 O) : + Result Std.U32 + := do + let o ← ByteOrderInst.ORDER + match o with + | byteorder.Order.BigEndian => ok (core.num.U32.from_be_bytes self._0) + | byteorder.Order.LittleEndian => ok (core.num.U32.from_le_bytes self._0) + +/-- [zerocopy::byteorder::verification::read_u32_le]: + Source: 'src/byteorder.rs', lines 1711:4-1713:5 -/ +def byteorder.verification.read_u32_le + (bytes : Array Std.U8 4#usize) : Result Std.U32 := do + let u ← byteorder.U32.from_bytes byteorder.LittleEndian bytes + byteorder.U32.get byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder u + +/-- [zerocopy::byteorder::verification::write_u32_le]: + Source: 'src/byteorder.rs', lines 1722:4-1724:5 -/ +def byteorder.verification.write_u32_le + (n : Std.U32) : Result (Array Std.U8 4#usize) := do + let u ← + byteorder.U32.new byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder n + core.convert.IntoFrom.into (ArrayU84.Insts.CoreConvertFromU32 + byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder) u + +/-- [zerocopy::byteorder::verification::set_u32_le]: + Source: 'src/byteorder.rs', lines 1732:4-1736:5 -/ +def byteorder.verification.set_u32_le + (bytes : Array Std.U8 4#usize) (n : Std.U32) : Result Std.U32 := do + let value ← byteorder.U32.from_bytes byteorder.LittleEndian bytes + let value1 ← + byteorder.U32.set byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder + value n + byteorder.U32.get byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder + value1 + +/-- [zerocopy::byteorder::verification::read_u32_be]: + Source: 'src/byteorder.rs', lines 1745:4-1747:5 -/ +def byteorder.verification.read_u32_be + (bytes : Array Std.U8 4#usize) : Result Std.U32 := do + let u ← byteorder.U32.from_bytes byteorder.BigEndian bytes + byteorder.U32.get byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder u + +/-- [zerocopy::byteorder::verification::write_u32_be]: + Source: 'src/byteorder.rs', lines 1756:4-1758:5 -/ +def byteorder.verification.write_u32_be + (n : Std.U32) : Result (Array Std.U8 4#usize) := do + let u ← + byteorder.U32.new byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder n + core.convert.IntoFrom.into (ArrayU84.Insts.CoreConvertFromU32 + byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder) u + +/-- [zerocopy::byteorder::verification::set_u32_be]: + Source: 'src/byteorder.rs', lines 1766:4-1770:5 -/ +def byteorder.verification.set_u32_be + (bytes : Array Std.U8 4#usize) (n : Std.U32) : Result Std.U32 := do + let value ← byteorder.U32.from_bytes byteorder.BigEndian bytes + let value1 ← + byteorder.U32.set byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder + value n + byteorder.U32.get byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder value1 + /-- [zerocopy::util::padding_needed_for]: Source: 'src/util/mod.rs', lines 163:0-223:1 -/ def util.padding_needed_for diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index 687cf0b1f8..2a68dbe0e2 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -28,6 +28,13 @@ set_option maxRecDepth 2048 namespace Zerocopy +/-- [core::marker::PhantomData] + Source: '/rustc/library/core/src/marker.rs', lines 811:0-811:39 + Name pattern: [core::marker::PhantomData] + Visibility: public -/ +@[rust_type "core::marker::PhantomData"] +structure core.marker.PhantomData (T : Type) where + /-- Trait declaration: [core::num::nonzero::ZeroablePrimitive] Source: '/rustc/library/core/src/num/nonzero.rs', lines 34:0-34:59 Name pattern: [core::num::nonzero::ZeroablePrimitive] @@ -39,4 +46,57 @@ structure core.num.nonzero.ZeroablePrimitive (Self : Type) (Self_NonZeroInner : markerCopyInst : core.marker.Copy Self innerCopyInst : core.marker.Copy Self_NonZeroInner +/-- [zerocopy::byteorder::Order] + Source: 'src/byteorder.rs', lines 103:0-108:1 + Visibility: public -/ +@[discriminant isize] +inductive byteorder.Order where +| BigEndian : byteorder.Order +| LittleEndian : byteorder.Order + +/-- Trait declaration: [zerocopy::byteorder::private::Sealed] + Source: 'src/byteorder.rs', lines 95:4-95:23 + Visibility: public -/ +structure byteorder.private.Sealed (Self : Type) where + +/-- Trait declaration: [zerocopy::byteorder::ByteOrder] + Source: 'src/byteorder.rs', lines 87:0-92:1 + Visibility: public -/ +structure byteorder.ByteOrder (Self : Type) where + ORDER : Result byteorder.Order + coremarkerCopyInst : core.marker.Copy Self + corecloneCloneInst : core.clone.Clone Self + corefmtDebugInst : core.fmt.Debug Self + corefmtDisplayInst : core.fmt.Display Self + corecmpEqInst : core.cmp.Eq Self + corecmpPartialEqInst : core.cmp.PartialEq Self Self + corecmpOrdInst : core.cmp.Ord Self + corecmpPartialOrdInst : core.cmp.PartialOrd Self Self + corehashHashInst : core.hash.Hash Self + privateSealedInst : byteorder.private.Sealed Self + +/-- [zerocopy::byteorder::BigEndian] + Source: 'src/byteorder.rs', lines 114:0-114:21 + Visibility: public -/ +inductive byteorder.BigEndian where + +/-- [zerocopy::byteorder::LittleEndian] + Source: 'src/byteorder.rs', lines 131:0-131:24 + Visibility: public -/ +inductive byteorder.LittleEndian where + +/-- [zerocopy::byteorder::U16] + Source: 'src/byteorder.rs', lines 528:12-528:62 + Visibility: public -/ +structure byteorder.U16 (O : Type) where + _0 : Array Std.U8 2#usize + _1 : core.marker.PhantomData O + +/-- [zerocopy::byteorder::U32] + Source: 'src/byteorder.rs', lines 528:12-528:62 + Visibility: public -/ +structure byteorder.U32 (O : Type) where + _0 : Array Std.U8 4#usize + _1 : core.marker.PhantomData O + end Zerocopy diff --git a/verification/aeneas/lean/BytesAdapter.lean b/verification/aeneas/lean/BytesAdapter.lean new file mode 100644 index 0000000000..597f52f176 --- /dev/null +++ b/verification/aeneas/lean/BytesAdapter.lean @@ -0,0 +1,60 @@ +/- 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 RustAeneas.Bytes +public import ModelLemmas +@[expose] public section + +/-! +These adapters preserve byte values through zerocopy's scalar-array decoders. +The generic numerical byte bridges live in the shared Aeneas companion package. +Rust/compiler correspondence remains a separate obligation. +-/ + +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +/-- Scalar list decoding accepts every finite scalar and preserves its value. -/ +theorem decodeList_unsigned {ty : UScalarTy} (raw : List (UScalar ty)) : + decodeList (modelUScalar ty).decode raw = some (raw.map unsignedWord) := by + induction raw with + | nil => rfl + | cons head tail ih => simp [decodeList, ih] + +/-- The mathematical witness for every raw scalar array, at its original length. -/ +def unsignedArray {ty : UScalarTy} {count : Usize} (raw : Aeneas.Std.Array (UScalar ty) count) : + ArrayValue (UnsignedWord ty) count := + ⟨raw.val.map unsignedWord, by simpa only [List.length_map] using raw.property⟩ + +theorem decodeArray_unsigned {ty : UScalarTy} {count : Usize} + (raw : Aeneas.Std.Array (UScalar ty) count) : + (modelArray count).decode raw = some (unsignedArray raw) := by + apply (decodeArray_iff (modelUScalar ty) count raw (unsignedArray raw)).mpr + exact decodeList_unsigned raw.val + +theorem u8_ofNat_val (raw : U8) : BitVec.ofNat 8 raw.val = raw.bv := by + apply BitVec.eq_of_toNat_eq + simp only [BitVec.toNat_ofNat, UScalar.val] + exact Nat.mod_eq_of_lt raw.bv.isLt + +/-- The decoded array retains every byte used by the numerical specification. -/ +theorem decodedArray_bytes_eq {count : Usize} (raw : Aeneas.Std.Array U8 count) + (value : ArrayValue (UnsignedWord .U8) count) + (decoded : (modelArray count).decode raw = some value) : + value.val.map (fun byte => BitVec.ofNat 8 (byte : Nat)) = raw.val.map U8.bv := by + have same : raw.val.map unsignedWord = value.val := + Option.some.inj ((decodeList_unsigned raw.val).symm.trans + ((decodeArray_iff (modelUScalar .U8) count raw value).mp decoded)) + simp only [← same, bind_pure_comp] + simp only [Functor.map, List.map_map] + apply List.map_congr_left + intro byte _ + exact u8_ofNat_val byte + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Check.lean b/verification/aeneas/lean/Check.lean index 084929939d..ec91cb7b9a 100644 --- a/verification/aeneas/lean/Check.lean +++ b/verification/aeneas/lean/Check.lean @@ -33,6 +33,17 @@ run_elab do -- may have only the pointer-width size read and require no generic ABI inputs. let hasLayoutReads := env.contains `core.mem.align_of let modelInputs := if hasLayoutReads then layoutInputs else #[] + -- ByteOrder carries formatting dictionaries even when a numerical method + -- never formats a value. The backend leaves Formatter's representation + -- abstract. Admit this exact opaque type, with no axiom about its values or + -- behavior; changing it into a proposition or a function is an error. + let opaqueCarriers := #[`Aeneas.Std.core.fmt.Formatter] + let expectedCarrier ← Term.elabType (← `(Type)) + for carrier in opaqueCarriers do + let some (.axiomInfo info) := env.find? carrier + | throwError "Missing pinned opaque carrier {carrier}" + unless info.levelParams.isEmpty && (← Meta.isDefEq info.type expectedCarrier) do + throwError "Opaque carrier {carrier} changed its type-only signature" -- ABI inputs are functions returning data, with no proposition asserting -- alignment, size, or correctness. A changed type could smuggle a theorem -- into the allowed axiom list, so check their exact compiled signatures. @@ -430,11 +441,11 @@ run_elab do let used ← collectAxioms declName for ax in used do -- These are Lean's permitted logical axioms. The only additional - -- allowances are the ABI data inputs whose exact signatures were - -- checked above. They supply no proposition; + -- allowances are the ABI data inputs and opaque carrier whose exact + -- signatures were checked above. Neither supplies a proposition; -- sorryAx and user-defined proof axioms remain errors. unless #[`propext, `Classical.choice, `Quot.sound].contains ax || - modelInputs.contains ax do + modelInputs.contains ax || opaqueCarriers.contains ax do throwError "{declName} depends on unapproved axiom {ax}" audited := audited + 1 IO.FS.writeFile "proof-dependencies.json" (Json.arr graph).pretty diff --git a/verification/aeneas/lean/DeriveModels.lean b/verification/aeneas/lean/DeriveModels.lean index 8a3e51c336..0aa8c4699e 100644 --- a/verification/aeneas/lean/DeriveModels.lean +++ b/verification/aeneas/lean/DeriveModels.lean @@ -104,6 +104,10 @@ meta partial def boundModelProvider (raw : Expr) (params dicts : Array Expr) : M mkAppOptM n (xs.map some) if head.isConstOf ``UScalar then return ← app ``modelUScalar args if head.isConstOf ``IScalar then return ← app ``modelIScalar args + -- PhantomData has no stored child value: select its fixed empty provider + -- without demanding a model for the type named by its phantom parameter. + if head.isConstOf ``Zerocopy.core.marker.PhantomData then + return ← app ``modelPhantomData args if head.isConstOf ``Bool then return mkConst ``modelBool if head.isConstOf ``Nat then return mkConst ``modelNat if head.isConstOf ``Int then return mkConst ``modelInt diff --git a/verification/aeneas/lean/ModelPrelude.lean b/verification/aeneas/lean/ModelPrelude.lean index c2082eeb4b..7d2f64655c 100644 --- a/verification/aeneas/lean/ModelPrelude.lean +++ b/verification/aeneas/lean/ModelPrelude.lean @@ -8,7 +8,7 @@ those terms. -/ module public import RustModel -public import Zerocopy.TypesExternal +public import Zerocopy.Types @[expose] public section /-! @@ -25,6 +25,20 @@ decoders test that condition and preserve its proof in the accepted value. open Aeneas.Std namespace AeneasSpecs +-- The imported PhantomData carrier has no runtime fields. Its value model +-- records only that empty stored value; it makes no claim about ownership, +-- variance, drop checking, or pointer provenance. +@[reducible] instance modelPhantomData (T : Type) : + RustModel (Zerocopy.core.marker.PhantomData T) := + { Model := Unit, «decode» := fun _ => some () } + +/-- This check fails if the pinned extracted carrier gains runtime fields. -/ +theorem phantomData_eq_mk (T : Type) (raw : Zerocopy.core.marker.PhantomData T) : + raw = Zerocopy.core.marker.PhantomData.mk := by + cases raw + rfl + + -- The bounds are proofs stored beside the value. They contribute constraints -- to the mathematical type without another runtime field or admission test. structure UnsignedWord (ty : UScalarTy) where diff --git a/verification/aeneas/lean/Obligations/Byteorder.lean b/verification/aeneas/lean/Obligations/Byteorder.lean new file mode 100644 index 0000000000..580f41b132 --- /dev/null +++ b/verification/aeneas/lean/Obligations/Byteorder.lean @@ -0,0 +1,117 @@ +/- 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 +@[expose] public section + +open Aeneas Aeneas.Std +namespace Zerocopy.Obligations + +/- These byteorder expectations retain the raw input domain. Readers must +return the positional base-256 value; writers must return every numeric byte, +including zeros. They deliberately use explicit digit arithmetic rather than +invoking the authored specification's shared decoder or encoder. -/ + +def read_u16_le_spec_contract (bytes : Aeneas.Std.Array U8 2#usize) + (run : Result (U16)) : Prop := + run ⦃ output => output.val = bytes.val[0]!.val + 256 * (bytes.val[1]!.val) ⦄ + +def read_u16_le_spec : Prop := + ∀ (bytes : Aeneas.Std.Array U8 2#usize), read_u16_le_spec_contract bytes + (byteorder.verification.read_u16_le bytes) + +def write_u16_le_spec_contract (n : U16) + (run : Result (Aeneas.Std.Array U8 2#usize)) : Prop := + run ⦃ output => output.val.map UScalar.val = [n.val % 256, n.val / 256 % 256] ⦄ + +def write_u16_le_spec : Prop := + ∀ (n : U16), write_u16_le_spec_contract n + (byteorder.verification.write_u16_le n) + +def set_u16_le_spec_contract (_bytes : Aeneas.Std.Array U8 2#usize) (n : U16) + (run : Result (U16)) : Prop := + run ⦃ output => output = n ⦄ + +def set_u16_le_spec : Prop := + ∀ (bytes : Aeneas.Std.Array U8 2#usize) (n : U16), set_u16_le_spec_contract bytes n + (byteorder.verification.set_u16_le bytes n) + +def read_u16_be_spec_contract (bytes : Aeneas.Std.Array U8 2#usize) + (run : Result (U16)) : Prop := + run ⦃ output => output.val = bytes.val[1]!.val + 256 * (bytes.val[0]!.val) ⦄ + +def read_u16_be_spec : Prop := + ∀ (bytes : Aeneas.Std.Array U8 2#usize), read_u16_be_spec_contract bytes + (byteorder.verification.read_u16_be bytes) + +def write_u16_be_spec_contract (n : U16) + (run : Result (Aeneas.Std.Array U8 2#usize)) : Prop := + run ⦃ output => output.val.map UScalar.val = [n.val / 256 % 256, n.val % 256] ⦄ + +def write_u16_be_spec : Prop := + ∀ (n : U16), write_u16_be_spec_contract n + (byteorder.verification.write_u16_be n) + +def set_u16_be_spec_contract (_bytes : Aeneas.Std.Array U8 2#usize) (n : U16) + (run : Result (U16)) : Prop := + run ⦃ output => output = n ⦄ + +def set_u16_be_spec : Prop := + ∀ (bytes : Aeneas.Std.Array U8 2#usize) (n : U16), set_u16_be_spec_contract bytes n + (byteorder.verification.set_u16_be bytes n) + +def read_u32_le_spec_contract (bytes : Aeneas.Std.Array U8 4#usize) + (run : Result (U32)) : Prop := + run ⦃ output => output.val = bytes.val[0]!.val + 256 * (bytes.val[1]!.val + 256 * (bytes.val[2]!.val + 256 * (bytes.val[3]!.val))) ⦄ + +def read_u32_le_spec : Prop := + ∀ (bytes : Aeneas.Std.Array U8 4#usize), read_u32_le_spec_contract bytes + (byteorder.verification.read_u32_le bytes) + +def write_u32_le_spec_contract (n : U32) + (run : Result (Aeneas.Std.Array U8 4#usize)) : Prop := + run ⦃ output => output.val.map UScalar.val = [n.val % 256, n.val / 256 % 256, n.val / 65536 % 256, n.val / 16777216 % 256] ⦄ + +def write_u32_le_spec : Prop := + ∀ (n : U32), write_u32_le_spec_contract n + (byteorder.verification.write_u32_le n) + +def set_u32_le_spec_contract (_bytes : Aeneas.Std.Array U8 4#usize) (n : U32) + (run : Result (U32)) : Prop := + run ⦃ output => output = n ⦄ + +def set_u32_le_spec : Prop := + ∀ (bytes : Aeneas.Std.Array U8 4#usize) (n : U32), set_u32_le_spec_contract bytes n + (byteorder.verification.set_u32_le bytes n) + +def read_u32_be_spec_contract (bytes : Aeneas.Std.Array U8 4#usize) + (run : Result (U32)) : Prop := + run ⦃ output => output.val = bytes.val[3]!.val + 256 * (bytes.val[2]!.val + 256 * (bytes.val[1]!.val + 256 * (bytes.val[0]!.val))) ⦄ + +def read_u32_be_spec : Prop := + ∀ (bytes : Aeneas.Std.Array U8 4#usize), read_u32_be_spec_contract bytes + (byteorder.verification.read_u32_be bytes) + +def write_u32_be_spec_contract (n : U32) + (run : Result (Aeneas.Std.Array U8 4#usize)) : Prop := + run ⦃ output => output.val.map UScalar.val = [n.val / 16777216 % 256, n.val / 65536 % 256, n.val / 256 % 256, n.val % 256] ⦄ + +def write_u32_be_spec : Prop := + ∀ (n : U32), write_u32_be_spec_contract n + (byteorder.verification.write_u32_be n) + +def set_u32_be_spec_contract (_bytes : Aeneas.Std.Array U8 4#usize) (n : U32) + (run : Result (U32)) : Prop := + run ⦃ output => output = n ⦄ + +def set_u32_be_spec : Prop := + ∀ (bytes : Aeneas.Std.Array U8 4#usize) (n : U32), set_u32_be_spec_contract bytes n + (byteorder.verification.set_u32_be bytes n) + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs/Byteorder.lean b/verification/aeneas/lean/Proofs/Byteorder.lean new file mode 100644 index 0000000000..83cb21701a --- /dev/null +++ b/verification/aeneas/lean/Proofs/Byteorder.lean @@ -0,0 +1,275 @@ +/- 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 BytesAdapter +@[expose] public section + +/-! +The raw lemmas check the extracted constructors, accessors and setters. The +canonical proofs then transport those facts through the ordinary scalar and +array decoders without adding input restrictions. +-/ + +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs.Raw + +theorem read_u16_le (bytes : Aeneas.Std.Array U8 2#usize) : + byteorder.verification.read_u16_le bytes + ⦃ output => output.val = Rust.Bytes.decodeLE (bytes.val.map U8.bv) ⦄ := by + simp only [byteorder.verification.read_u16_le, byteorder.U16.from_bytes, + byteorder.U16.get, byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder.ORDER, bind_ok, WP.spec_ok] + simp only [core.num.U16.from_le_bytes, UScalar.val, BitVec.toNat_cast] + exact Rust.Bytes.AeneasAdapter.fromLEBytes_toNat _ + +theorem write_u16_le (n : U16) : + byteorder.verification.write_u16_le n + ⦃ output => output.val.map U8.bv = Rust.Bytes.encodeLE 2 n.val ⦄ := by + have digits : (core.num.U16.to_le_bytes n).val.map U8.bv = n.bv.toLEBytes := by + simp only [core.num.U16.to_le_bytes, Array.from_val, List.map_map, + ↓U8.bv_UScalar_mk, List.map_id] + simp only [byteorder.verification.write_u16_le, byteorder.U16.new, + core.convert.IntoFrom.into, ArrayU82.Insts.CoreConvertFromU16.from, + byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder.ORDER, lift, bind_ok, WP.spec_ok] + rw [digits] + exact Rust.Bytes.AeneasAdapter.toLEBytes_eq_encodeLE (by decide) n.bv + +theorem set_u16_le (bytes : Aeneas.Std.Array U8 2#usize) (n : U16) : + byteorder.verification.set_u16_le bytes n ⦃ output => output = n ⦄ := by + have digits : (core.num.U16.to_le_bytes n).val.map U8.bv = n.bv.toLEBytes := by + simp only [core.num.U16.to_le_bytes, Array.from_val, List.map_map, + ↓U8.bv_UScalar_mk, List.map_id] + simp only [byteorder.verification.set_u16_le, byteorder.U16.from_bytes, + byteorder.U16.set, byteorder.U16.new, byteorder.U16.get, + byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder.ORDER, lift, bind_ok, WP.spec_ok] + apply UScalar.eq_of_val_eq + change (BitVec.fromLEBytes ((core.num.U16.to_le_bytes n).val.map U8.bv)).toNat = n.bv.toNat + rw [digits, Rust.Bytes.AeneasAdapter.fromLEBytes_toNat] + exact Rust.Bytes.AeneasAdapter.decodeLE_toLEBytes (by decide) n.bv + +theorem read_u16_be (bytes : Aeneas.Std.Array U8 2#usize) : + byteorder.verification.read_u16_be bytes + ⦃ output => output.val = Rust.Bytes.decodeBE (bytes.val.map U8.bv) ⦄ := by + simp only [byteorder.verification.read_u16_be, byteorder.U16.from_bytes, + byteorder.U16.get, byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder.ORDER, bind_ok, WP.spec_ok] + simp only [core.num.U16.from_be_bytes, UScalar.val, BitVec.toNat_cast] + exact Rust.Bytes.AeneasAdapter.fromBEBytes_toNat _ + +theorem write_u16_be (n : U16) : + byteorder.verification.write_u16_be n + ⦃ output => output.val.map U8.bv = Rust.Bytes.encodeBE 2 n.val ⦄ := by + have digits : (core.num.U16.to_be_bytes n).val.map U8.bv = n.bv.toBEBytes := by + simp only [core.num.U16.to_be_bytes, Array.from_val, List.map_map, + ↓U8.bv_UScalar_mk, List.map_id] + simp only [byteorder.verification.write_u16_be, byteorder.U16.new, + core.convert.IntoFrom.into, ArrayU82.Insts.CoreConvertFromU16.from, + byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder.ORDER, lift, bind_ok, WP.spec_ok] + rw [digits] + exact Rust.Bytes.AeneasAdapter.toBEBytes_eq_encodeBE (by decide) n.bv + +theorem set_u16_be (bytes : Aeneas.Std.Array U8 2#usize) (n : U16) : + byteorder.verification.set_u16_be bytes n ⦃ output => output = n ⦄ := by + have digits : (core.num.U16.to_be_bytes n).val.map U8.bv = n.bv.toBEBytes := by + simp only [core.num.U16.to_be_bytes, Array.from_val, List.map_map, + ↓U8.bv_UScalar_mk, List.map_id] + simp only [byteorder.verification.set_u16_be, byteorder.U16.from_bytes, + byteorder.U16.set, byteorder.U16.new, byteorder.U16.get, + byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder.ORDER, lift, bind_ok, WP.spec_ok] + apply UScalar.eq_of_val_eq + change (BitVec.fromBEBytes ((core.num.U16.to_be_bytes n).val.map U8.bv)).toNat = n.bv.toNat + rw [digits, Rust.Bytes.AeneasAdapter.fromBEBytes_toNat] + exact Rust.Bytes.AeneasAdapter.decodeBE_toBEBytes (by decide) n.bv + +theorem read_u32_le (bytes : Aeneas.Std.Array U8 4#usize) : + byteorder.verification.read_u32_le bytes + ⦃ output => output.val = Rust.Bytes.decodeLE (bytes.val.map U8.bv) ⦄ := by + simp only [byteorder.verification.read_u32_le, byteorder.U32.from_bytes, + byteorder.U32.get, byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder.ORDER, bind_ok, WP.spec_ok] + simp only [core.num.U32.from_le_bytes, UScalar.val, BitVec.toNat_cast] + exact Rust.Bytes.AeneasAdapter.fromLEBytes_toNat _ + +theorem write_u32_le (n : U32) : + byteorder.verification.write_u32_le n + ⦃ output => output.val.map U8.bv = Rust.Bytes.encodeLE 4 n.val ⦄ := by + have digits : (core.num.U32.to_le_bytes n).val.map U8.bv = n.bv.toLEBytes := by + simp only [core.num.U32.to_le_bytes, Array.from_val, List.map_map, + ↓U8.bv_UScalar_mk, List.map_id] + simp only [byteorder.verification.write_u32_le, byteorder.U32.new, + core.convert.IntoFrom.into, ArrayU84.Insts.CoreConvertFromU32.from, + byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder.ORDER, lift, bind_ok, WP.spec_ok] + rw [digits] + exact Rust.Bytes.AeneasAdapter.toLEBytes_eq_encodeLE (by decide) n.bv + +theorem set_u32_le (bytes : Aeneas.Std.Array U8 4#usize) (n : U32) : + byteorder.verification.set_u32_le bytes n ⦃ output => output = n ⦄ := by + have digits : (core.num.U32.to_le_bytes n).val.map U8.bv = n.bv.toLEBytes := by + simp only [core.num.U32.to_le_bytes, Array.from_val, List.map_map, + ↓U8.bv_UScalar_mk, List.map_id] + simp only [byteorder.verification.set_u32_le, byteorder.U32.from_bytes, + byteorder.U32.set, byteorder.U32.new, byteorder.U32.get, + byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder.ORDER, lift, bind_ok, WP.spec_ok] + apply UScalar.eq_of_val_eq + change (BitVec.fromLEBytes ((core.num.U32.to_le_bytes n).val.map U8.bv)).toNat = n.bv.toNat + rw [digits, Rust.Bytes.AeneasAdapter.fromLEBytes_toNat] + exact Rust.Bytes.AeneasAdapter.decodeLE_toLEBytes (by decide) n.bv + +theorem read_u32_be (bytes : Aeneas.Std.Array U8 4#usize) : + byteorder.verification.read_u32_be bytes + ⦃ output => output.val = Rust.Bytes.decodeBE (bytes.val.map U8.bv) ⦄ := by + simp only [byteorder.verification.read_u32_be, byteorder.U32.from_bytes, + byteorder.U32.get, byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder.ORDER, bind_ok, WP.spec_ok] + simp only [core.num.U32.from_be_bytes, UScalar.val, BitVec.toNat_cast] + exact Rust.Bytes.AeneasAdapter.fromBEBytes_toNat _ + +theorem write_u32_be (n : U32) : + byteorder.verification.write_u32_be n + ⦃ output => output.val.map U8.bv = Rust.Bytes.encodeBE 4 n.val ⦄ := by + have digits : (core.num.U32.to_be_bytes n).val.map U8.bv = n.bv.toBEBytes := by + simp only [core.num.U32.to_be_bytes, Array.from_val, List.map_map, + ↓U8.bv_UScalar_mk, List.map_id] + simp only [byteorder.verification.write_u32_be, byteorder.U32.new, + core.convert.IntoFrom.into, ArrayU84.Insts.CoreConvertFromU32.from, + byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder.ORDER, lift, bind_ok, WP.spec_ok] + rw [digits] + exact Rust.Bytes.AeneasAdapter.toBEBytes_eq_encodeBE (by decide) n.bv + +theorem set_u32_be (bytes : Aeneas.Std.Array U8 4#usize) (n : U32) : + byteorder.verification.set_u32_be bytes n ⦃ output => output = n ⦄ := by + have digits : (core.num.U32.to_be_bytes n).val.map U8.bv = n.bv.toBEBytes := by + simp only [core.num.U32.to_be_bytes, Array.from_val, List.map_map, + ↓U8.bv_UScalar_mk, List.map_id] + simp only [byteorder.verification.set_u32_be, byteorder.U32.from_bytes, + byteorder.U32.set, byteorder.U32.new, byteorder.U32.get, + byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder.ORDER, lift, bind_ok, WP.spec_ok] + apply UScalar.eq_of_val_eq + change (BitVec.fromBEBytes ((core.num.U32.to_be_bytes n).val.map U8.bv)).toNat = n.bv.toNat + rw [digits, Rust.Bytes.AeneasAdapter.fromBEBytes_toNat] + exact Rust.Bytes.AeneasAdapter.decodeBE_toBEBytes (by decide) n.bv + +end Zerocopy.Proofs.Raw + +namespace Zerocopy.Proofs + +theorem read_u16_le_spec : Specs.read_u16_le_spec := by + intro bytes value decoded + apply WP.spec_mono (Raw.read_u16_le bytes) + intro output facts + refine ⟨unsignedWord output, rfl, ?_⟩ + change output.val = Rust.Bytes.decodeLE _ + rw [decodedArray_bytes_eq bytes value decoded] + exact facts + +theorem write_u16_le_spec : Specs.write_u16_le_spec := by + intro n value decoded + have same := (decodeUScalar_iff n value).mp decoded + apply WP.spec_mono (Raw.write_u16_le n) + intro output facts + refine ⟨unsignedArray output, decodeArray_unsigned output, ?_⟩ + change (unsignedArray output).val.map (fun byte => BitVec.ofNat 8 (byte : Nat)) = + Rust.Bytes.encodeLE 2 value.value + rw [decodedArray_bytes_eq output (unsignedArray output) (decodeArray_unsigned output)] + rw [← same] + exact facts + +theorem set_u16_le_spec : Specs.set_u16_le_spec := by + intro bytes n _ _ value decoded + apply WP.spec_mono (Raw.set_u16_le bytes n) + intro output facts + subst output + refine ⟨unsignedWord n, rfl, ?_⟩ + exact Option.some.inj decoded + +theorem read_u16_be_spec : Specs.read_u16_be_spec := by + intro bytes value decoded + apply WP.spec_mono (Raw.read_u16_be bytes) + intro output facts + refine ⟨unsignedWord output, rfl, ?_⟩ + change output.val = Rust.Bytes.decodeBE _ + rw [decodedArray_bytes_eq bytes value decoded] + exact facts + +theorem write_u16_be_spec : Specs.write_u16_be_spec := by + intro n value decoded + have same := (decodeUScalar_iff n value).mp decoded + apply WP.spec_mono (Raw.write_u16_be n) + intro output facts + refine ⟨unsignedArray output, decodeArray_unsigned output, ?_⟩ + change (unsignedArray output).val.map (fun byte => BitVec.ofNat 8 (byte : Nat)) = + Rust.Bytes.encodeBE 2 value.value + rw [decodedArray_bytes_eq output (unsignedArray output) (decodeArray_unsigned output)] + rw [← same] + exact facts + +theorem set_u16_be_spec : Specs.set_u16_be_spec := by + intro bytes n _ _ value decoded + apply WP.spec_mono (Raw.set_u16_be bytes n) + intro output facts + subst output + refine ⟨unsignedWord n, rfl, ?_⟩ + exact Option.some.inj decoded + +theorem read_u32_le_spec : Specs.read_u32_le_spec := by + intro bytes value decoded + apply WP.spec_mono (Raw.read_u32_le bytes) + intro output facts + refine ⟨unsignedWord output, rfl, ?_⟩ + change output.val = Rust.Bytes.decodeLE _ + rw [decodedArray_bytes_eq bytes value decoded] + exact facts + +theorem write_u32_le_spec : Specs.write_u32_le_spec := by + intro n value decoded + have same := (decodeUScalar_iff n value).mp decoded + apply WP.spec_mono (Raw.write_u32_le n) + intro output facts + refine ⟨unsignedArray output, decodeArray_unsigned output, ?_⟩ + change (unsignedArray output).val.map (fun byte => BitVec.ofNat 8 (byte : Nat)) = + Rust.Bytes.encodeLE 4 value.value + rw [decodedArray_bytes_eq output (unsignedArray output) (decodeArray_unsigned output)] + rw [← same] + exact facts + +theorem set_u32_le_spec : Specs.set_u32_le_spec := by + intro bytes n _ _ value decoded + apply WP.spec_mono (Raw.set_u32_le bytes n) + intro output facts + subst output + refine ⟨unsignedWord n, rfl, ?_⟩ + exact Option.some.inj decoded + +theorem read_u32_be_spec : Specs.read_u32_be_spec := by + intro bytes value decoded + apply WP.spec_mono (Raw.read_u32_be bytes) + intro output facts + refine ⟨unsignedWord output, rfl, ?_⟩ + change output.val = Rust.Bytes.decodeBE _ + rw [decodedArray_bytes_eq bytes value decoded] + exact facts + +theorem write_u32_be_spec : Specs.write_u32_be_spec := by + intro n value decoded + have same := (decodeUScalar_iff n value).mp decoded + apply WP.spec_mono (Raw.write_u32_be n) + intro output facts + refine ⟨unsignedArray output, decodeArray_unsigned output, ?_⟩ + change (unsignedArray output).val.map (fun byte => BitVec.ofNat 8 (byte : Nat)) = + Rust.Bytes.encodeBE 4 value.value + rw [decodedArray_bytes_eq output (unsignedArray output) (decodeArray_unsigned output)] + rw [← same] + exact facts + +theorem set_u32_be_spec : Specs.set_u32_be_spec := by + intro bytes n _ _ value decoded + apply WP.spec_mono (Raw.set_u32_be bytes n) + intro output facts + subst output + refine ⟨unsignedWord n, rfl, ?_⟩ + exact Option.some.inj decoded + +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/RequiredModelContracts/Byteorder.lean b/verification/aeneas/lean/RequiredModelContracts/Byteorder.lean new file mode 100644 index 0000000000..f20154b9bb --- /dev/null +++ b/verification/aeneas/lean/RequiredModelContracts/Byteorder.lean @@ -0,0 +1,194 @@ +/- 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 RequiredContracts +public import Specs +public import BytesAdapter +public import Obligations.Byteorder +@[expose] public section + +/-! +These implications inspect an arbitrary execution outcome and use only its +supplied mathematical contract. Total scalar-array decoding covers every raw +input. The recovered observations are the separately stated positional sums, +complete numeric byte lists and exact setter results. +-/ + +open Aeneas Aeneas.Std AeneasSpecs +namespace Zerocopy.Proofs + +theorem byteorder_decode_u16_le (bytes : Aeneas.Std.Array U8 2#usize) : + Rust.Bytes.decodeLE (bytes.val.map U8.bv) = bytes.val[0]!.val + 256 * (bytes.val[1]!.val) := by + obtain ⟨b0, b1, same⟩ := List.length_eq_two.mp + (show bytes.val.length = 2 by simp) + simp [same, Rust.Bytes.decodeLE] + +@[contract_simps] theorem required_read_u16_le (bytes : Aeneas.Std.Array U8 2#usize) + (run : Result U16) (provided : Specs.read_u16_le_spec_contract bytes run) : + Obligations.read_u16_le_spec_contract bytes run := by + apply WP.spec_mono (provided (unsignedArray bytes) (decodeArray_unsigned bytes)) + rintro output ⟨value, decoded, facts⟩ + have same := (decodeUScalar_iff output value).mp decoded + change value.value = Rust.Bytes.decodeLE _ at facts + rw [decodedArray_bytes_eq bytes (unsignedArray bytes) (decodeArray_unsigned bytes)] at facts + change output.val = _ + rw [same, facts] + exact byteorder_decode_u16_le bytes + +@[contract_simps] theorem required_write_u16_le (n : U16) + (run : Result (Aeneas.Std.Array U8 2#usize)) (provided : Specs.write_u16_le_spec_contract n run) : + Obligations.write_u16_le_spec_contract n run := by + apply WP.spec_mono (provided (unsignedWord n) rfl) + rintro output ⟨value, decoded, facts⟩ + change value.val.map (fun byte => BitVec.ofNat 8 (byte : Nat)) = + Rust.Bytes.encodeLE 2 n.val at facts + rw [decodedArray_bytes_eq output value decoded] at facts + have digits := congrArg (List.map BitVec.toNat) facts + change output.val.map UScalar.val = _ + simpa [List.map_map, Function.comp_def, Rust.Bytes.encodeBE, + Rust.Bytes.encodeLE, BitVec.toNat_ofNat, Nat.div_div_eq_div_mul] using digits + +@[contract_simps] theorem required_set_u16_le (bytes : Aeneas.Std.Array U8 2#usize) (n : U16) + (run : Result U16) (provided : Specs.set_u16_le_spec_contract bytes n run) : + Obligations.set_u16_le_spec_contract bytes n run := by + apply WP.spec_mono (provided (unsignedArray bytes) (decodeArray_unsigned bytes) + (unsignedWord n) rfl) + rintro output ⟨value, decoded, facts⟩ + apply UScalar.eq_of_val_eq + have same := (decodeUScalar_iff output value).mp decoded + rw [same] + exact congrArg UnsignedWord.value facts + +theorem byteorder_decode_u16_be (bytes : Aeneas.Std.Array U8 2#usize) : + Rust.Bytes.decodeBE (bytes.val.map U8.bv) = bytes.val[1]!.val + 256 * (bytes.val[0]!.val) := by + obtain ⟨b0, b1, same⟩ := List.length_eq_two.mp + (show bytes.val.length = 2 by simp) + simp [same, Rust.Bytes.decodeBE, Rust.Bytes.decodeLE] + +@[contract_simps] theorem required_read_u16_be (bytes : Aeneas.Std.Array U8 2#usize) + (run : Result U16) (provided : Specs.read_u16_be_spec_contract bytes run) : + Obligations.read_u16_be_spec_contract bytes run := by + apply WP.spec_mono (provided (unsignedArray bytes) (decodeArray_unsigned bytes)) + rintro output ⟨value, decoded, facts⟩ + have same := (decodeUScalar_iff output value).mp decoded + change value.value = Rust.Bytes.decodeBE _ at facts + rw [decodedArray_bytes_eq bytes (unsignedArray bytes) (decodeArray_unsigned bytes)] at facts + change output.val = _ + rw [same, facts] + exact byteorder_decode_u16_be bytes + +@[contract_simps] theorem required_write_u16_be (n : U16) + (run : Result (Aeneas.Std.Array U8 2#usize)) (provided : Specs.write_u16_be_spec_contract n run) : + Obligations.write_u16_be_spec_contract n run := by + apply WP.spec_mono (provided (unsignedWord n) rfl) + rintro output ⟨value, decoded, facts⟩ + change value.val.map (fun byte => BitVec.ofNat 8 (byte : Nat)) = + Rust.Bytes.encodeBE 2 n.val at facts + rw [decodedArray_bytes_eq output value decoded] at facts + have digits := congrArg (List.map BitVec.toNat) facts + change output.val.map UScalar.val = _ + simpa [List.map_map, Function.comp_def, Rust.Bytes.encodeBE, + Rust.Bytes.encodeLE, BitVec.toNat_ofNat, Nat.div_div_eq_div_mul] using digits + +@[contract_simps] theorem required_set_u16_be (bytes : Aeneas.Std.Array U8 2#usize) (n : U16) + (run : Result U16) (provided : Specs.set_u16_be_spec_contract bytes n run) : + Obligations.set_u16_be_spec_contract bytes n run := by + apply WP.spec_mono (provided (unsignedArray bytes) (decodeArray_unsigned bytes) + (unsignedWord n) rfl) + rintro output ⟨value, decoded, facts⟩ + apply UScalar.eq_of_val_eq + have same := (decodeUScalar_iff output value).mp decoded + rw [same] + exact congrArg UnsignedWord.value facts + +theorem byteorder_decode_u32_le (bytes : Aeneas.Std.Array U8 4#usize) : + Rust.Bytes.decodeLE (bytes.val.map U8.bv) = bytes.val[0]!.val + 256 * (bytes.val[1]!.val + 256 * (bytes.val[2]!.val + 256 * (bytes.val[3]!.val))) := by + obtain ⟨b0, b1, b2, b3, same⟩ := List.length_eq_four.mp + (show bytes.val.length = 4 by simp) + simp [same, Rust.Bytes.decodeLE] + +@[contract_simps] theorem required_read_u32_le (bytes : Aeneas.Std.Array U8 4#usize) + (run : Result U32) (provided : Specs.read_u32_le_spec_contract bytes run) : + Obligations.read_u32_le_spec_contract bytes run := by + apply WP.spec_mono (provided (unsignedArray bytes) (decodeArray_unsigned bytes)) + rintro output ⟨value, decoded, facts⟩ + have same := (decodeUScalar_iff output value).mp decoded + change value.value = Rust.Bytes.decodeLE _ at facts + rw [decodedArray_bytes_eq bytes (unsignedArray bytes) (decodeArray_unsigned bytes)] at facts + change output.val = _ + rw [same, facts] + exact byteorder_decode_u32_le bytes + +@[contract_simps] theorem required_write_u32_le (n : U32) + (run : Result (Aeneas.Std.Array U8 4#usize)) (provided : Specs.write_u32_le_spec_contract n run) : + Obligations.write_u32_le_spec_contract n run := by + apply WP.spec_mono (provided (unsignedWord n) rfl) + rintro output ⟨value, decoded, facts⟩ + change value.val.map (fun byte => BitVec.ofNat 8 (byte : Nat)) = + Rust.Bytes.encodeLE 4 n.val at facts + rw [decodedArray_bytes_eq output value decoded] at facts + have digits := congrArg (List.map BitVec.toNat) facts + change output.val.map UScalar.val = _ + simpa [List.map_map, Function.comp_def, Rust.Bytes.encodeBE, + Rust.Bytes.encodeLE, BitVec.toNat_ofNat, Nat.div_div_eq_div_mul] using digits + +@[contract_simps] theorem required_set_u32_le (bytes : Aeneas.Std.Array U8 4#usize) (n : U32) + (run : Result U32) (provided : Specs.set_u32_le_spec_contract bytes n run) : + Obligations.set_u32_le_spec_contract bytes n run := by + apply WP.spec_mono (provided (unsignedArray bytes) (decodeArray_unsigned bytes) + (unsignedWord n) rfl) + rintro output ⟨value, decoded, facts⟩ + apply UScalar.eq_of_val_eq + have same := (decodeUScalar_iff output value).mp decoded + rw [same] + exact congrArg UnsignedWord.value facts + +theorem byteorder_decode_u32_be (bytes : Aeneas.Std.Array U8 4#usize) : + Rust.Bytes.decodeBE (bytes.val.map U8.bv) = bytes.val[3]!.val + 256 * (bytes.val[2]!.val + 256 * (bytes.val[1]!.val + 256 * (bytes.val[0]!.val))) := by + obtain ⟨b0, b1, b2, b3, same⟩ := List.length_eq_four.mp + (show bytes.val.length = 4 by simp) + simp [same, Rust.Bytes.decodeBE, Rust.Bytes.decodeLE] + +@[contract_simps] theorem required_read_u32_be (bytes : Aeneas.Std.Array U8 4#usize) + (run : Result U32) (provided : Specs.read_u32_be_spec_contract bytes run) : + Obligations.read_u32_be_spec_contract bytes run := by + apply WP.spec_mono (provided (unsignedArray bytes) (decodeArray_unsigned bytes)) + rintro output ⟨value, decoded, facts⟩ + have same := (decodeUScalar_iff output value).mp decoded + change value.value = Rust.Bytes.decodeBE _ at facts + rw [decodedArray_bytes_eq bytes (unsignedArray bytes) (decodeArray_unsigned bytes)] at facts + change output.val = _ + rw [same, facts] + exact byteorder_decode_u32_be bytes + +@[contract_simps] theorem required_write_u32_be (n : U32) + (run : Result (Aeneas.Std.Array U8 4#usize)) (provided : Specs.write_u32_be_spec_contract n run) : + Obligations.write_u32_be_spec_contract n run := by + apply WP.spec_mono (provided (unsignedWord n) rfl) + rintro output ⟨value, decoded, facts⟩ + change value.val.map (fun byte => BitVec.ofNat 8 (byte : Nat)) = + Rust.Bytes.encodeBE 4 n.val at facts + rw [decodedArray_bytes_eq output value decoded] at facts + have digits := congrArg (List.map BitVec.toNat) facts + change output.val.map UScalar.val = _ + simpa [List.map_map, Function.comp_def, Rust.Bytes.encodeBE, + Rust.Bytes.encodeLE, BitVec.toNat_ofNat, Nat.div_div_eq_div_mul] using digits + +@[contract_simps] theorem required_set_u32_be (bytes : Aeneas.Std.Array U8 4#usize) (n : U32) + (run : Result U32) (provided : Specs.set_u32_be_spec_contract bytes n run) : + Obligations.set_u32_be_spec_contract bytes n run := by + apply WP.spec_mono (provided (unsignedArray bytes) (decodeArray_unsigned bytes) + (unsignedWord n) rfl) + rintro output ⟨value, decoded, facts⟩ + apply UScalar.eq_of_val_eq + have same := (decodeUScalar_iff output value).mp decoded + rw [same] + exact congrArg UnsignedWord.value facts + +end Zerocopy.Proofs diff --git a/verification/aeneas/projections/ModelShapes.lean b/verification/aeneas/projections/ModelShapes.lean index dcfde584a6..b6adf01dfc 100644 --- a/verification/aeneas/projections/ModelShapes.lean +++ b/verification/aeneas/projections/ModelShapes.lean @@ -14,3 +14,13 @@ public import DeriveModels open Aeneas Aeneas.Std AeneasSpecs +derive_model_shape Zerocopy.byteorder.Order with 0 type parameters + +derive_model_shape Zerocopy.byteorder.BigEndian with 0 type parameters + +derive_model_shape Zerocopy.byteorder.LittleEndian with 0 type parameters + +derive_model_shape Zerocopy.byteorder.U16 with 1 type parameters + +derive_model_shape Zerocopy.byteorder.U32 with 1 type parameters + diff --git a/verification/aeneas/projections/Models.lean b/verification/aeneas/projections/Models.lean index 8ac2c48319..2d0496a35e 100644 --- a/verification/aeneas/projections/Models.lean +++ b/verification/aeneas/projections/Models.lean @@ -13,3 +13,18 @@ public import DeriveModels open Aeneas Aeneas.Std AeneasSpecs +derive_rust_model Zerocopy.byteorder.Order with 0 type parameters +check_model_binding Zerocopy.byteorder.Order with 0 type parameters + +derive_rust_model Zerocopy.byteorder.BigEndian with 0 type parameters +check_model_binding Zerocopy.byteorder.BigEndian with 0 type parameters + +derive_rust_model Zerocopy.byteorder.LittleEndian with 0 type parameters +check_model_binding Zerocopy.byteorder.LittleEndian with 0 type parameters + +derive_rust_model Zerocopy.byteorder.U16 with 1 type parameters +check_model_binding Zerocopy.byteorder.U16 with 1 type parameters + +derive_rust_model Zerocopy.byteorder.U32 with 1 type parameters +check_model_binding Zerocopy.byteorder.U32 with 1 type parameters + diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean index 0651aba92d..0980ee4e4f 100644 --- a/verification/aeneas/projections/Specs.lean +++ b/verification/aeneas/projections/Specs.lean @@ -17,6 +17,110 @@ open Aeneas Aeneas.Std open Zerocopy.Proofs namespace Zerocopy.Specs +check_model_inputs Zerocopy.byteorder.verification.read_u16_le with 0 type parameters +aeneas_spec_begin +spec read_u16_le_spec + for @Zerocopy.byteorder.verification.read_u16_le with 0 type parameters + ensures n => (n : Nat) = Rust.Bytes.decodeLE + (bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat))) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.read_u16_le_spec for Zerocopy.byteorder.verification.read_u16_le with 1 + +check_model_inputs Zerocopy.byteorder.verification.write_u16_le with 0 type parameters +aeneas_spec_begin +spec write_u16_le_spec + for @Zerocopy.byteorder.verification.write_u16_le with 0 type parameters + ensures bytes => bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat)) = + Rust.Bytes.encodeLE 2 (n : Nat) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.write_u16_le_spec for Zerocopy.byteorder.verification.write_u16_le with 1 + +check_model_inputs Zerocopy.byteorder.verification.set_u16_le with 0 type parameters +aeneas_spec_begin +spec set_u16_le_spec + for @Zerocopy.byteorder.verification.set_u16_le with 0 type parameters + ensures r => r = n +aeneas_spec_end +check_spec_binding Zerocopy.Specs.set_u16_le_spec for Zerocopy.byteorder.verification.set_u16_le with 2 + +check_model_inputs Zerocopy.byteorder.verification.read_u16_be with 0 type parameters +aeneas_spec_begin +spec read_u16_be_spec + for @Zerocopy.byteorder.verification.read_u16_be with 0 type parameters + ensures n => (n : Nat) = Rust.Bytes.decodeBE + (bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat))) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.read_u16_be_spec for Zerocopy.byteorder.verification.read_u16_be with 1 + +check_model_inputs Zerocopy.byteorder.verification.write_u16_be with 0 type parameters +aeneas_spec_begin +spec write_u16_be_spec + for @Zerocopy.byteorder.verification.write_u16_be with 0 type parameters + ensures bytes => bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat)) = + Rust.Bytes.encodeBE 2 (n : Nat) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.write_u16_be_spec for Zerocopy.byteorder.verification.write_u16_be with 1 + +check_model_inputs Zerocopy.byteorder.verification.set_u16_be with 0 type parameters +aeneas_spec_begin +spec set_u16_be_spec + for @Zerocopy.byteorder.verification.set_u16_be with 0 type parameters + ensures r => r = n +aeneas_spec_end +check_spec_binding Zerocopy.Specs.set_u16_be_spec for Zerocopy.byteorder.verification.set_u16_be with 2 + +check_model_inputs Zerocopy.byteorder.verification.read_u32_le with 0 type parameters +aeneas_spec_begin +spec read_u32_le_spec + for @Zerocopy.byteorder.verification.read_u32_le with 0 type parameters + ensures n => (n : Nat) = Rust.Bytes.decodeLE + (bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat))) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.read_u32_le_spec for Zerocopy.byteorder.verification.read_u32_le with 1 + +check_model_inputs Zerocopy.byteorder.verification.write_u32_le with 0 type parameters +aeneas_spec_begin +spec write_u32_le_spec + for @Zerocopy.byteorder.verification.write_u32_le with 0 type parameters + ensures bytes => bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat)) = + Rust.Bytes.encodeLE 4 (n : Nat) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.write_u32_le_spec for Zerocopy.byteorder.verification.write_u32_le with 1 + +check_model_inputs Zerocopy.byteorder.verification.set_u32_le with 0 type parameters +aeneas_spec_begin +spec set_u32_le_spec + for @Zerocopy.byteorder.verification.set_u32_le with 0 type parameters + ensures r => r = n +aeneas_spec_end +check_spec_binding Zerocopy.Specs.set_u32_le_spec for Zerocopy.byteorder.verification.set_u32_le with 2 + +check_model_inputs Zerocopy.byteorder.verification.read_u32_be with 0 type parameters +aeneas_spec_begin +spec read_u32_be_spec + for @Zerocopy.byteorder.verification.read_u32_be with 0 type parameters + ensures n => (n : Nat) = Rust.Bytes.decodeBE + (bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat))) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.read_u32_be_spec for Zerocopy.byteorder.verification.read_u32_be with 1 + +check_model_inputs Zerocopy.byteorder.verification.write_u32_be with 0 type parameters +aeneas_spec_begin +spec write_u32_be_spec + for @Zerocopy.byteorder.verification.write_u32_be with 0 type parameters + ensures bytes => bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat)) = + Rust.Bytes.encodeBE 4 (n : Nat) +aeneas_spec_end +check_spec_binding Zerocopy.Specs.write_u32_be_spec for Zerocopy.byteorder.verification.write_u32_be with 1 + +check_model_inputs Zerocopy.byteorder.verification.set_u32_be with 0 type parameters +aeneas_spec_begin +spec set_u32_be_spec + for @Zerocopy.byteorder.verification.set_u32_be with 0 type parameters + ensures r => r = n +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.util.padding_needed_for with 0 type parameters aeneas_spec_begin spec padding_lt_alignment diff --git a/zerocopy/src/byteorder.rs b/zerocopy/src/byteorder.rs index fcb74f04b3..f0107a8c6b 100644 --- a/zerocopy/src/byteorder.rs +++ b/zerocopy/src/byteorder.rs @@ -1625,3 +1625,168 @@ mod tests { assert_eq!(val_be_i16.cmp(&val_be_i16), core::cmp::Ordering::Equal); } } + +// These private entry points expose concrete instantiations to Aeneas without +// depending on annotation discovery inside macro expansions. Each contract is +// checked for every input against both golden and live extractions. +#[allow(dead_code)] +mod verification { + use super::{BigEndian, LittleEndian, U16, U32}; + + /// Reads bytes according to their positional numerical value. + /// + /// ```aeneas + /// spec read_u16_le_spec + /// ensures n => (n : Nat) = Rust.Bytes.decodeLE + /// (bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat))) + /// ``` + fn read_u16_le(bytes: [u8; 2]) -> u16 { + U16::::from_bytes(bytes).get() + } + + /// Writes every byte of the integer in the requested order. + /// + /// ```aeneas + /// spec write_u16_le_spec + /// ensures bytes => bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat)) = + /// Rust.Bytes.encodeLE 2 (n : Nat) + /// ``` + fn write_u16_le(n: u16) -> [u8; 2] { + U16::::new(n).into() + } + + /// Setting a wrapper preserves the complete numerical value. + /// + /// ```aeneas + /// spec set_u16_le_spec + /// ensures r => r = n + /// ``` + fn set_u16_le(bytes: [u8; 2], n: u16) -> u16 { + let mut value = U16::::from_bytes(bytes); + value.set(n); + value.get() + } + + /// Reads bytes according to their positional numerical value. + /// + /// ```aeneas + /// spec read_u16_be_spec + /// ensures n => (n : Nat) = Rust.Bytes.decodeBE + /// (bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat))) + /// ``` + fn read_u16_be(bytes: [u8; 2]) -> u16 { + U16::::from_bytes(bytes).get() + } + + /// Writes every byte of the integer in the requested order. + /// + /// ```aeneas + /// spec write_u16_be_spec + /// ensures bytes => bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat)) = + /// Rust.Bytes.encodeBE 2 (n : Nat) + /// ``` + fn write_u16_be(n: u16) -> [u8; 2] { + U16::::new(n).into() + } + + /// Setting a wrapper preserves the complete numerical value. + /// + /// ```aeneas + /// spec set_u16_be_spec + /// ensures r => r = n + /// ``` + fn set_u16_be(bytes: [u8; 2], n: u16) -> u16 { + let mut value = U16::::from_bytes(bytes); + value.set(n); + value.get() + } + + /// Reads bytes according to their positional numerical value. + /// + /// ```aeneas + /// spec read_u32_le_spec + /// ensures n => (n : Nat) = Rust.Bytes.decodeLE + /// (bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat))) + /// ``` + fn read_u32_le(bytes: [u8; 4]) -> u32 { + U32::::from_bytes(bytes).get() + } + + /// Writes every byte of the integer in the requested order. + /// + /// ```aeneas + /// spec write_u32_le_spec + /// ensures bytes => bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat)) = + /// Rust.Bytes.encodeLE 4 (n : Nat) + /// ``` + fn write_u32_le(n: u32) -> [u8; 4] { + U32::::new(n).into() + } + + /// Setting a wrapper preserves the complete numerical value. + /// + /// ```aeneas + /// spec set_u32_le_spec + /// ensures r => r = n + /// ``` + fn set_u32_le(bytes: [u8; 4], n: u32) -> u32 { + let mut value = U32::::from_bytes(bytes); + value.set(n); + value.get() + } + + /// Reads bytes according to their positional numerical value. + /// + /// ```aeneas + /// spec read_u32_be_spec + /// ensures n => (n : Nat) = Rust.Bytes.decodeBE + /// (bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat))) + /// ``` + fn read_u32_be(bytes: [u8; 4]) -> u32 { + U32::::from_bytes(bytes).get() + } + + /// Writes every byte of the integer in the requested order. + /// + /// ```aeneas + /// spec write_u32_be_spec + /// ensures bytes => bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat)) = + /// Rust.Bytes.encodeBE 4 (n : Nat) + /// ``` + fn write_u32_be(n: u32) -> [u8; 4] { + U32::::new(n).into() + } + + /// Setting a wrapper preserves the complete numerical value. + /// + /// ```aeneas + /// spec set_u32_be_spec + /// ensures r => r = n + /// ``` + fn set_u32_be(bytes: [u8; 4], n: u32) -> u32 { + let mut value = U32::::from_bytes(bytes); + value.set(n); + value.get() + } + + #[cfg(test)] + mod tests { + use super::*; + + #[test] + fn byte_examples() { + for n in [0, 1, 0x1234, u16::MAX] { + assert_eq!(read_u16_le(write_u16_le(n)), n); + assert_eq!(read_u16_be(write_u16_be(n)), n); + assert_eq!(set_u16_le([0x55; 2], n), n); + assert_eq!(set_u16_be([0x55; 2], n), n); + } + for n in [0, 1, 0x1234_5678, u32::MAX] { + assert_eq!(read_u32_le(write_u32_le(n)), n); + assert_eq!(read_u32_be(write_u32_be(n)), n); + assert_eq!(set_u32_le([0x55; 4], n), n); + assert_eq!(set_u32_be([0x55; 4], n), n); + } + } + } +}