From 21013b4810dcccc195b9c35a871360979551e053 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Wed, 14 Oct 2026 13:49:34 -0400 Subject: [PATCH] Prove wrapper and byteorder IntoBytes implementations Transparent wrappers and byteorder types add no uninitialized storage when their complete payload representation is initialized. Mark the six generic wrapper and twelve concrete byteorder impl sites, then prove each native dictionary from its actual payload decoder. Byteorder F32/F64 store byte arrays; their proofs do not require native floating-point semantics. Validate native repr, fields, generic inputs and before/final identity before assigning local physical decoders. Missing child representations remain missing. Standard Cell, UnsafeCell and ManuallyDrop carriers model stored values only, without claiming mutation, aliasing or destruction. Publish the exact 59-impl scope and Rust correspondence premises. Slices, str, native floats, atomics, SIMD and generated derives remain deferred. Golden/live proof builds and generic witness audits independently check each marked impl under its incoming element law and model premises. gherrit-pr-id: Gmunmfwlfxo5nsdg4ic6omp6if4lggr4 Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/LOWERING_AUDIT.md | 176 +++++-- verification/aeneas/README.md | 432 +++++++++++++----- verification/aeneas/golden/Funs.lean | 366 ++++++++++++++- verification/aeneas/golden/Types.lean | 90 ++++ .../aeneas/golden/TypesExternal_Template.lean | 21 + verification/aeneas/lean/DeriveModels.lean | 3 +- verification/aeneas/lean/ModelPrelude.lean | 11 + .../aeneas/lean/Proofs/IntoBytes.lean | 151 ++++++ .../aeneas/projections/ModelShapes.lean | 24 + verification/aeneas/projections/Models.lean | 36 ++ zerocopy/src/byteorder.rs | 83 +++- zerocopy/src/impls.rs | 28 +- zerocopy/src/wrappers.rs | 14 +- 13 files changed, 1265 insertions(+), 170 deletions(-) diff --git a/verification/aeneas/LOWERING_AUDIT.md b/verification/aeneas/LOWERING_AUDIT.md index db9c129733..5eeb79b31c 100644 --- a/verification/aeneas/LOWERING_AUDIT.md +++ b/verification/aeneas/LOWERING_AUDIT.md @@ -119,47 +119,145 @@ numerical propositions are false. Conversely, they apply inside annotated functions too: finding every annotation does not establish that every relevant operation in its dependency closure was faithfully modeled. -## Pure byte representations and the array law +## Pure byte representations and `IntoBytes` laws -[`Rust.Storage`](../../anneal/lean/Rust/Storage.lean) now represents initialized -and uninitialized bytes and fixed-width physical decoders as pure values. +[`Rust.Storage`](../../anneal/lean/Rust/Storage.lean) represents initialized and +uninitialized bytes and fixed-width physical decoders as pure values. `BitDecoder.Initialized` says that every byte list accepted by a decoder is -initialized. `RustModel.initializedRepresentation` requires this law when a -physical decoder is available and is `False` otherwise. It does not use the -library's mathematical decoder to restrict the byte lists under consideration. - -The array theorem partitions an accepted representation into contiguous element -chunks and proves initialization from the element law. Its proof consumes the -whole byte list, including an empty final remainder, for every count. Counting -elements rather than advancing by a positive byte width also covers empty -arrays and zero-sized elements. - -The Rust interpretation remains an explicit correspondence premise: each -physical decoder's width and admission domain must cover the language-valid -representations of its Rust type. `BitDecoder` does not encode or prove that -premise. A decoder which rejects everything satisfies the initialization law -vacuously, so that law alone cannot justify its use as a Rust representation -model. The current primitive decoders and their array composition must be -reviewed against the [Rust Reference layout](https://doc.rust-lang.org/reference/type-layout.html#array-layout) -and [validity rules](https://doc.rust-lang.org/reference/behavior-considered-undefined.html#invalid-values), -as explained in [README.md](README.md#array-intobytes-initialization-law). -Array size and element offsets exclude padding outside complete element chunks; -padding inside a chunk is covered only by the element's law. - -A nameless `invariant_proof` fence on the ordinary array impl selects that -exact compiler owner, independently of any caller harness. Both AST stages must -retain its original type, usize length, and element dictionary parameters. -The checked ordinary Lean theorem covers that complete native dictionary -application under the element's law and model correspondence premises; the -kernel witness and independent telescope audit reject specialization or added -assumptions. This still relies on the reviewed correspondence from the Rust -impl header to its native dictionary, not merely on a proof name. - -These definitions do not make the existing lowering retain byte storage events, -initialization changes, or pointer provenance. They prove the modeled array -`IntoBytes` trait law under the representation premises, not the runtime -`as_bytes` implementation or general Rust UB-freedom. The typed-transfer and -value-production boundaries above still apply. +initialized. `RustModel.initializedRepresentation` requires an available +physical decoder and this law; absence is `False`. The library's mathematical +`decode` cannot restrict that quantification. A decoder rejecting every byte +list satisfies initialization vacuously, so its law alone does not establish +correspondence with Rust. + +The physical correspondence premise has three parts: decoder width equals the +Rust representation width for the selected type and metadata; every +language-valid representation is admitted with the corresponding raw value; +and every admitted representation denotes a language-valid value. Neither +`BitDecoder` nor a proof of initialization establishes those parts. The +following laws are conditional on those representation premises and the +translation premises already recorded in [SEMANTICS.md](SEMANTICS.md). + +### Exact authored implementation scope + +The default-feature library extraction has 59 nameless `invariant_proof` +markers, each attached through invocation arguments to one native positive +`IntoBytes` impl. This count inventories authored claims; the native binding +manifest and checked implementation-law witnesses establish which compiled +owners fulfill them. + +| Family | Exact Rust carriers and bounds | Count | +| --- | --- | --- | +| Primitive | `()`, `bool`, `char` | 3 | +| Integer | `u8`, `u16`, `u32`, `u64`, `u128`, `usize`, `i8`, `i16`, `i32`, `i64`, `i128`, `isize` | 12 | +| Nonzero | `NonZeroU8`, `NonZeroU16`, `NonZeroU32`, `NonZeroU64`, `NonZeroU128`, `NonZeroUsize`, `NonZeroI8`, `NonZeroI16`, `NonZeroI32`, `NonZeroI64`, `NonZeroI128`, `NonZeroIsize` | 12 | +| Niche option | `Option` for each of the preceding 12 nonzero carriers | 12 | +| Empty marker | `PhantomData` for `T: ?Sized`, without `T: IntoBytes` | 1 | +| Array | `[T; N]` for `T: IntoBytes`, every `const N: usize` | 1 | +| Sized wrapper | `Wrapping`, `Unalign` for `T: IntoBytes` | 2 | +| Possibly unsized wrapper | `ManuallyDrop`, `Cell`, `UnsafeCell`, `ReadOnly` for `T: ?Sized + IntoBytes` | 4 | +| Byteorder | `U16`, `U32`, `U64`, `U128`, `Usize`, `I16`, `I32`, `I64`, `I128`, `Isize`, `F32`, `F64` for every `O`, without `O: ByteOrder` | 12 | + +The source locations are [`impls.rs`](../../zerocopy/src/impls.rs), +[`wrappers.rs`](../../zerocopy/src/wrappers.rs), and +[`byteorder.rs`](../../zerocopy/src/byteorder.rs). The `unsafe_impl!` grouped arm +accepts attributes before each trait; shared proof attributes would duplicate a +source fence and fail unique-owner binding. Single generic calls use leading +attributes. `impl_for_transmute_from!` forwards attributes to its single impl. +`impl_or_verify!` forwards them only to the handwritten implementation. + +`Unalign` and byteorder select that handwritten branch only with neither +`feature = "derive"` nor `cfg(test)`. Their derive/test branches verify separate +derive-generated implementations; these are outside this extraction claim. +Byteorder markers are concrete invocation arguments, not a fence duplicated by +`define_type!`. `F32` and `F64` store `[u8; 4]` and `[u8; 8]`; their laws depend +on those byte arrays, not native floating-point bit semantics. + +Deferred implementations are `[T]`, `str`, native `f32`/`f64` and feature-gated +`f16`/`f128`, atomics under their target/version cfgs, SIMD under its +feature/target/version cfgs, procedural derives, and the generated struct/union +impls of `cryptocorrosion_derive_traits!`. These remain ordinary Rust impls; +this inventory makes no initialization-law certification for them. Neither +core nor zerocopy `MaybeUninit`, non-unit tuples, raw pointers, references, +`NonNull`, nor arbitrary `Option` has an `IntoBytes` impl in this snapshot. +Incoming downstream dictionaries still require their own conditional law +premises; these 59 local markers do not certify future external implementations. + +### Decoder correspondence premises + +Admission currently requires one little-endian 64-bit target, as checked in +[`admission.py`](admission.py). The word decoders use that byte order and an +eight-byte `usize`/`isize`; this is an enforced extraction restriction, not a +Rust guarantee for every target. Integer assembly preserves the full unsigned +word and interprets signed values in two's complement. Every fixed-width word +first requires exactly its width of initialized bytes. + +The following versioned references identify the concrete propositions consumed +by decoder correspondence. Their applicability to the selected compiler and +standard library is an explicit semantic compatibility premise, not a +kernel-checked Rust theorem or an all-release soundness claim. These exact +semantic compatibility propositions are admitted trust premises. Compiler or +standard-library pin changes require review of these propositions and mappings. +The current standard-library documentation reviewed for these mappings reports +Rust 1.99.0 (`b940084d7`, 2026-09-28); archived 1.81/1.85 links also remain in the +adjacent Rust safety comments. Versioned archive URLs were unavailable to the +documentation checker during this update, so that archive verification is not +claimed as new evidence. + +| Decoder | Required language/stdlib proposition and resulting interpretation | +| --- | --- | +| Integers | [Rust 1.81 numeric validity](https://doc.rust-lang.org/1.81.0/reference/types/numeric.html#bit-validity) equates a numeric type's bit validity with its same-size `u8` array; uninitialized `u8` is invalid. Its signed integer definition uses two's complement. The [primitive layout table](https://doc.rust-lang.org/1.81.0/reference/type-layout.html#primitive-data-layout) fixes 1/2/4/8/16-byte integer widths; the target premise fixes pointer-sized words. | +| `bool` | [Rust 1.81 boolean rules](https://doc.rust-lang.org/1.81.0/reference/types/boolean.html) give one-byte layout and the encodings zero/one. The decoder rejects every other byte and every uninitialized byte. | +| `char` | [Rust 1.81 textual rules](https://doc.rust-lang.org/1.81.0/reference/types/textual.html) describe a 32-bit unsigned word representing a Unicode scalar value. Four initialized bytes are decoded; values above `0x10ffff` or in `0xd800..=0xdfff` are rejected. | +| Nonzero integers | [Rust 1.99 `NonZero` layout](https://doc.rust-lang.org/1.99.0/std/num/struct.NonZero.html#layout) preserves the underlying layout and validity except for the all-zero pattern. `filterMap` rejects zero as decoder failure; it never converts failure into an admitted optional payload. | +| `Option>` | The same `NonZero` layout contract gives ABI compatibility with the underlying integer. [Rust 1.99 `Option` representation](https://doc.rust-lang.org/1.99.0/std/option/index.html#representation) additionally guarantees the all-zero `None` representation and preserves valid `Some` payloads. The niche mapping decodes the full integer domain: zero becomes the Rust payload `None`, nonzero becomes `Some`; uninitialized storage still fails outer decoding. No generic `Option` layout is inferred. | +| `()` and `PhantomData` | [Rust 1.81 unit layout](https://doc.rust-lang.org/1.81.0/reference/type-layout.html#tuple-layout) has size zero. [Rust 1.99 `PhantomData` layout](https://doc.rust-lang.org/1.99.0/std/marker/struct.PhantomData.html#layout) guarantees size zero for every `T`; its public fieldless constructor stores no `T`. Each decoder supplies its explicit raw constructor, without fabricating a `T` or requiring `RustModel T`. | +| `[T; N]` | [Rust 1.81 array layout](https://doc.rust-lang.org/1.81.0/reference/type-layout.html#array-layout) gives total size `N * size_of::()` and element offset `k * size_of::()`. [Validity rules](https://doc.rust-lang.org/1.81.0/reference/behavior-considered-undefined.html#invalid-values) require valid elements. Consecutive complete element chunks cover all storage; padding within each chunk remains the element law's obligation. | +| Standard wrappers | [Rust 1.99 `Wrapping`](https://doc.rust-lang.org/1.99.0/std/num/struct.Wrapping.html#layout) preserves inner layout and ABI; its public single field stores `T`. [`ManuallyDrop`](https://doc.rust-lang.org/1.99.0/std/mem/struct.ManuallyDrop.html) preserves layout and bit validity. [`Cell`](https://doc.rust-lang.org/1.99.0/std/cell/struct.Cell.html#memory-layout) and [`UnsafeCell`](https://doc.rust-lang.org/1.99.0/std/cell/struct.UnsafeCell.html#memory-layout) preserve the inner in-memory representation. Map the actual inner decoder, including its failures; these premises do not certify interior mutation, aliasing, or destruction. | +| Local wrappers | Source `repr(transparent)` on `ReadOnly`/byteorder and `repr(C, packed)` on `Unalign`, with the [Rust 1.81 representation rules](https://doc.rust-lang.org/1.81.0/reference/type-layout.html#representations), justify retaining their complete field storage. `Unalign` removes outer alignment padding; it cannot remove padding within `T`. Byteorder's array and empty marker occupy all its storage. | + +The generic wrapper laws retain the original `?Sized` bounds. A physical +interpretation for a particular unsized value must retain the relevant metadata +and representation width in its supplied provider. These conditional laws do +not install a universal DST decoder or certify arbitrary slices, strings, or +trait objects. A missing child representation remains unavailable through its +wrapper; an available child decoder must carry its actual correspondence and +initialization premise. + +### Empty construction and external invariants + +Size zero does not imply that a value exists, that a Rust constructor may be +called, or that a library invariant holds. `emptyDecoder` requires an explicit +raw value; there is no blanket physical model inferred from size, a fieldless +extracted shape, or Lean `Inhabited`. A fieldless Rust token can carry a +constructor obligation about external state even when its physical bytes are +empty. That obligation needs an explicit state model or a retained caller +premise. A bit-valid raw constructor does not discharge it. + +[`EmptyConstructionTests.lean`](lean/EmptyConstructionTests.lean) checks an +uninhabited raw carrier with no representation model, an inhabited carrier +without one, and an explicit empty physical decoder with an external-state +condition in its library provider. Physical construction of the latter succeeds +in both states; full `decodeBytesResult` rejects the absent-state case as +`.fail .undef`. Both total and partial correctness reject that result even with +postcondition `True`. `PhantomData` succeeds using its actual empty +constructor, with no value or model of `Empty`. These are tests of modeled +admission, not executions of invalid Rust and not a proof of an external token's +safe constructor. + +The array theorem partitions storage by element count, requires an empty final +remainder, and derives initialization for every count from the element law. +The same rule handles empty arrays, zero-byte elements, and nested arrays. +Each marker requests its exact native impl independently of caller roots. +Both retained AST stages and the implementation-law audit preserve the full +trait, type/const parameters, carrier application, and dictionary bounds; +checked ordinary Lean witnesses cannot specialize or add premises. + +These laws establish modeled initialization conditional on correspondence. +They do not prove every `IntoBytes` method body, runtime storage transitions, +`as_bytes` pointer formation, aliasing, provenance, synchronization, destruction, +or general Rust UB-freedom. The typed-transfer and value-production boundaries +above continue to apply. ## Complete LLBC operation inventory diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 7974ad2e32..743f2fb2af 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -14,11 +14,47 @@ the inline Rust specifications against both the checked-in and live models. The required `All checks succeeded (ci.yml)` job depends on it. The settled design and deferred work are recorded in [DESIGN.md](DESIGN.md). -Application claims can use ordinary Rust assertion harnesses with total -`ensures _ => True` specifications. Successful termination requires every -assertion to pass. Review the independent calculation, complete comparisons, -and early returns together: returning early excludes that input from the -comparison. +For application review, start with the ordinary Rust reference calculations and +assertion harnesses in [`layout/nested_reference.rs`](../../zerocopy/src/layout/nested_reference.rs), +[`layout/tail_checks.rs`](../../zerocopy/src/layout/tail_checks.rs), +[`layout/composition_checks.rs`](../../zerocopy/src/layout/composition_checks.rs), +[`layout/tail_transform_checks.rs`](../../zerocopy/src/layout/tail_transform_checks.rs), +[`layout/primitive_checks.rs`](../../zerocopy/src/layout/primitive_checks.rs), and +[`util/checks.rs`](../../zerocopy/src/util/checks.rs). A total `ensures _ => True` +specification on a harness proves that it terminates without failing any of its +assertions for every admitted input. The assertions, comparisons, and early +returns are ordinary Rust, so the reviewer can assess the intended behavior and +its domain together. In particular, a guard that returns early excludes that +case from the comparison even though the harness itself still succeeds. + +Six concrete wrappers in [`lib.rs`](../../zerocopy/src/lib.rs) call the actual +`PointerMetadata` implementations for `()` and `usize`. Their contracts check +element-count conversion, layout-variant handling, and checked metadata sizing. +Using these results for an arbitrary `KnownLayout` implementation requires +separate layout correspondence. + +The numerical harness in [`split_at.rs`](../../zerocopy/src/split_at.rs) compares +split sizes with the independent remainder-based reference. It checks physical +tail containment and the zero-padding gate. The shared length helper also runs +in the production pointer path. These proofs establish bounds and disjoint byte +intervals, including empty and zero-sized tails; pointer validity and provenance +remain separate Rust obligations. + +The checks in [`pointer/mod.rs`](../../zerocopy/src/pointer/mod.rs) follow the +actual `CastUnsized` layout gate. Accepted DST pairs retain alignment, physical +tail offset, and complete sizes for every metadata count. Sized pairs need only +equal sizes, including zero-sized layouts with different alignments. Rejection +does not claim that a cast would be impossible. The proof covers the numerical +decision and sizing comparison, not the resulting pointer's validity. + +The checks in [`util/allocation.rs`](../../zerocopy/src/util/allocation.rs) cover +actual metadata sizing and exact preparation of allocator arguments. Preparation +preserves every optional size and the supplied alignment, without adding a +runtime validity filter. Under explicit correspondence to a valid recursive +layout, separate lemmas establish complete size and tail containment. Numerical +allocator admission additionally needs the outer alignment and the signed +metadata-size bound. Allocator behavior, zeroing, and `Box` validity remain +separate Rust obligations. These harnesses use the same annotation and proof rules as every other function. There is no root marker or separately maintained list of required functions. @@ -70,8 +106,10 @@ each tool answers a different question: from Charon declarations; Lean checks the complete compiled image against that roster. Local nominal types additionally need their exact source-bound model provider. Macro-generated dependency types can use a structural model - only when their inspected source span belongs to an item macro. Literal `invariant_proof` markers in macro input bind through native doc - origins; function specs and model declarations still require direct items. + only when their inspected source span belongs to an item macro. A literal + `invariant_proof` marker in macro input instead binds to its unique compiled + trait impl through the compiler's documentation origins. Macro input does + not support function specs or mathematical model declarations. 4. The `spec` command turns the inline requirements and postconditions into a transparent proposition in `Specs`. A handwritten Lean theorem proves that proposition. The command supplies input decoding and successful-result @@ -84,8 +122,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. @@ -156,14 +195,15 @@ postconditions could promise less. Passing proofs establish the written claims; they do not establish that those claims capture the intended behavior. The comments in these modules explain their inputs, outputs, and non-obvious -checks. This integration proves conditional functional +checks. [SEMANTICS.md](SEMANTICS.md) states the premise connecting the independent +layout mathematics to Rust. This integration proves conditional functional behavior; it does not prove that every caller meets the requirements or that zerocopy's unsafe pointer operations are sound. ## Unsafe boundaries and admission `external.json` lists exact reviewed Rust identities and signatures, with the -Lean interpretation used at each boundary. It derives the two local `--opaque` +Lean interpretation used at each boundary. It derives the local `--opaque` selections; arbitrary opaque flags are rejected. A changed local helper body requires a fresh review and an updated body digest. Registration is a trusted Rust-to-model premise, not a Lean proof of the omitted body. Standard-library @@ -179,8 +219,24 @@ The first storage examples are in entire destination unchanged when the source is too long. Its model returns the updated mutable slice explicitly. +The production `IntoBytes` write methods now call the proved +[`util/bytewrite`](../../zerocopy/src/util/bytewrite/mod.rs) helpers. Their +contracts cover exact, prefix, and suffix writes, preserved surrounding bytes, +and unchanged rejection. A concrete big-endian word consumer additionally +checks the public byteorder constructor/accessor composed with prefix writing. +Native tests compare that composition with `IntoBytes::write_to_prefix`; the +`as_bytes` pointer bridge remains the existing Rust safety argument. + +[`util/validity`](../../zerocopy/src/util/validity/mod.rs) supplies the Boolean and +nonzero-word predicates used by the actual scalar `TryFromBytes` implementations. +The checked conversions retain raw candidates until validation; pair and slice +contracts cover invalid bytes at every position. The exact byte-read bridge has +an execution-time bounds guard. These proofs establish conditional behavior for +initialized byte slices, without claiming the whole generic `Maybe` pointer path +has been lowered and verified. + The existing production `add_scaled_metadata` exercises guarded unchecked -addition and multiplication. Each of these four primitive definitions has an +addition and multiplication. The primitive definitions have an independent complete-definition check, including its forbidden branch. Kernel controls prove rejection even if an invalid result is discarded or followed by divergence. Extraction controls check actual generated callers that discard an @@ -207,38 +263,92 @@ whole-program unsafe-code certification. ## Scope and proofs Extraction starts from the function and nominal-type owners of every present -`aeneas` fence in `zerocopy/src`, including their dependencies. Every present -fence must have a supported Rust owner, exact extraction binding, and the -corresponding checked Lean declarations. Unannotated functions and impls can be -added without extending the specification set. +`aeneas` fence in `zerocopy/src`, including their dependencies. The current +function specifications cover the layout and arithmetic methods and their Rust +reference harnesses. Unannotated functions and impls can be added without +extending the specification set. Every present fence must have a supported Rust +owner, exact extraction binding, and the corresponding checked Lean declarations. -| Rust function | Checked property | +| Functions | 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. | -| `round_down_to_next_multiple_of_alignment` | For any positive power-of-two alignment, succeeds with a result no larger than the input and divisible by the alignment. | - -Every registered function uses total `spec`: accepted raw representations, -supplied mathematical ghosts, and explicit requirements imply successful -termination, successful output decoding, and the postconditions. These are -quantified conditional contracts, not finite test inputs. Broader ordinary Raw -lemmas retain useful representation-level domains. - -This initial arithmetic scope establishes extrema, padding bounds and an -aligned result no larger than the input. It does not claim least padding or -the greatest aligned predecessor. +| `max`, `min`, padding, round-down | Exact extrema, least padding, greatest aligned predecessor, and bounds. | +| Alignment/phase encoder and decoders | Power-of-two alignment, bounded phase, and exact encoding round-trip. | +| Trailing size, padding, capacity, and advancement | Independent unbounded size formulas, exact checked-size overflow, wrapping padding, and byte advancement. | +| Size-sequence comparison | A positive answer establishes equal sizes for every natural metadata value. | +| Zero-stride conversion and element capacity | Exact zero handling, preserved representation fields, and greatest fitting element count. | +| `DstLayout` constructors, extension, and padding | Exact fields, field placement, alignment, flags, and normalized size formulas. The record constructor terminates for arbitrary field lists satisfying the independent construction domain. | +| Static and dynamic padding queries | Exact flag result and the mathematical condition sufficient to eliminate dynamic padding for all metadata values. | +| Cast validation and exact-size metadata | Alignment/size error priority, greatest fitting metadata, exact prefix/suffix split, and rejection of unattainable sizes. | + +All registered specifications use total `spec`: accepted input representations +and their stated requirements imply successful termination, a valid returned +value, and their postconditions. Intentional panic for +casting a zero-stride DST is checked separately. The size-sequence comparison +is conservative: a negative result does not claim that the sequences differ. + +`LayoutMath.lean` defines an independent recursive layout semantics and proves +normalization correct for every nesting depth and metadata value. The extracted +contracts connect machine arithmetic and control flow to that mathematics. +`LayoutModel.lean` supplies shared interpretation predicates, without using +any function proof. `Corollaries.lean` connects checked sizes and physical +padding to the recursive semantics, proves that outer padding preserves +complete inner sizes, and connects the record constructor to direct +per-metadata field placement. +See [SEMANTICS.md](SEMANTICS.md) for the exact Rust premise and trust boundary. + +The nested Rust reference starts with `metadata * element_size`, then places +each complete inner record at a remainder-based aligned offset and rounds the +containing size. Its equivalence harness constructs the production layout and +compares the complete `Option` result, including overflow. It handles +arbitrary nesting, zero-size tails, and every machine-word metadata count. +The construction guards are visible in Rust: invalid descriptors, excessive +alignment, and static layouts that do not fit return before construction. +The tail harnesses additionally compare capacity, exact-size metadata, and both +successful cast splits and alignment/size errors. Their explicit witnesses let +reviewers read alignment and phase directly instead of decoding a stored word. +The original mathematical helper theorems retain their broader natural-number +domains; these Rust harnesses quantify the machine-word arguments Rust receives. +The composition harnesses compare extension, padding, and arbitrary field-list +construction, including every stored field and the shallow-padding flag. The +transformation harnesses compare byte advancement, wrapping padding, dynamic +padding queries, and checked sizes after a positive size-sequence answer. The +existing sequence theorem additionally preserves its unbounded size equality; +equality of checked optional sizes alone would lose differences after overflow. + +The inline checks in `layout/cast_from.rs` cover numerical cast composition. +They select a production `CastPlan`, require the checked metadata calculation +to succeed, compare it with the actual unchecked conversion, and compare +complete sizes using the independent remainder-based reference. Metadata +representability follows from a representable complete source size; it is not +an assumed harness precondition. The proof covers all three accepted plan +variants. Rejected plans carry no completeness promise, and the typed pointer +adapter's provenance and `KnownLayout` obligations remain outside this proof. + +The constructor's requirements check field alignment, the independent prefix +layout's overflow bounds, canonical encodings, and final padding bounds. These +are predicates over the mathematical construction, not assumptions that the +Rust constructor returned a correct result. Fragment operations have explicit +fit requirements; arbitrary malformed internal layout records need not succeed. +Generic size/alignment reads are explicit external data inputs, never axioms +asserting layout correctness. 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 -automatic input and output decoding. - -CI uses the default features, debug assertions and the runner's native target. -Local replay also supports macOS arm64. These conditional contracts do not -certify other extraction configurations, rustc, zerocopy's pointer safety or -whole-crate unsafe behavior. +and, for NonZero, positivity. They coerce to `Nat` or `Int` without unwrapping +raw fields. Binding `let N : Nat := n` makes addition and remainder ordinary +unbounded mathematics. Explicit `(raw)` clauses retain the extracted scalar +operations, whose checked arithmetic returns execution `Result` values. +Operation-specific power-of-two alignment and overflow bounds remain explicit +requirements. + +CI uses the default features, debug assertions, and the runner's native +`x86_64-unknown-linux-gnu` target. Local replay also supports macOS arm64. The +proofs cover all registered layout methods under their stated domains; +they do not certify other extraction configurations, a rustc implementation, +or zerocopy's pointer safety. The explicit Rust premise connects the recursive +semantics to an actual type's layout. Compiler regression tests challenge that +premise independently of the Lean algebra. Aeneas currently targets a safe Rust +subset; whole-crate unsafe verification is a separate task. The Rust tests also compare reconstruction with rustc directly at compile time. Concrete instantiations of ordinary, aligned, and packed `repr(C)` records @@ -536,7 +646,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 @@ -555,8 +665,10 @@ These are conditional contracts over accepted representations, supplied ghosts, and satisfied requirements. A decoder may intentionally forget observations or reject raw values. A ghost with type `False`, or a dependent ghost with an empty domain, makes the relevant contract vacuous. Neither the pipeline nor a decoder -proves that every Rust caller meets the domain. Operation-specific -alignment and fit conditions remain explicit. The independently written operation expectations check both intended input +proves that every Rust caller meets the domain. `DstLayout` initially keeps a +structural mathematical model, including its unpadded flag and decoded rounding +pair, without imposing a global realizable-layout requirement. Operation-specific +alignment, fit, and construction conditions remain explicit. The independently written operation expectations check both intended input admission and promised behavior. Representation laws can be useful proof helpers; they are not an additional universal model-certification requirement. @@ -565,7 +677,7 @@ Rust. Charon's root identity, exact source body, source path, and signature must match the annotation, including inherent Self types and inactive `cfg` alternatives. Discovery retains exact inspected source snapshots; later digest, binding, and assembly steps reject changes to any inspected input. The source -digest includes unannotated dependency files. Every +digest includes all inspected crate Rust sources and reserved-fence candidates. Every contents-bearing Charon-local file must agree with its inspected snapshot, so an unchanged caller cannot hide a changed dependency. Pinned external `/rustc` files without source contents remain within the translation premise. @@ -581,65 +693,96 @@ dictionary is absent from extraction still fails binding. Removing an annotation and its associated proof intentionally removes that claim from the checked set; the source and generated golden changes make the reduced coverage reviewable. There is no separately maintained function or type coverage roster. Nominal -types are still registered and audited independently from their specifications. - -Every present function annotation must match its exact extracted function. -Called functions and constants remain part of the complete dependency model. -Model -names, theorem identities, filenames, and dependency edges are derived rather -than stored as additional synchronized inventory fields. Discovery scans all -repository Rust sources except generated and vendored directories. A Rust -lexer distinguishes comments from strings and `syn` establishes ownership -before conditional compilation. +types used by extracted functions retain their exact source mapping and +structural model checks, including unannotated dependency types. + +Model names, theorem identities, filenames, and dependency edges are derived +from the present annotations and verified extraction. Discovery inspects all +`zerocopy/src` Rust sources and reserved-fence candidates elsewhere in the +repository, except generated and vendored directories. A Rust lexer distinguishes +comments from strings and `syn` establishes ownership before conditional +compilation. A present fence on an unsupported owner, including one hidden in a +macro, fails discovery; unannotated macros and impls keep their ordinary Rust +meaning. Every function extraction root must match a present function annotation. No parser can recognize every informal prose claim as a proof. The `aeneas` -fence is the reserved CI-checked convention. Near-miss guard detection and the -independent policy protect that convention without treating all mathematical -prose as annotations. +fence is the reserved CI-checked convention. Near-miss guard detection protects +that convention without treating all mathematical prose as annotations. CI +checks every present specification on both the golden and live models so an +owned fence cannot escape proof checking or the compiled binding and axiom audits. -## Array `IntoBytes` initialization law +## `IntoBytes` initialization laws The `IntoBytes` fence in [`lib.rs`](../../zerocopy/src/lib.rs) requires every accepted physical representation byte to be initialized. A byte in [`Rust.Storage`](../../anneal/lean/Rust/Storage.lean) is either initialized with -an eight-bit value or uninitialized. Each physical decoder has a fixed width; -a successful run must consume exactly that width. The law covers the entire -accepted byte list, including any padding within an element representation. - -This physical decoder is separate from `RustModel.decode`, which interprets a -typed value for library contracts. `RustModel.initializedRepresentation` -quantifies over every successful physical decoding, even when the library -model rejects that value. A missing physical decoder makes the law `False`. -The current physical models cover `bool`, `u8`, `()`, and arrays recursively -built from them; other mathematical models do not acquire a byte law by default. - -`arrayDecoder_initialized` proves that arrays inherit this law from their -element decoder for every element count. The decoder splits the representation -into consecutive chunks of the element width and requires an empty final -remainder. An empty array accepts only an empty byte list. Zero-sized elements -use empty chunks, so positive counts of `()` also have no representation bytes. -The concrete checks in -[`trait_checks.rs`](../../zerocopy/src/trait_checks.rs) exercise primitive, -empty, zero-sized, and nested arrays; the extracted generic implementation law -supplies the result for arbitrary counts under the element's law. - -Applying the theorem to Rust requires a correspondence premise for the physical -decoder. Its width must equal Rust's size, and it must admit every language-valid -representation. The [Rust Reference array layout rules](https://doc.rust-lang.org/reference/type-layout.html#array-layout) -give size `N * size_of::()`, alignment equal to `T`'s alignment, and element -`k` at byte offset `k * size_of::()`. These rules leave no padding between -complete element representations; padding already included in `size_of::()` -still needs the element's initialization law. The [validity rules](https://doc.rust-lang.org/reference/behavior-considered-undefined.html#invalid-values) -require valid array elements, restrict `bool` to zero and one, and require -initialized integers. The primitive layouts give `bool` and `u8` one byte and -`()` zero bytes. These language facts justify the current decoder choices; -Lean checks the initialization and array composition laws within that model. - -This proof establishes the array trait law under those correspondence premises. -The pure representation model does not track runtime storage, typed transfers, -or pointer provenance. `IntoBytes::as_bytes` retains its Rust safety argument; -its pointer implementation is not proved by this array law. See -[LOWERING_AUDIT.md](LOWERING_AUDIT.md) for the remaining lowering boundaries. +an eight-bit value or uninitialized. A physical decoder has a fixed width and +a successful run consumes exactly that width. `RustModel.initializedRepresentation` +requires an available physical decoder and initialization over its entire +accepted domain. Absence is `False`; rejection by the library's mathematical +`RustModel.decode` cannot reduce this domain. + +There are 59 authored implementation markers: `()`, `bool`, `char`; all twelve +signed/unsigned integer carriers; all twelve corresponding `NonZero` carriers +and their `Option` forms; `PhantomData`; arrays; `Wrapping`, `ManuallyDrop`, +`Cell`, `UnsafeCell`, `ReadOnly`, `Unalign`; and all twelve byteorder wrappers. +[The scope inventory](LOWERING_AUDIT.md#exact-authored-implementation-scope) +retains their exact generic bounds, configuration branches, and deferred impls. +The default library build selects the handwritten `Unalign` and byteorder +implementations; their derive/test alternatives remain deferred. Native floats, +slices, `str`, atomics, SIMD, and other derive-generated impls remain outside +this implementation-law scope. + +Integer physical decoders assemble initialized bytes in the extraction target's +little-endian order, then interpret signed words in two's complement. Admission +requires a little-endian 64-bit target, so pointer-sized words occupy eight +bytes. Nonzero decoders reject zero as decoder failure. The specialized +`Option>` decoder admits all initialized underlying integer patterns: +zero becomes the Rust payload `None`, nonzero becomes `Some`. Outer decoding +failure stays a failure. The character decoder rejects surrogates and values +above `0x10ffff`. No general optional-value or struct layout is inferred. + +Array decoding splits complete element representations into consecutive chunks +and requires an empty final remainder. `arrayDecoder_initialized` proves the +law for every count under the actual element decoder's law. Recursion counts +elements, so the same rule covers empty arrays, positive counts of zero-byte +elements, and nested arrays. Padding within an element remains the element +law's obligation. Wrapper decoders preserve the actual child's failures and +initialization law. Generic `?Sized` impl bounds are retained; a supplied +physical provider for an unsized value must also carry its applicable metadata +and representation width. These conditional laws supply no universal DST +representation model. + +The byteorder structs have transparent byte-array storage plus an empty +`PhantomData` field. In particular, `F32` and `F64` use `[u8; 4]` and `[u8; 8]`; +their initialization laws require no native floating-point representation model. +`PhantomData` uses its explicit empty raw constructor, without a stored `T` +or a model of `T`. This differs from inventing a value based on size zero or a +Lean `Inhabited` instance. Structural mathematical models receive no physical +decoder by default. + +[`EmptyConstructionTests.lean`](lean/EmptyConstructionTests.lean) checks that +empty-byte construction without a physical provider fails, including for an +uninhabited raw type. An explicit empty physical decoder can produce a +unit-like raw token, but its full provider rejects that token when the modeled +external-state condition is false. Total and partial correctness both reject +this `.fail .undef` result even with postcondition `True`. Empty storage proves +neither Rust constructor permission nor an external library invariant. + +Applying these Lean laws to Rust requires explicit correspondence: the +physical decoder has the correct width and admits exactly the applicable +language-valid representations with their corresponding raw values. The +[versioned language and standard-library premises](LOWERING_AUDIT.md#decoder-correspondence-premises) +record what each builtin interpretation consumes and their compatibility trust. +Initialization theorems alone cannot prove that correspondence: a decoder +rejecting all inputs also satisfies initialization vacuously. + +These are conditional initialization laws for the exact native trait dictionaries. +They do not prove every method body, runtime storage, typed transfers, aliasing, +pointer provenance, destruction, or general Rust UB-freedom. +`IntoBytes::as_bytes` retains its Rust safety argument; its pointer implementation +is outside these laws. See [LOWERING_AUDIT.md](LOWERING_AUDIT.md) for the remaining +lowering boundaries. ## Native Lean proofs and independent checks @@ -696,6 +839,16 @@ audit checks those identities and their generated-module ownership in both directions, independently scans raw nominal types, and rejects missing or extra provider registrations. This reuses one verified table without another coverage roster. +For cast validation and +exact-size metadata, the required outcomes spell out error priority, split +positions, exact size, and greatest-fitting metadata independently of the +predicates used by the inline specs. `OutcomeTests.lean` pins distinguishing +fixed-size, suffix-alignment, and padded-size plateau examples. +`LayoutModelDomainTests.lean` also establishes concrete admitted constructor +inputs and exact views for an ordinary record and a nested packed DST. These +bounded examples guard against vacuous preconditions; they do not establish +that every Rust type meets the construction domain. + `Check.lean` derives dependencies from elaborated theorem types and terms, following helpers across handwritten modules, including private helpers, and writes `proof-dependencies.json` in each proof workspace. It imports and audits all @@ -703,6 +856,12 @@ declarations from every handwritten Lean module, including unused auxiliary modules, together with the model, vocabulary, obligations, and generated specifications. Only `propext`, `Classical.choice`, and `Quot.sound` are permitted. +The explicit data-only Rust layout inputs documented in `SEMANTICS.md` +are also permitted. Models with generic alignment reads must provide both +data inputs with their exact signatures; the audit also checks that generic +size/alignment reads use those inputs and that `Usize` size uses the pointer +width. These checks pin the declared external interpretation; correspondence +to the actual Rust ABI remains an explicit premise. New axioms, `sorryAx`, and native evaluator proof axioms fail. Callers reuse ordinary exported theorems, either explicitly with `step with` or @@ -720,14 +879,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 @@ -833,7 +995,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 @@ -854,6 +1016,48 @@ its generated proposition. Edit its proof directly in Lean. No proof copying back to Rust is required. This development cache is for iteration; CI always regenerates specifications and builds both models in fresh isolated projects. +## Mathematical views and indexed loops + +### Arithmetic, mathematical views, and indexed loops + +Checked addition, subtraction, and multiplication already have upstream +`step_pure` specifications. Use `step as ⟨result, facts⟩` and split the `Option` +result to obtain both the exact successful value and the overflow condition. +`SupportTests.lean` exercises all inputs, including overflow. Layout proofs use +these registrations directly, without naming bitvector specification lemmas. + +A contract may express equality through a pure mathematical view: + +```lean +theorem operation_spec (input : Input) (h : valid input) : + operation input ⦃ result => + view result = mathematicalOperation (view input) ∧ canonical result ⦄ := by + ... +``` + +This ordinary theorem states the existing total WP postcondition directly. +A view-only theorem states just the view equality. Partial correctness uses +`⦄div` in place of `⦄`: it explicitly permits divergence and still excludes +failure. These are Aeneas's existing specification operators. Use `WP.spec_mono` +to adapt an existing result specification to a view, and register useful caller +specifications with `attribute [step] operation_spec`. The existing Aeneas +registry then lets callers use `step` without specifying the theorem manually. + +`AeneasContracts.indexed_loop_spec` specializes Aeneas's `loop.spec_decr_nat` +to a state and `Usize` index. Supply a view, the mathematical value of each +prefix, and a representation invariant. Each continuing body step must advance +the index by +exactly one and establish the next prefix; a completed step must be at the +length. The adapter supplies bounds and the decreasing `length - index` +termination measure. The record constructor instantiates this rule; its body +proof still establishes the arithmetic bounds needed to avoid Rust overflow. +`SupportTests.lean` contains a smaller independent example. + +The specification syntax, examples, and required-contract proof terms +participate in the axiom audit. Failure controls challenge an incorrect view, +divergence under a total view contract, a stationary loop index, an incorrect +prefix step, and continuing past the loop bound. + ## Updating models and fuzzy comparison `golden/` stores all four complete generated Aeneas modules, including types, @@ -887,7 +1091,7 @@ additional generated files, changes to external-template signatures, and code changes fail with a normalized diff and require regeneration. CI compiles the checked-in model and the unmodified live model in separate fresh -Lake workspaces. Both must prove all inline specifications and any checked-in composition +Lake workspaces. Both must prove all inline specifications and composition corollaries and pass required checks and the complete axiom audit. The normalized text is used only for comparison, never compilation. This independently checks that accepted differences preserve the proved properties; it does not by itself @@ -936,6 +1140,28 @@ records but does not formally prove: Rust values by admitting zero; the generated conditional contracts assume successful recursive decoding of inputs and prove it for returned values. This introduces no axiom asserting that every modeled wrapper is nonzero. +- The guarded `NonZeroUsize::new_unchecked` interpretation returns its input + in the raw wrapper only when that input is nonzero. Zero and unsupported + native types produce forbidden execution (`fail undef`), including when the + result is ignored. Admission checks the original Rust `usize` instantiation + and its lifted `NonZeroUsizeInner` argument; the compiled audit compares the + whole definition independently of successful-input proofs. The pinned std + contract (`core/src/num/nonzero.rs`, nightly-2026-09-17, lines 394–399) says + that zero causes undefined behavior and requires a nonzero argument. Its + Rust-to-model correspondence remains a primitive boundary premise. The + `divide_by_unaligned` body stays extracted: the exact dictionary's law proves + alignment one, hence `1 / alignment = 1`, establishing constructor safety + before the final checked division. The concrete `u8` caller discharges its + implementation law. These proofs concern values and arithmetic, not memory. +- The external `usize::unchecked_mul` and `usize::unchecked_add` models + return the exact product and sum on non-overflowing inputs. Their Lean + definitions use checked arithmetic, and every use proves both results fit. + They claim no Rust behavior outside that domain. The cast composition + harness derives these bounds from successful plan selection and a + representable source size, and compares complete source/destination sizes + using the independent remainder-based reference. Pointer provenance, + reference validity, and `KnownLayout` implementations remain outside this + numerical proof. - Lean's kernel, its standard logic axioms, and the imported proof artifacts check the encoded propositions correctly. Release checksums establish artifact identity, not a proof of compiler or model correctness. diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean index ba39e32eb6..7b27a3e9a1 100644 --- a/verification/aeneas/golden/Funs.lean +++ b/verification/aeneas/golden/Funs.lean @@ -411,14 +411,14 @@ def byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder : } /-- [zerocopy::byteorder::{zerocopy::byteorder::U16}::from_bytes]: - Source: 'src/byteorder.rs', lines 570:12-572:13 + Source: 'src/byteorder.rs', lines 569:12-571: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 + Source: 'src/byteorder.rs', lines 569:12-571:13 Visibility: public -/ def byteorder.U32.from_bytes (O : Type) (bytes : Array Std.U8 4#usize) : Result (byteorder.U32 O) := do @@ -441,7 +441,7 @@ def byteorder.U16.new ok { _0 := bytes, _1 := core.marker.PhantomData.mk } /-- [zerocopy::byteorder::{zerocopy::byteorder::U16}::set]: - Source: 'src/byteorder.rs', lines 619:12-621:13 + Source: 'src/byteorder.rs', lines 618:12-620:13 Visibility: public -/ def byteorder.U16.set {O : Type} (ByteOrderInst : byteorder.ByteOrder O) (self : byteorder.U16 O) @@ -467,7 +467,7 @@ def byteorder.U32.new ok { _0 := bytes, _1 := core.marker.PhantomData.mk } /-- [zerocopy::byteorder::{zerocopy::byteorder::U32}::set]: - Source: 'src/byteorder.rs', lines 619:12-621:13 + Source: 'src/byteorder.rs', lines 618:12-620:13 Visibility: public -/ def byteorder.U32.set {O : Type} (ByteOrderInst : byteorder.ByteOrder O) (self : byteorder.U32 O) @@ -477,7 +477,7 @@ def byteorder.U32.set byteorder.U32.new ByteOrderInst n /-- [zerocopy::byteorder::{impl core::convert::From> for [u8; 2usize]}::from]: - Source: 'src/byteorder.rs', lines 631:12-633:13 + Source: 'src/byteorder.rs', lines 630:12-632:13 Visibility: public -/ def ArrayU82.Insts.CoreConvertFromU16.from {O : Type} (ByteOrderInst : byteorder.ByteOrder O) (x : byteorder.U16 O) : @@ -486,7 +486,7 @@ def ArrayU82.Insts.CoreConvertFromU16.from ok x._0 /-- Trait implementation: [zerocopy::byteorder::{impl core::convert::From> for [u8; 2usize]}] - Source: 'src/byteorder.rs', lines 629:8-634:9 -/ + Source: 'src/byteorder.rs', lines 628:8-633:9 -/ @[reducible] def ArrayU82.Insts.CoreConvertFromU16 {O : Type} (ByteOrderInst : byteorder.ByteOrder O) : core.convert.From (Array Std.U8 2#usize) @@ -495,7 +495,7 @@ def ArrayU82.Insts.CoreConvertFromU16 {O : Type} (ByteOrderInst : } /-- [zerocopy::byteorder::{impl core::convert::From> for [u8; 4usize]}::from]: - Source: 'src/byteorder.rs', lines 631:12-633:13 + Source: 'src/byteorder.rs', lines 630:12-632:13 Visibility: public -/ def ArrayU84.Insts.CoreConvertFromU32.from {O : Type} (ByteOrderInst : byteorder.ByteOrder O) (x : byteorder.U32 O) : @@ -504,7 +504,7 @@ def ArrayU84.Insts.CoreConvertFromU32.from ok x._0 /-- Trait implementation: [zerocopy::byteorder::{impl core::convert::From> for [u8; 4usize]}] - Source: 'src/byteorder.rs', lines 629:8-634:9 -/ + Source: 'src/byteorder.rs', lines 628:8-633:9 -/ @[reducible] def ArrayU84.Insts.CoreConvertFromU32 {O : Type} (ByteOrderInst : byteorder.ByteOrder O) : core.convert.From (Array Std.U8 4#usize) @@ -525,14 +525,14 @@ def byteorder.U16.get | 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 -/ + Source: 'src/byteorder.rs', lines 1724:4-1726: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 -/ + Source: 'src/byteorder.rs', lines 1735:4-1737:5 -/ def byteorder.verification.write_u16_le (n : Std.U16) : Result (Array Std.U8 2#usize) := do let u ← @@ -541,7 +541,7 @@ def byteorder.verification.write_u16_le byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder) u /-- [zerocopy::byteorder::verification::set_u16_le]: - Source: 'src/byteorder.rs', lines 1664:4-1668:5 -/ + Source: 'src/byteorder.rs', lines 1745:4-1749: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 @@ -552,14 +552,14 @@ def byteorder.verification.set_u16_le value1 /-- [zerocopy::byteorder::verification::read_u16_be]: - Source: 'src/byteorder.rs', lines 1677:4-1679:5 -/ + Source: 'src/byteorder.rs', lines 1758:4-1760: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 -/ + Source: 'src/byteorder.rs', lines 1769:4-1771:5 -/ def byteorder.verification.write_u16_be (n : Std.U16) : Result (Array Std.U8 2#usize) := do let u ← @@ -568,7 +568,7 @@ def byteorder.verification.write_u16_be byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder) u /-- [zerocopy::byteorder::verification::set_u16_be]: - Source: 'src/byteorder.rs', lines 1698:4-1702:5 -/ + Source: 'src/byteorder.rs', lines 1779:4-1783: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 @@ -590,14 +590,14 @@ def byteorder.U32.get | 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 -/ + Source: 'src/byteorder.rs', lines 1792:4-1794: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 -/ + Source: 'src/byteorder.rs', lines 1803:4-1805:5 -/ def byteorder.verification.write_u32_le (n : Std.U32) : Result (Array Std.U8 4#usize) := do let u ← @@ -606,7 +606,7 @@ def byteorder.verification.write_u32_le byteorder.LittleEndian.Insts.ZerocopyByteorderByteOrder) u /-- [zerocopy::byteorder::verification::set_u32_le]: - Source: 'src/byteorder.rs', lines 1732:4-1736:5 -/ + Source: 'src/byteorder.rs', lines 1813:4-1817: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 @@ -617,14 +617,14 @@ def byteorder.verification.set_u32_le value1 /-- [zerocopy::byteorder::verification::read_u32_be]: - Source: 'src/byteorder.rs', lines 1745:4-1747:5 -/ + Source: 'src/byteorder.rs', lines 1826:4-1828: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 -/ + Source: 'src/byteorder.rs', lines 1837:4-1839:5 -/ def byteorder.verification.write_u32_be (n : Std.U32) : Result (Array Std.U8 4#usize) := do let u ← @@ -633,7 +633,7 @@ def byteorder.verification.write_u32_be byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder) u /-- [zerocopy::byteorder::verification::set_u32_be]: - Source: 'src/byteorder.rs', lines 1766:4-1770:5 -/ + Source: 'src/byteorder.rs', lines 1847:4-1851: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 @@ -1405,6 +1405,222 @@ def core.option.OptionNonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes : core.option.OptionNonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait } +/-- [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::U16}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + byteorder.U16.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + (O : Type) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::U16}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def byteorder.U16.Insts.ZerocopyIntoBytes (O : Type) : IntoBytes (byteorder.U16 + O) := { + only_derive_is_allowed_to_implement_this_trait := + byteorder.U16.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + O +} + +/-- [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::U32}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + byteorder.U32.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + (O : Type) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::U32}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def byteorder.U32.Insts.ZerocopyIntoBytes (O : Type) : IntoBytes (byteorder.U32 + O) := { + only_derive_is_allowed_to_implement_this_trait := + byteorder.U32.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + O +} + +/-- [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::U64}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + byteorder.U64.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + (O : Type) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::U64}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def byteorder.U64.Insts.ZerocopyIntoBytes (O : Type) : IntoBytes (byteorder.U64 + O) := { + only_derive_is_allowed_to_implement_this_trait := + byteorder.U64.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + O +} + +/-- [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::U128}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + byteorder.U128.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + (O : Type) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::U128}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def byteorder.U128.Insts.ZerocopyIntoBytes (O : Type) : IntoBytes + (byteorder.U128 O) := { + only_derive_is_allowed_to_implement_this_trait := + byteorder.U128.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + O +} + +/-- [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::Usize}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + byteorder.Usize.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + (O : Type) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::Usize}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def byteorder.Usize.Insts.ZerocopyIntoBytes (O : Type) : IntoBytes + (byteorder.Usize O) := { + only_derive_is_allowed_to_implement_this_trait := + byteorder.Usize.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + O +} + +/-- [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::I16}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + byteorder.I16.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + (O : Type) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::I16}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def byteorder.I16.Insts.ZerocopyIntoBytes (O : Type) : IntoBytes (byteorder.I16 + O) := { + only_derive_is_allowed_to_implement_this_trait := + byteorder.I16.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + O +} + +/-- [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::I32}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + byteorder.I32.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + (O : Type) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::I32}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def byteorder.I32.Insts.ZerocopyIntoBytes (O : Type) : IntoBytes (byteorder.I32 + O) := { + only_derive_is_allowed_to_implement_this_trait := + byteorder.I32.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + O +} + +/-- [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::I64}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + byteorder.I64.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + (O : Type) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::I64}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def byteorder.I64.Insts.ZerocopyIntoBytes (O : Type) : IntoBytes (byteorder.I64 + O) := { + only_derive_is_allowed_to_implement_this_trait := + byteorder.I64.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + O +} + +/-- [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::I128}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + byteorder.I128.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + (O : Type) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::I128}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def byteorder.I128.Insts.ZerocopyIntoBytes (O : Type) : IntoBytes + (byteorder.I128 O) := { + only_derive_is_allowed_to_implement_this_trait := + byteorder.I128.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + O +} + +/-- [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::Isize}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + byteorder.Isize.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + (O : Type) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::Isize}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def byteorder.Isize.Insts.ZerocopyIntoBytes (O : Type) : IntoBytes + (byteorder.Isize O) := { + only_derive_is_allowed_to_implement_this_trait := + byteorder.Isize.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + O +} + +/-- [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::F32}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + byteorder.F32.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + (O : Type) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::F32}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def byteorder.F32.Insts.ZerocopyIntoBytes (O : Type) : IntoBytes (byteorder.F32 + O) := { + only_derive_is_allowed_to_implement_this_trait := + byteorder.F32.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + O +} + +/-- [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::F64}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + byteorder.F64.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + (O : Type) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::byteorder::_::{impl zerocopy::IntoBytes for zerocopy::byteorder::F64}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def byteorder.F64.Insts.ZerocopyIntoBytes (O : Type) : IntoBytes (byteorder.F64 + O) := { + only_derive_is_allowed_to_implement_this_trait := + byteorder.F64.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + O +} + /-- [zerocopy::impls::_#12::{impl zerocopy::IntoBytes for core::marker::PhantomData}::only_derive_is_allowed_to_implement_this_trait]: Source: 'src/util/macros.rs', lines 165:8-165:62 Visibility: public -/ @@ -1423,6 +1639,116 @@ def core.marker.PhantomData.Insts.ZerocopyIntoBytes (T : Type) : IntoBytes T } +/-- [zerocopy::wrappers::_::{impl zerocopy::IntoBytes for zerocopy::wrappers::Unalign}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + wrappers.Unalign.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + {T : Type} (IntoBytesInst : IntoBytes T) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::wrappers::_::{impl zerocopy::IntoBytes for zerocopy::wrappers::Unalign}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def wrappers.Unalign.Insts.ZerocopyIntoBytes {T : Type} (IntoBytesInst : + IntoBytes T) : IntoBytes (wrappers.Unalign T) := { + only_derive_is_allowed_to_implement_this_trait := + wrappers.Unalign.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + IntoBytesInst +} + +/-- [zerocopy::wrappers::_#2::{impl zerocopy::IntoBytes for zerocopy::wrappers::read_only_def::ReadOnly}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 165:8-165:62 + Visibility: public -/ +def + wrappers.read_only_def.ReadOnly.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + {T : Type} (IntoBytesInst : IntoBytes T) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::wrappers::_#2::{impl zerocopy::IntoBytes for zerocopy::wrappers::read_only_def::ReadOnly}] + Source: 'src/util/macros.rs', lines 132:8-134:9 -/ +@[reducible] +def wrappers.read_only_def.ReadOnly.Insts.ZerocopyIntoBytes {T : Type} + (IntoBytesInst : IntoBytes T) : IntoBytes (wrappers.read_only_def.ReadOnly T) + := { + only_derive_is_allowed_to_implement_this_trait := + wrappers.read_only_def.ReadOnly.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + IntoBytesInst +} + +/-- [zerocopy::impls::_#31::{impl zerocopy::IntoBytes for core::num::wrapping::Wrapping}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 204:16-221:17 + Visibility: public -/ +def + core.num.wrapping.Wrapping.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + {T : Type} (IntoBytesInst : IntoBytes T) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#31::{impl zerocopy::IntoBytes for core::num::wrapping::Wrapping}] + Source: 'src/util/macros.rs', lines 201:12-228:13 -/ +@[reducible] +def core.num.wrapping.Wrapping.Insts.ZerocopyIntoBytes {T : Type} + (IntoBytesInst : IntoBytes T) : IntoBytes (core.num.wrapping.Wrapping T) := { + only_derive_is_allowed_to_implement_this_trait := + core.num.wrapping.Wrapping.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + IntoBytesInst +} + +/-- [zerocopy::impls::_#35::{impl zerocopy::IntoBytes for core::mem::manually_drop::ManuallyDrop}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 204:16-221:17 + Visibility: public -/ +def + core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + {T : Type} (IntoBytesInst : IntoBytes T) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#35::{impl zerocopy::IntoBytes for core::mem::manually_drop::ManuallyDrop}] + Source: 'src/util/macros.rs', lines 201:12-228:13 -/ +@[reducible] +def core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes {T : Type} + (IntoBytesInst : IntoBytes T) : IntoBytes + (core.mem.manually_drop.ManuallyDrop T) := { + only_derive_is_allowed_to_implement_this_trait := + core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + IntoBytesInst +} + +/-- [zerocopy::impls::_#39::{impl zerocopy::IntoBytes for core::cell::Cell}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 204:16-221:17 + Visibility: public -/ +def + core.cell.Cell.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + {T : Type} (IntoBytesInst : IntoBytes T) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#39::{impl zerocopy::IntoBytes for core::cell::Cell}] + Source: 'src/util/macros.rs', lines 201:12-228:13 -/ +@[reducible] +def core.cell.Cell.Insts.ZerocopyIntoBytes {T : Type} (IntoBytesInst : + IntoBytes T) : IntoBytes (core.cell.Cell T) := { + only_derive_is_allowed_to_implement_this_trait := + core.cell.Cell.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + IntoBytesInst +} + +/-- [zerocopy::impls::_#42::{impl zerocopy::IntoBytes for core::cell::UnsafeCell}::only_derive_is_allowed_to_implement_this_trait]: + Source: 'src/util/macros.rs', lines 204:16-221:17 + Visibility: public -/ +def + core.cell.UnsafeCell.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + {T : Type} (IntoBytesInst : IntoBytes T) : Result Unit := do + ok () + +/-- Trait implementation: [zerocopy::impls::_#42::{impl zerocopy::IntoBytes for core::cell::UnsafeCell}] + Source: 'src/util/macros.rs', lines 201:12-228:13 -/ +@[reducible] +def core.cell.UnsafeCell.Insts.ZerocopyIntoBytes {T : Type} (IntoBytesInst : + IntoBytes T) : IntoBytes (core.cell.UnsafeCell T) := { + only_derive_is_allowed_to_implement_this_trait := + core.cell.UnsafeCell.Insts.ZerocopyIntoBytes.only_derive_is_allowed_to_implement_this_trait + IntoBytesInst +} + /-- [zerocopy::util::padding_needed_for]: Source: 'src/util/mod.rs', lines 166:0-226:1 -/ def util.padding_needed_for diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean index 464a829fb8..d91799ec1f 100644 --- a/verification/aeneas/golden/Types.lean +++ b/verification/aeneas/golden/Types.lean @@ -46,6 +46,14 @@ structure core.num.nonzero.ZeroablePrimitive (Self : Type) (Self_NonZeroInner : markerCopyInst : core.marker.Copy Self innerCopyInst : core.marker.Copy Self_NonZeroInner +/-- [core::num::wrapping::Wrapping] + Source: '/rustc/library/core/src/num/wrapping.rs', lines 43:0-43:22 + Name pattern: [core::num::wrapping::Wrapping] + Visibility: public -/ +@[rust_type "core::num::wrapping::Wrapping"] +structure core.num.wrapping.Wrapping (T : Type) where + _0 : T + /-- [zerocopy::byteorder::Order] Source: 'src/byteorder.rs', lines 103:0-108:1 Visibility: public -/ @@ -99,6 +107,76 @@ structure byteorder.U32 (O : Type) where _0 : Array Std.U8 4#usize _1 : core.marker.PhantomData O +/-- [zerocopy::byteorder::U64] + Source: 'src/byteorder.rs', lines 528:12-528:62 + Visibility: public -/ +structure byteorder.U64 (O : Type) where + _0 : Array Std.U8 8#usize + _1 : core.marker.PhantomData O + +/-- [zerocopy::byteorder::U128] + Source: 'src/byteorder.rs', lines 528:12-528:62 + Visibility: public -/ +structure byteorder.U128 (O : Type) where + _0 : Array Std.U8 16#usize + _1 : core.marker.PhantomData O + +/-- [zerocopy::byteorder::Usize] + Source: 'src/byteorder.rs', lines 528:12-528:62 + Visibility: public -/ +structure byteorder.Usize (O : Type) where + _0 : Array Std.U8 8#usize + _1 : core.marker.PhantomData O + +/-- [zerocopy::byteorder::I16] + Source: 'src/byteorder.rs', lines 528:12-528:62 + Visibility: public -/ +structure byteorder.I16 (O : Type) where + _0 : Array Std.U8 2#usize + _1 : core.marker.PhantomData O + +/-- [zerocopy::byteorder::I32] + Source: 'src/byteorder.rs', lines 528:12-528:62 + Visibility: public -/ +structure byteorder.I32 (O : Type) where + _0 : Array Std.U8 4#usize + _1 : core.marker.PhantomData O + +/-- [zerocopy::byteorder::I64] + Source: 'src/byteorder.rs', lines 528:12-528:62 + Visibility: public -/ +structure byteorder.I64 (O : Type) where + _0 : Array Std.U8 8#usize + _1 : core.marker.PhantomData O + +/-- [zerocopy::byteorder::I128] + Source: 'src/byteorder.rs', lines 528:12-528:62 + Visibility: public -/ +structure byteorder.I128 (O : Type) where + _0 : Array Std.U8 16#usize + _1 : core.marker.PhantomData O + +/-- [zerocopy::byteorder::Isize] + Source: 'src/byteorder.rs', lines 528:12-528:62 + Visibility: public -/ +structure byteorder.Isize (O : Type) where + _0 : Array Std.U8 8#usize + _1 : core.marker.PhantomData O + +/-- [zerocopy::byteorder::F32] + Source: 'src/byteorder.rs', lines 528:12-528:62 + Visibility: public -/ +structure byteorder.F32 (O : Type) where + _0 : Array Std.U8 4#usize + _1 : core.marker.PhantomData O + +/-- [zerocopy::byteorder::F64] + Source: 'src/byteorder.rs', lines 528:12-528:62 + Visibility: public -/ +structure byteorder.F64 (O : Type) where + _0 : Array Std.U8 8#usize + _1 : core.marker.PhantomData O + /-- Trait declaration: [zerocopy::IntoBytes] Source: 'src/lib.rs', lines 5941:0-6446:1 Visibility: public -/ @@ -120,4 +198,16 @@ structure trait_checks.XorCodec where structure trait_checks.Forward (C : Type) where _0 : core.marker.PhantomData C +/-- [zerocopy::wrappers::Unalign] + Source: 'src/wrappers.rs', lines 118:0-118:25 + Visibility: public -/ +structure wrappers.Unalign (T : Type) where + _0 : T + +/-- [zerocopy::wrappers::read_only_def::ReadOnly] + Source: 'src/wrappers.rs', lines 630:4-634:5 + Visibility: public -/ +structure wrappers.read_only_def.ReadOnly (T : Type) where + inner : T + end Zerocopy diff --git a/verification/aeneas/golden/TypesExternal_Template.lean b/verification/aeneas/golden/TypesExternal_Template.lean index 7e0a757dc9..da94ce8f16 100644 --- a/verification/aeneas/golden/TypesExternal_Template.lean +++ b/verification/aeneas/golden/TypesExternal_Template.lean @@ -26,6 +26,27 @@ set_option maxHeartbeats 1000000 /- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/ set_option maxRecDepth 2048 +/-- [core::cell::Cell] + Source: '/rustc/library/core/src/cell.rs', lines 315:0-315:26 + Name pattern: [core::cell::Cell] + Visibility: public -/ +@[rust_type "core::cell::Cell"] +axiom core.cell.Cell (T : Type) : Type + +/-- [core::cell::UnsafeCell] + Source: '/rustc/library/core/src/cell.rs', lines 2311:0-2311:32 + Name pattern: [core::cell::UnsafeCell] + Visibility: public -/ +@[rust_type "core::cell::UnsafeCell"] +axiom core.cell.UnsafeCell (T : Type) : Type + +/-- [core::mem::manually_drop::ManuallyDrop] + Source: '/rustc/library/core/src/mem/manually_drop.rs', lines 156:0-156:34 + Name pattern: [core::mem::manually_drop::ManuallyDrop] + Visibility: public -/ +@[rust_type "core::mem::manually_drop::ManuallyDrop"] +axiom core.mem.manually_drop.ManuallyDrop (T : Type) : Type + /-- [core::num::niche_types::NonZeroUsizeInner] Source: '/rustc/library/core/src/num/niche_types.rs', lines 20:8-20:55 Name pattern: [core::num::niche_types::NonZeroUsizeInner] diff --git a/verification/aeneas/lean/DeriveModels.lean b/verification/aeneas/lean/DeriveModels.lean index d245ad4202..0e852ef2e4 100644 --- a/verification/aeneas/lean/DeriveModels.lean +++ b/verification/aeneas/lean/DeriveModels.lean @@ -112,7 +112,8 @@ meta partial def boundModelProvider (raw : Expr) (params dicts : Array Expr) : M return ← app ``modelPhantomData args for (carrier, provider) in #[ (``core.mem.manually_drop.ManuallyDrop, ``modelManuallyDrop), - (``core.cell.Cell, ``modelCell), (``core.cell.UnsafeCell, ``modelUnsafeCell)] do + (``core.cell.Cell, ``modelCell), (``core.cell.UnsafeCell, ``modelUnsafeCell), + (``Zerocopy.core.num.wrapping.Wrapping, ``modelWrapping)] do if head.isConstOf carrier then let child ← boundModelProvider args[0]! params dicts return ← app provider (args ++ #[child]) diff --git a/verification/aeneas/lean/ModelPrelude.lean b/verification/aeneas/lean/ModelPrelude.lean index b8c02429de..065d4305ce 100644 --- a/verification/aeneas/lean/ModelPrelude.lean +++ b/verification/aeneas/lean/ModelPrelude.lean @@ -78,6 +78,12 @@ theorem initializedWrapperRepresentation {A B : Type} [ma : RustModel A] decode raw := ma.decode raw.value representation := wrapperRepresentation core.cell.UnsafeCell.mk +@[reducible] instance modelWrapping (T : Type) [ma : RustModel T] : + RustModel (Zerocopy.core.num.wrapping.Wrapping T) where + Model := ma.Model + decode raw := ma.decode raw._0 + representation := wrapperRepresentation Zerocopy.core.num.wrapping.Wrapping.mk + theorem initializedManuallyDrop (T : Type) [ma : RustModel T] (child : RustModel.initializedRepresentation T) : RustModel.initializedRepresentation (core.mem.manually_drop.ManuallyDrop T) := @@ -93,6 +99,11 @@ theorem initializedUnsafeCell (T : Type) [ma : RustModel T] RustModel.initializedRepresentation (core.cell.UnsafeCell T) := initializedWrapperRepresentation core.cell.UnsafeCell.mk child +theorem initializedWrapping (T : Type) [ma : RustModel T] + (child : RustModel.initializedRepresentation T) : + RustModel.initializedRepresentation (Zerocopy.core.num.wrapping.Wrapping T) := + initializedWrapperRepresentation Zerocopy.core.num.wrapping.Wrapping.mk child + -- 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/Proofs/IntoBytes.lean b/verification/aeneas/lean/Proofs/IntoBytes.lean index 393b327069..7cc9f8408f 100644 --- a/verification/aeneas/lean/Proofs/IntoBytes.lean +++ b/verification/aeneas/lean/Proofs/IntoBytes.lean @@ -206,4 +206,155 @@ namespace Zerocopy.Proofs (Zerocopy.core.marker.PhantomData.Insts.ZerocopyIntoBytes T) := ⟨Rust.Storage.emptyDecoder_initialized _⟩ + +-- Transparent wrappers inherit the exact incoming dictionary promise. +-- The proof never assumes the output implementation's own invariant. + +@[instance] theorem core.num.wrapping.Wrapping.Insts.ZerocopyIntoBytes_law + {T : Type} (dictionary : IntoBytes T) + [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] : + TraitLaws.into_bytes_initialized (Zerocopy.core.num.wrapping.Wrapping T) + (Zerocopy.core.num.wrapping.Wrapping.Insts.ZerocopyIntoBytes dictionary) := + ⟨initializedWrapping T + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩ + +@[instance] theorem core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes_law + {T : Type} (dictionary : IntoBytes T) + [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] : + TraitLaws.into_bytes_initialized (core.mem.manually_drop.ManuallyDrop T) + (Zerocopy.core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes dictionary) := + ⟨initializedManuallyDrop T + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩ + +@[instance] theorem core.cell.Cell.Insts.ZerocopyIntoBytes_law + {T : Type} (dictionary : IntoBytes T) + [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] : + TraitLaws.into_bytes_initialized (core.cell.Cell T) + (Zerocopy.core.cell.Cell.Insts.ZerocopyIntoBytes dictionary) := + ⟨initializedCell T + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩ + +@[instance] theorem core.cell.UnsafeCell.Insts.ZerocopyIntoBytes_law + {T : Type} (dictionary : IntoBytes T) + [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] : + TraitLaws.into_bytes_initialized (core.cell.UnsafeCell T) + (Zerocopy.core.cell.UnsafeCell.Insts.ZerocopyIntoBytes dictionary) := + ⟨initializedUnsafeCell T + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩ + +@[instance] theorem wrappers.Unalign.Insts.ZerocopyIntoBytes_law + {T : Type} (dictionary : IntoBytes T) + [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] : + TraitLaws.into_bytes_initialized (Zerocopy.wrappers.Unalign T) + (Zerocopy.wrappers.Unalign.Insts.ZerocopyIntoBytes dictionary) := + ⟨initializedWrapperRepresentation Zerocopy.wrappers.Unalign.mk + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩ + +@[instance] theorem wrappers.read_only_def.ReadOnly.Insts.ZerocopyIntoBytes_law + {T : Type} (dictionary : IntoBytes T) + [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] : + TraitLaws.into_bytes_initialized (Zerocopy.wrappers.read_only_def.ReadOnly T) + (Zerocopy.wrappers.read_only_def.ReadOnly.Insts.ZerocopyIntoBytes dictionary) := + ⟨initializedWrapperRepresentation Zerocopy.wrappers.read_only_def.ReadOnly.mk + (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩ + +-- The byte-order parameter is phantom. Only the byte array contributes +-- storage, and its elements inherit the u8 initialization theorem. + +@[instance] theorem byteorder.U16.Insts.ZerocopyIntoBytes_law + (O : Type) [meaning : RustModel O] : + TraitLaws.into_bytes_initialized (Zerocopy.byteorder.U16 O) + (Zerocopy.byteorder.U16.Insts.ZerocopyIntoBytes O) := + ⟨initializedWrapperRepresentation + (fun raw => Zerocopy.byteorder.U16.mk raw Zerocopy.core.marker.PhantomData.mk) + (RustModel.initialized_array U8 (2#usize) (initializedUScalar .U8))⟩ + +@[instance] theorem byteorder.U32.Insts.ZerocopyIntoBytes_law + (O : Type) [meaning : RustModel O] : + TraitLaws.into_bytes_initialized (Zerocopy.byteorder.U32 O) + (Zerocopy.byteorder.U32.Insts.ZerocopyIntoBytes O) := + ⟨initializedWrapperRepresentation + (fun raw => Zerocopy.byteorder.U32.mk raw Zerocopy.core.marker.PhantomData.mk) + (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8))⟩ + +@[instance] theorem byteorder.U64.Insts.ZerocopyIntoBytes_law + (O : Type) [meaning : RustModel O] : + TraitLaws.into_bytes_initialized (Zerocopy.byteorder.U64 O) + (Zerocopy.byteorder.U64.Insts.ZerocopyIntoBytes O) := + ⟨initializedWrapperRepresentation + (fun raw => Zerocopy.byteorder.U64.mk raw Zerocopy.core.marker.PhantomData.mk) + (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8))⟩ + +@[instance] theorem byteorder.U128.Insts.ZerocopyIntoBytes_law + (O : Type) [meaning : RustModel O] : + TraitLaws.into_bytes_initialized (Zerocopy.byteorder.U128 O) + (Zerocopy.byteorder.U128.Insts.ZerocopyIntoBytes O) := + ⟨initializedWrapperRepresentation + (fun raw => Zerocopy.byteorder.U128.mk raw Zerocopy.core.marker.PhantomData.mk) + (RustModel.initialized_array U8 (16#usize) (initializedUScalar .U8))⟩ + +@[instance] theorem byteorder.Usize.Insts.ZerocopyIntoBytes_law + (O : Type) [meaning : RustModel O] : + TraitLaws.into_bytes_initialized (Zerocopy.byteorder.Usize O) + (Zerocopy.byteorder.Usize.Insts.ZerocopyIntoBytes O) := + ⟨initializedWrapperRepresentation + (fun raw => Zerocopy.byteorder.Usize.mk raw Zerocopy.core.marker.PhantomData.mk) + (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8))⟩ + +@[instance] theorem byteorder.I16.Insts.ZerocopyIntoBytes_law + (O : Type) [meaning : RustModel O] : + TraitLaws.into_bytes_initialized (Zerocopy.byteorder.I16 O) + (Zerocopy.byteorder.I16.Insts.ZerocopyIntoBytes O) := + ⟨initializedWrapperRepresentation + (fun raw => Zerocopy.byteorder.I16.mk raw Zerocopy.core.marker.PhantomData.mk) + (RustModel.initialized_array U8 (2#usize) (initializedUScalar .U8))⟩ + +@[instance] theorem byteorder.I32.Insts.ZerocopyIntoBytes_law + (O : Type) [meaning : RustModel O] : + TraitLaws.into_bytes_initialized (Zerocopy.byteorder.I32 O) + (Zerocopy.byteorder.I32.Insts.ZerocopyIntoBytes O) := + ⟨initializedWrapperRepresentation + (fun raw => Zerocopy.byteorder.I32.mk raw Zerocopy.core.marker.PhantomData.mk) + (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8))⟩ + +@[instance] theorem byteorder.I64.Insts.ZerocopyIntoBytes_law + (O : Type) [meaning : RustModel O] : + TraitLaws.into_bytes_initialized (Zerocopy.byteorder.I64 O) + (Zerocopy.byteorder.I64.Insts.ZerocopyIntoBytes O) := + ⟨initializedWrapperRepresentation + (fun raw => Zerocopy.byteorder.I64.mk raw Zerocopy.core.marker.PhantomData.mk) + (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8))⟩ + +@[instance] theorem byteorder.I128.Insts.ZerocopyIntoBytes_law + (O : Type) [meaning : RustModel O] : + TraitLaws.into_bytes_initialized (Zerocopy.byteorder.I128 O) + (Zerocopy.byteorder.I128.Insts.ZerocopyIntoBytes O) := + ⟨initializedWrapperRepresentation + (fun raw => Zerocopy.byteorder.I128.mk raw Zerocopy.core.marker.PhantomData.mk) + (RustModel.initialized_array U8 (16#usize) (initializedUScalar .U8))⟩ + +@[instance] theorem byteorder.Isize.Insts.ZerocopyIntoBytes_law + (O : Type) [meaning : RustModel O] : + TraitLaws.into_bytes_initialized (Zerocopy.byteorder.Isize O) + (Zerocopy.byteorder.Isize.Insts.ZerocopyIntoBytes O) := + ⟨initializedWrapperRepresentation + (fun raw => Zerocopy.byteorder.Isize.mk raw Zerocopy.core.marker.PhantomData.mk) + (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8))⟩ + +@[instance] theorem byteorder.F32.Insts.ZerocopyIntoBytes_law + (O : Type) [meaning : RustModel O] : + TraitLaws.into_bytes_initialized (Zerocopy.byteorder.F32 O) + (Zerocopy.byteorder.F32.Insts.ZerocopyIntoBytes O) := + ⟨initializedWrapperRepresentation + (fun raw => Zerocopy.byteorder.F32.mk raw Zerocopy.core.marker.PhantomData.mk) + (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8))⟩ + +@[instance] theorem byteorder.F64.Insts.ZerocopyIntoBytes_law + (O : Type) [meaning : RustModel O] : + TraitLaws.into_bytes_initialized (Zerocopy.byteorder.F64 O) + (Zerocopy.byteorder.F64.Insts.ZerocopyIntoBytes O) := + ⟨initializedWrapperRepresentation + (fun raw => Zerocopy.byteorder.F64.mk raw Zerocopy.core.marker.PhantomData.mk) + (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8))⟩ + end Zerocopy.Proofs diff --git a/verification/aeneas/projections/ModelShapes.lean b/verification/aeneas/projections/ModelShapes.lean index 3079f053ed..7c7177520b 100644 --- a/verification/aeneas/projections/ModelShapes.lean +++ b/verification/aeneas/projections/ModelShapes.lean @@ -24,7 +24,31 @@ derive_model_shape Zerocopy.byteorder.U16 with 1 type parameters derive_model_shape Zerocopy.byteorder.U32 with 1 type parameters +derive_model_shape Zerocopy.byteorder.U64 with 1 type parameters + +derive_model_shape Zerocopy.byteorder.U128 with 1 type parameters + +derive_model_shape Zerocopy.byteorder.Usize with 1 type parameters + +derive_model_shape Zerocopy.byteorder.I16 with 1 type parameters + +derive_model_shape Zerocopy.byteorder.I32 with 1 type parameters + +derive_model_shape Zerocopy.byteorder.I64 with 1 type parameters + +derive_model_shape Zerocopy.byteorder.I128 with 1 type parameters + +derive_model_shape Zerocopy.byteorder.Isize with 1 type parameters + +derive_model_shape Zerocopy.byteorder.F32 with 1 type parameters + +derive_model_shape Zerocopy.byteorder.F64 with 1 type parameters + derive_model_shape Zerocopy.trait_checks.XorCodec with 0 type parameters derive_model_shape Zerocopy.trait_checks.Forward with 1 type parameters +derive_model_shape Zerocopy.wrappers.Unalign with 1 type parameters + +derive_model_shape Zerocopy.wrappers.read_only_def.ReadOnly with 1 type parameters + diff --git a/verification/aeneas/projections/Models.lean b/verification/aeneas/projections/Models.lean index 67cf095612..36e1204eb0 100644 --- a/verification/aeneas/projections/Models.lean +++ b/verification/aeneas/projections/Models.lean @@ -28,9 +28,45 @@ check_model_binding Zerocopy.byteorder.U16 with 1 type parameters derive_rust_model Zerocopy.byteorder.U32 with 1 type parameters with_physical 0 check_model_binding Zerocopy.byteorder.U32 with 1 type parameters +derive_rust_model Zerocopy.byteorder.U64 with 1 type parameters with_physical 0 +check_model_binding Zerocopy.byteorder.U64 with 1 type parameters + +derive_rust_model Zerocopy.byteorder.U128 with 1 type parameters with_physical 0 +check_model_binding Zerocopy.byteorder.U128 with 1 type parameters + +derive_rust_model Zerocopy.byteorder.Usize with 1 type parameters with_physical 0 +check_model_binding Zerocopy.byteorder.Usize with 1 type parameters + +derive_rust_model Zerocopy.byteorder.I16 with 1 type parameters with_physical 0 +check_model_binding Zerocopy.byteorder.I16 with 1 type parameters + +derive_rust_model Zerocopy.byteorder.I32 with 1 type parameters with_physical 0 +check_model_binding Zerocopy.byteorder.I32 with 1 type parameters + +derive_rust_model Zerocopy.byteorder.I64 with 1 type parameters with_physical 0 +check_model_binding Zerocopy.byteorder.I64 with 1 type parameters + +derive_rust_model Zerocopy.byteorder.I128 with 1 type parameters with_physical 0 +check_model_binding Zerocopy.byteorder.I128 with 1 type parameters + +derive_rust_model Zerocopy.byteorder.Isize with 1 type parameters with_physical 0 +check_model_binding Zerocopy.byteorder.Isize with 1 type parameters + +derive_rust_model Zerocopy.byteorder.F32 with 1 type parameters with_physical 0 +check_model_binding Zerocopy.byteorder.F32 with 1 type parameters + +derive_rust_model Zerocopy.byteorder.F64 with 1 type parameters with_physical 0 +check_model_binding Zerocopy.byteorder.F64 with 1 type parameters + derive_rust_model Zerocopy.trait_checks.XorCodec with 0 type parameters check_model_binding Zerocopy.trait_checks.XorCodec with 0 type parameters derive_rust_model Zerocopy.trait_checks.Forward with 1 type parameters check_model_binding Zerocopy.trait_checks.Forward with 1 type parameters +derive_rust_model Zerocopy.wrappers.Unalign with 1 type parameters with_physical 0 +check_model_binding Zerocopy.wrappers.Unalign with 1 type parameters + +derive_rust_model Zerocopy.wrappers.read_only_def.ReadOnly with 1 type parameters with_physical 0 +check_model_binding Zerocopy.wrappers.read_only_def.ReadOnly with 1 type parameters + diff --git a/zerocopy/src/byteorder.rs b/zerocopy/src/byteorder.rs index f0107a8c6b..2348a0f085 100644 --- a/zerocopy/src/byteorder.rs +++ b/zerocopy/src/byteorder.rs @@ -542,7 +542,6 @@ example of how it can be used for parsing UDP packets. impl_or_verify!(O => TryFromBytes for $name); impl_or_verify!(O => FromZeros for $name); impl_or_verify!(O => FromBytes for $name); - impl_or_verify!(O => IntoBytes for $name); impl_or_verify!(O => Unaligned for $name); }; @@ -971,6 +970,88 @@ define_type!( [] ); +// These handwritten impls are selected by the default-feature library build. +// With `derive` or `test`, `impl_or_verify!` checks the separately derived impls; +// those generated declarations are outside the current invariant-proof scope. +#[allow(unused_unsafe)] +#[allow(clippy::multiple_unsafe_ops_per_block)] +// SAFETY: Each wrapper is `repr(transparent)` over a `u8` array and a +// `PhantomData` field. Its entire storage is the initialized array storage. +const _: () = unsafe { + impl_or_verify!( + /// ```aeneas + /// invariant_proof + /// ``` + O => IntoBytes for U16 + ); + impl_or_verify!( + /// ```aeneas + /// invariant_proof + /// ``` + O => IntoBytes for U32 + ); + impl_or_verify!( + /// ```aeneas + /// invariant_proof + /// ``` + O => IntoBytes for U64 + ); + impl_or_verify!( + /// ```aeneas + /// invariant_proof + /// ``` + O => IntoBytes for U128 + ); + impl_or_verify!( + /// ```aeneas + /// invariant_proof + /// ``` + O => IntoBytes for Usize + ); + impl_or_verify!( + /// ```aeneas + /// invariant_proof + /// ``` + O => IntoBytes for I16 + ); + impl_or_verify!( + /// ```aeneas + /// invariant_proof + /// ``` + O => IntoBytes for I32 + ); + impl_or_verify!( + /// ```aeneas + /// invariant_proof + /// ``` + O => IntoBytes for I64 + ); + impl_or_verify!( + /// ```aeneas + /// invariant_proof + /// ``` + O => IntoBytes for I128 + ); + impl_or_verify!( + /// ```aeneas + /// invariant_proof + /// ``` + O => IntoBytes for Isize + ); + impl_or_verify!( + /// ```aeneas + /// invariant_proof + /// ``` + O => IntoBytes for F32 + ); + impl_or_verify!( + /// ```aeneas + /// invariant_proof + /// ``` + O => IntoBytes for F64 + ); +}; + macro_rules! module { ($name:ident, $trait:ident, $endianness_str:expr) => { /// Numeric primitives stored in diff --git a/zerocopy/src/impls.rs b/zerocopy/src/impls.rs index 3f6c672b24..e3d2c10f14 100644 --- a/zerocopy/src/impls.rs +++ b/zerocopy/src/impls.rs @@ -906,7 +906,12 @@ const _: () = unsafe { impl_for_transmute_from!(T: TryFromBytes => TryFromBytes for Wrapping[T]); impl_for_transmute_from!(T: FromZeros => FromZeros for Wrapping[T]); impl_for_transmute_from!(T: FromBytes => FromBytes for Wrapping[T]); -impl_for_transmute_from!(T: IntoBytes => IntoBytes for Wrapping[T]); +impl_for_transmute_from!( + /// ```aeneas + /// invariant_proof + /// ``` + T: IntoBytes => IntoBytes for Wrapping[T] +); assert_unaligned!(Wrapping<()>, Wrapping); // SAFETY: Per [1], `Wrapping` has the same layout as `T`. Since its single @@ -980,7 +985,12 @@ const _: () = unsafe { unsafe_impl!(T: ?Sized + Immutable => Immutable for Manua impl_for_transmute_from!(T: ?Sized + TryFromBytes => TryFromBytes for ManuallyDrop[T]); impl_for_transmute_from!(T: ?Sized + FromZeros => FromZeros for ManuallyDrop[T]); impl_for_transmute_from!(T: ?Sized + FromBytes => FromBytes for ManuallyDrop[T]); -impl_for_transmute_from!(T: ?Sized + IntoBytes => IntoBytes for ManuallyDrop[T]); +impl_for_transmute_from!( + /// ```aeneas + /// invariant_proof + /// ``` + T: ?Sized + IntoBytes => IntoBytes for ManuallyDrop[T] +); // SAFETY: `ManuallyDrop` has the same layout as `T` [1], and thus has the // same alignment as `T`. // @@ -1070,7 +1080,12 @@ const _: () = { impl_for_transmute_from!(T: ?Sized + TryFromBytes => TryFromBytes for Cell[T]); impl_for_transmute_from!(T: ?Sized + FromZeros => FromZeros for Cell[T]); impl_for_transmute_from!(T: ?Sized + FromBytes => FromBytes for Cell[T]); -impl_for_transmute_from!(T: ?Sized + IntoBytes => IntoBytes for Cell[T]); +impl_for_transmute_from!( + /// ```aeneas + /// invariant_proof + /// ``` + T: ?Sized + IntoBytes => IntoBytes for Cell[T] +); // SAFETY: `Cell` has the same in-memory representation as `T` [1], and thus // has the same alignment as `T`. // @@ -1081,7 +1096,12 @@ const _: () = unsafe { unsafe_impl!(T: ?Sized + Unaligned => Unaligned for Cell< impl_for_transmute_from!(T: ?Sized + FromZeros => FromZeros for UnsafeCell[T]); impl_for_transmute_from!(T: ?Sized + FromBytes => FromBytes for UnsafeCell[T]); -impl_for_transmute_from!(T: ?Sized + IntoBytes => IntoBytes for UnsafeCell[T]); +impl_for_transmute_from!( + /// ```aeneas + /// invariant_proof + /// ``` + T: ?Sized + IntoBytes => IntoBytes for UnsafeCell[T] +); // SAFETY: `UnsafeCell` has the same in-memory representation as `T` [1], and // thus has the same alignment as `T`. // diff --git a/zerocopy/src/wrappers.rs b/zerocopy/src/wrappers.rs index 2d4ff55159..ea3e97f116 100644 --- a/zerocopy/src/wrappers.rs +++ b/zerocopy/src/wrappers.rs @@ -155,7 +155,12 @@ const _: () = unsafe { ); impl_or_verify!(T: FromZeros => FromZeros for Unalign); impl_or_verify!(T: FromBytes => FromBytes for Unalign); - impl_or_verify!(T: IntoBytes => IntoBytes for Unalign); + impl_or_verify!( + /// ```aeneas + /// invariant_proof + /// ``` + T: IntoBytes => IntoBytes for Unalign + ); }; // Note that `Unalign: Clone` only if `T: Copy`. Since the inner `T` may not be @@ -684,7 +689,12 @@ const _: () = unsafe { ); unsafe_impl!(T: ?Sized + FromZeros => FromZeros for ReadOnly); unsafe_impl!(T: ?Sized + FromBytes => FromBytes for ReadOnly); - unsafe_impl!(T: ?Sized + IntoBytes => IntoBytes for ReadOnly); + unsafe_impl!( + /// ```aeneas + /// invariant_proof + /// ``` + T: ?Sized + IntoBytes => IntoBytes for ReadOnly + ); }; // SAFETY: By invariant, `inner` is never mutated through a `&ReadOnly`