From 3580b1d52e3fb5373f7a480e8e79efde29fbf8d6 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser's Agent Date: Tue, 8 Sep 2026 23:51:34 +0000 Subject: [PATCH] [kani] Prove Unalign update write-back *Authored by an AI agent acting on Josh Liebow-Feeser's behalf.* gherrit-pr-id: G56sp4dsuukjpe3trlzhqbkuvl6f53jkg --- zerocopy/src/wrappers.rs | 613 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 612 insertions(+), 1 deletion(-) diff --git a/zerocopy/src/wrappers.rs b/zerocopy/src/wrappers.rs index 8b52996108..efbd3af665 100644 --- a/zerocopy/src/wrappers.rs +++ b/zerocopy/src/wrappers.rs @@ -367,7 +367,7 @@ impl Unalign { // SAFETY: `slf` is the raw pointer value of `self`. We know it // is valid for writes and properly aligned because `self` is a // mutable reference, which guarantees both of these properties. - unsafe { ptr::write(self.slf, Unalign::new(copy)) }; + unsafe { ptr::write(self.slf, Unalign(copy)) }; } } @@ -845,6 +845,617 @@ where } } +#[cfg(kani)] +mod proofs { + use super::*; + use crate::proof_support::assert_same_usize; + + // Configuration: Uses the common Kani CI configuration documented in + // `agent_docs/validation.md`: the CI-pinned Kani release and its bundled + // x86_64-unknown-linux-gnu compiler, the stable-compatible feature bundle, + // `-Zfunction-contracts`, and one layout selected by `--randomize-layout` + // per invocation. + // + // Domain: These normal-return harnesses are universal over every ordered + // triple of old, new, and closure-result byte values in the exact Kani + // model. In `any_unalign_update_values`, Rust evaluates the three tuple- + // expression operands in order; their results initialize tuple fields zero, + // one, and two respectively. The helper returns that tuple through its tail + // expression, and each harness's `(old, new, result)` tuple pattern + // destructures those positional fields into the correspondingly ordered + // bindings [7][35]. Each operand calls `kani::any::()`. Kani + // 0.67 documents `any::()` as representing every valid `T`; its `u8` + // implementation reaches `AnyRawHook` without a validity restriction + // [29][36]. That hook assigns a backend nondeterministic value to the call + // destination. Kani 0.67 pins CBMC 6.8.0, whose nondeterminism model + // permits any computation arising from its choices and permits separate + // nondeterministic calls to return different results [37]. + // + // Inspection of the exact linked GOTO programs produced for both harnesses + // under the common configuration found three ordered `any` calls assigning + // helper locals, followed by tuple construction and field bindings to + // `old`, `new`, and `result` in the same order. The shared raw-any body + // contains one static nondeterministic assignment which all three calls + // execute. We accept as a TOOL/TCB premise—not + // a conclusion of either harness—that the exact Kani 0.67/CBMC 6.8.0 + // lowering gives those three dynamic evaluations fresh, mutually + // unconstrained byte choices. This is a premise about dynamic evaluations, + // not a claim that the GOTO program contains three static nondeterministic + // nodes. Under that premise and Rust's `u8` range [13], the modeled + // input domain before the target call is exactly the Cartesian product + // `0..=255` × `0..=255` × `0..=255`. No source-level `kani::assume` + // constrains any choice or relates them. Only after all target + // postconditions does each + // harness call `cover_unalign_update_byte_partitions`; those covers use + // `u8` equality and inequality [27]. In the final cover, Rust's Boolean + // `&&` is logical AND and evaluates the right operand only if the left is + // true [39]. Thus `result != old && result != new` is true exactly when + // both independently grounded inequalities are true: the result differs + // from both field values. These covers establish only terminal + // reachability of the old/new equal and unequal partitions and the + // result's equal, unequal, and distinct-from-both partitions. They do not + // establish the Cartesian product. + // One harness uses a + // `repr(transparent)` wrapper over `u8`, whose alignment is one. The other + // uses a `repr(C)` value with a destructor whose greater-than-one alignment + // is an explicit premise of the pinned compiler/target case. That value's + // `Unalign` receiver is at byte offset one in a `repr(C)` backing object + // aligned to the inner type, and is therefore physically misaligned for the + // inner type. Fail-closed `size_of` assertions record the pinned target's + // exact sizes: `Byte` and `Unalign` are one byte, `DropTracked` and + // `Unalign` are 16 bytes, and `Misaligned` is 24 + // bytes. The alignment-one harness body declares six named locals; the + // write-back harness body declares eight. The latter count treats the + // zero-length alignment field as part of `backing`, not as a separate + // object. These are deliberately only harness-body binding counts: the + // exact reachable source paths also contain closure values and parameters, + // the terminal cover-helper parameters, and target/helper bindings (`t` on + // the alignment-one path; `copy`, `write_back`, `ret`, and the guard's + // second `copy` on the write-back path), plus function receiver parameters. + // The compiler may elide those values or introduce temporaries, so this + // proof makes no claim about a total stack-object count or stack-frame size. + // The harnesses and target perform no dynamic allocation, contain no + // `kani::assume`, and have no explicit source-level loop. Their explicit + // unwind bound is one, which also applies to any target or language-oracle + // loop Kani reaches, with unwinding assertions enabled. + // + // Establishes: Together, they exercise both branches of `Unalign::update`, + // including closure-result forwarding, mutation write-back from a receiver + // physically misaligned for `DropTracked`, and one observable final + // destructor. + // + // Proof-only isolation: Calls to the compiler-defined tuple-struct + // constructor create the receiver without calling `Unalign::new`, and the + // write-back branch restores the receiver through that same constructor + // [1]. Thus neither exercised target branch depends on `Unalign::new`, so a + // defect in that constructor cannot compensate for an `update` defect. A + // tuple-struct pattern observes the result without calling `into_inner`. + // + // Alignment and placement oracles: `align_of` returns a type's ABI-required + // alignment [15]. Every `size_of`, `align_of`, and `offset_of!` query below + // produces a `usize`; the shared `assert_same_usize` makes a mismatch fail + // through `assert_eq!` and `usize::PartialEq` [27]. It supplies equality + // mechanics only. The expected numeric sizes and offsets remain the + // language-derived or pinned-compiler premises described here, not general + // layout theorems. The expected layout values and alignment threshold use + // `usize`-suffixed literals. Rust assigns those literals the suffix's + // primitive type. Its integer-literal evaluation rules select decimal + // radix, remove the suffix, parse the digits as `u128`, and cast to the + // expression's type. Zero, one, sixteen, and twenty-four all fit the pinned + // target's 64-bit `usize`, so these literals supply those exact values [33]. + // `Byte` has the same layout as `u8` by its transparent representation + // [16]. Rust fixes `u8`'s size at one byte, requires alignment to be at + // least one, and requires size to be a multiple of alignment, so `Byte`'s + // alignment is exactly one [17]. This supplies the expected result of the + // first alignment assertion and selects the direct reference branch + // independently of `update`. + // + // Rust does not fix reference alignment across targets. For the pinned + // x86_64 compiler/target, the second alignment assertion records and checks + // the exact compiler-layout premise that `DropTracked`'s alignment exceeds + // one through primitive `usize` ordering [28]; no cross-target inference is + // made. `Unalign` is declared + // `#[repr(C, packed)]`. Rust specifies that an omitted packing value is one + // and that `packed` lowers the type and field-positioning alignments [21]. + // Since every Rust alignment is at least one [17], `Unalign` therefore + // has alignment exactly one. Arrays of length zero have size zero and + // retain their element alignment [18]. The `repr(C)` backing type is + // consequently aligned to `T`, places its one-byte prefix at offset zero, + // and places its alignment-one `Unalign` field immediately afterward at + // offset one [19]. Since the base is aligned to `T` and `T`'s alignment is + // greater than one, that field address is not aligned to `T`. Applying the + // same `repr(C)` first-field rule to `Unalign` places its sole tuple field + // at offset zero; a separate `offset_of!` assertion records that edge + // explicitly. `offset_of!` asks the compiler for each field's byte offset; + // `addr_of!` obtains the inner field's address without creating a reference; + // and `is_aligned` reports whether it meets `T`'s alignment [20]. Those + // contracts supply the offsets, outer alignment, and physical-misalignment + // assertions before the write-back branch is called. These explicit + // representation guarantees, rather than an unspecified default layout, + // supply the relevant placement under layout randomization. + // + // Rust's Boolean truth table makes `!b` true exactly when `b` is false + // [30]. Consequently, `!receiver.is_aligned()` denotes physical + // misalignment under [20], both in the assertion and the matching cover. + // `assert!` requires its Boolean operand to evaluate to true and cannot be + // disabled [30]; Kani 0.67 maps the no-message form used here to a verifier + // assertion, whose false condition fails verification [31]. These + // contracts also govern the earlier + // `assert!(mem::align_of::>() > 1)`, whose comparison is + // supplied by [28]. The cover asks whether the same misalignment predicate + // is satisfiable at that point [32]. + // + // Other language oracles and assertion mapping: Named-field struct + // expressions initialize `DropTracked::value` with `old` and pass that + // value through `Misaligned::new` into its named `value` field [23]. This + // supplies the proof setup against which the closure-input assertion tests + // the target. Tuple-struct patterns destructure the wrapper, and their + // default binding mode moves the field into the `restored` local [2][3]. + // More specifically, Rust says a place bound by value in a pattern denotes + // the value stored there, and permits moving a field when its containing + // place is movable and does not implement `Drop` [26]. Both `Misaligned` and + // `Unalign` meet that condition. Rust's packed-field guidance identifies + // direct value access as the alternative to creating a forbidden unaligned + // reference [21]. Thus both `Unalign(restored)` patterns observe the packed + // field by a language-checked value move, rather than through a reference. + // Compiler/Kani lowering of the non-`Copy`, unaligned field move remains part + // of the TOOL/TCB boundary below. Each + // closure maps its parameter to its body expression [4]. The bare `old`, + // `new`, and `result` paths in both bodies are capture paths rooted in the + // correspondingly named enclosing locals. Both closures omit `move`, so + // Rust infers their capture modes while preferring shared references; each + // body only reads these three locals, and therefore captures all three + // through `ImmBorrow` [38]. A local path is a place expression. Evaluating + // each captured occurrence in the assertion operand, assignment right-hand + // side, or tail result's value context obtains the stored value and copies + // it because `u8: Copy` [9][38]. Thus every `old`, `new`, and `result` use + // observes tuple fields zero, one, and two respectively. The body executes + // its statements in order and evaluates its final operand in value context + // [5]. Assignment copies or moves the right-hand value into the selected + // place [6]. + // Together those rules supply the expected closure input, field mutation, + // and closure result without treating compiler capture behavior as an + // unstated oracle. At the `update` function boundary, + // `return f(t)` short-circuits the implicit return while the tail expression + // `ret` is returned to the caller [7]. Those two language paths map directly + // to the two `returned` assertions. + // + // Finally, safe `drop` moves and drops `restored` before returning [8]. A + // moved local is deinitialized [9], and a partially initialized aggregate + // drops only fields which remain initialized [10]. The field-move rule [26] + // makes the two containing aggregates partially initialized: the by-value + // wrapper pattern leaves no initialized wrapper field to drop, while + // `backing` retains only its prefix and zero-length alignment fields. + // `drop(restored)` then moves and deinitializes `restored` while running its + // destructor inside `drop`. Destruction of the + // `DropTracked` value calls its `Drop::drop` implementation [10]. Moving + // `backing.value` leaves `_prefix` and `_align` initialized. Array + // destruction visits its elements [24], and `[DropTracked; 0]` has no + // elements, so `_align` invokes no `DropTracked` destructor; `_prefix` is a + // `u8` without a destructor. When the restored value's method is invoked, + // [5] executes its single body statement, + // `*self.drops += 1u8`. The harness initializes `drops` with `0u8` and the + // final assertion compares it with `1u8`. Rust specifies that each suffixed + // integer literal has the suffix's primitive type and defines the decimal + // values represented by these tokens [33]. Thus all three literals are + // explicitly typed `u8`; this proof consumes no unsuffixed-literal + // inference or integer default. The mutable local `drops` denotes its memory + // location; `&mut drops` produces a mutable reference to that location, and + // the named-field struct expression stores that reference in + // `DropTracked::drops` [23][34]. Inside `Drop::drop`, field access through + // `self` denotes the stored field's location (automatically dereferencing + // the `&mut DropTracked` receiver), and applying built-in `*` to the stored + // `&mut u8` denotes that reference's pointed-to location and makes it + // assignable [34]. Thus the left operand of `*self.drops += 1u8` mutates the + // pointee of the reference that `update` restored. The final assertion tests + // that the observable connection to the original harness counter survived + // that target path; these language rules do not assume that conclusion. + // This test remains subject to the TOOL/TCB premise below that the stored + // reference remains live and exclusive across `update`'s raw moves. Rust + // specifies that the assigned place is mutated by applying the operator + // [11], and specifies integer `+` as addition [12]. The specified `u8` range + // includes zero and one [13], so the mathematical result `0 + 1 = 1` is in + // range and does not meet Rust's definition of overflow [14]. The final + // `assert_eq!` compares the observed and expected `u8` values through + // `u8::PartialEq` [27]. Thus the expected single destructor invocation + // changes the counter once from zero to one, and the final assertion checks + // that specific effect without relying on a second target API. The + // move/destruction argument above supplies the exactly-once expectation; + // this does not claim that a `u8` counter is an injective record of an + // arbitrary number of destructor invocations. + // + // They do not prove `update` for arbitrary types, alignments, physical + // offsets, or layouts; extend the selected compiler's `DropTracked` + // alignment premise to another compiler or target; model panic unwinding or + // abort; or establish reference aliasing and lifetime validity, raw-pointer + // provenance, invalid-value, or uninitialized-memory obligations. Kani + // lists pointer-aliasing violations and invalid values as unsupported and + // does not track reference lifetimes [22]. In particular, the mutation and + // destructor assertions do not prove that moving `DropTracked` with + // `ptr::read`, using its `&mut u8`, and writing it back with `ptr::write` + // respects that reference's liveness and exclusive-access rules. Those are + // TOOL/TCB premises, not proof conclusions. Kani's feature table also marks + // destructors and `Drop` as only partially supported [22]. The exactly-once + // normal-path destructor result is therefore conditional on Kani 0.67's + // lowering and execution model for the particular drops reached here; the + // harness does not independently establish that model. The ordinary test + // module below separately samples panic restoration, but this Kani proof + // does not model panic unwinding. + // + // [1] Per Rust 1.93's tuple-struct-construction contract: + // + // The constructor is a function which can be called to create a new + // instance of the struct. + // + // https://doc.rust-lang.org/1.93.0/reference/items/structs.html#r-items.struct.tuple + // + // [2] Per Rust 1.93's tuple-struct-pattern contract: + // + // They are also used to destructure a tuple struct or enum value. + // + // https://doc.rust-lang.org/1.93.0/reference/patterns.html#tuple-struct-patterns + // + // [3] Per Rust 1.93's binding-mode contract: + // + // The default binding mode starts in “move” mode which uses move + // semantics. + // + // https://doc.rust-lang.org/1.93.0/reference/patterns.html#binding-modes + // + // [4] Per Rust 1.93's closure contract: + // + // A closure expression denotes a function that maps a list of + // parameters onto the expression that follows the parameters. + // + // https://doc.rust-lang.org/1.93.0/reference/expressions/closure-expr.html + // + // [5] Per Rust 1.93's block-expression contract: + // + // As a control flow expression, a block sequentially executes its + // component non-item declaration statements and then its final optional + // expression. + // + // Blocks are always value expressions and evaluate the last operand in + // value expression context. + // + // https://doc.rust-lang.org/1.93.0/reference/expressions/block-expr.html + // + // [6] Per Rust 1.93's assignment contract: + // + // Next it either copies or moves the assigned value to the assigned + // place. + // + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#assignment-expressions + // + // [7] Per Rust 1.93's function-body contract, the body first binds its + // argument patterns and then returns its body value; specifically: + // + // This means that the tail expression of the block, if evaluated, ends + // up being returned to the caller. As usual, an explicit return + // expression within the body of the function will short-cut that + // implicit return, if reached. + // + // https://doc.rust-lang.org/1.93.0/reference/items/functions.html#function-body + // + // [8] Per Rust 1.93's `drop` contract: + // + // Because `_x` is moved into the function, it is automatically dropped + // before the function returns. + // + // https://doc.rust-lang.org/1.93.0/std/mem/fn.drop.html + // + // [9] Per Rust 1.93's move-expression contract: + // + // After moving out of a place expression that evaluates to a local + // variable, the location is deinitialized and cannot be read from again + // until it is reinitialized. + // + // https://doc.rust-lang.org/1.93.0/reference/expressions.html#moved-and-copied-types + // + // [10] Per Rust 1.93's destructor contract, destruction of `T: Drop` calls + // `::drop`, and: + // + // If a variable has been partially initialized, only its initialized + // fields are dropped. + // + // https://doc.rust-lang.org/1.93.0/reference/destructors.html + // + // [11] Per Rust 1.93's compound-assignment contract: + // + // Compound assignment expressions combine arithmetic and logical + // binary operators with assignment expressions. + // + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#r-expr.compound-assign.intro + // + // For operands known to be primitive, the same contract specifies that: + // + // the place given by the evaluation of the left hand side is mutated + // by applying the operator to the values of both sides. + // + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#r-expr.compound-assign.primitives + // + // [12] Rust 1.93's arithmetic-operator table assigns integer `+` the + // behavior "Addition": + // + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#r-expr.arith-logic.behavior + // + // [13] Rust 1.93's unsigned-integer table gives `u8` minimum `0` and + // maximum `2^8 - 1`: + // + // https://doc.rust-lang.org/1.93.0/reference/types/numeric.html#r-type.numeric.int.unsigned + // + // [14] Per Rust 1.93's integer-overflow contract, overflow includes: + // + // When `+`, `*` or binary `-` create a value greater than the maximum + // value, or less than the minimum value that can be stored. + // + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#r-expr.operator.int-overflow.binary-arith + // + // [15] Rust 1.93 specifies that `align_of` returns the ABI-required minimum + // alignment of the type in bytes: + // + // https://doc.rust-lang.org/1.93.0/core/mem/fn.align_of.html + // + // [16] Rust 1.93 specifies that a transparent struct has the same layout + // and ABI as its only non-zero-sized field: + // + // https://doc.rust-lang.org/1.93.0/reference/type-layout.html#r-layout.repr.transparent.layout-abi + // + // [17] Rust 1.93 specifies that `u8` has size one, alignment is at least + // one, and size is a multiple of alignment: + // + // https://doc.rust-lang.org/1.93.0/reference/type-layout.html#r-layout.primitive.size + // https://doc.rust-lang.org/1.93.0/reference/type-layout.html#r-layout.properties.align + // https://doc.rust-lang.org/1.93.0/reference/type-layout.html#r-layout.properties.size + // + // [18] Rust 1.93 specifies that `[T; N]` has size + // `size_of::() * N` and the same alignment as `T`: + // + // https://doc.rust-lang.org/1.93.0/reference/type-layout.html#array-layout + // + // [19] Rust 1.93 specifies that a `repr(C)` struct is aligned to its most + // aligned field and places fields in declaration order with only the + // padding needed for each field's alignment: + // + // https://doc.rust-lang.org/1.93.0/reference/type-layout.html#r-layout.repr.c.struct.align + // https://doc.rust-lang.org/1.93.0/reference/type-layout.html#r-layout.repr.c.struct.size-field-offset + // + // [20] Rust 1.93 specifies that `offset_of!` expands to a field's byte + // offset, `addr_of!` creates a raw pointer without creating a reference, + // pointer `cast` casts to another pointer type, and `is_aligned` reports + // whether the pointer is properly aligned for `T`: + // + // https://doc.rust-lang.org/1.93.0/core/mem/macro.offset_of.html + // https://doc.rust-lang.org/1.93.0/std/ptr/macro.addr_of.html + // https://doc.rust-lang.org/1.93.0/std/primitive.pointer.html#method.cast + // https://doc.rust-lang.org/1.93.0/std/primitive.pointer.html#method.is_aligned + // + // [21] Rust 1.93 specifies: + // + // For `packed`, if no value is given, as in `#[repr(packed)]`, then the + // value is 1. + // + // It also makes each positioning alignment the smaller of that value and + // the field type's alignment. For value access at such an alignment, its + // guidance says references to unaligned fields are not allowed and: + // + // Instead of creating a reference to a field, copy the value to a local + // variable. + // + // https://doc.rust-lang.org/1.93.0/reference/type-layout.html#r-layout.repr.alignment.intro + // https://doc.rust-lang.org/1.93.0/reference/type-layout.html#r-layout.repr.alignment.constraint-alignment + // https://doc.rust-lang.org/1.93.0/reference/type-layout.html#r-layout.repr.alignment.packed + // https://doc.rust-lang.org/1.93.0/reference/type-layout.html#r-layout.repr.alignment.packed-fields + // + // [22] Kani documents pointer-aliasing violations and invalid values as + // unsupported, documents that it does not track reference lifetimes, and + // marks destructors and `Drop` as partially supported: + // + // https://model-checking.github.io/kani/rust-feature-support.html + // https://model-checking.github.io/kani/undefined-behaviour.html + // + // [23] Rust 1.93 specifies that a struct expression creates a struct value + // and that its named fields are supplied by the corresponding field values: + // https://doc.rust-lang.org/1.93.0/reference/expressions/struct-expr.html + // + // [24] Rust 1.93 specifies: + // + // The elements of an array or owned slice are dropped in order from the + // first element to the last. + // + // https://doc.rust-lang.org/1.93.0/reference/destructors.html#destructors.operation.sequence + // + // [25] Rust 1.93 specifies that `size_of` returns a type's size in bytes: + // https://doc.rust-lang.org/1.93.0/core/mem/fn.size_of.html + // + // [26] Rust 1.93 specifies that a place "bound by value in a pattern" + // denotes the value stored there, and permits moving fields out of a movable + // containing place which does not implement `Drop`: + // https://doc.rust-lang.org/1.93.0/reference/expressions.html#moved-and-copied-types + // https://doc.rust-lang.org/1.93.0/reference/expressions/field-expr.html#borrowing + // + // [27] https://doc.rust-lang.org/1.93.0/std/macro.assert_eq.html + // https://doc.rust-lang.org/1.93.0/std/cmp/trait.PartialEq.html#tymethod.eq + // https://doc.rust-lang.org/1.93.0/std/cmp/trait.PartialEq.html#method.ne + // https://doc.rust-lang.org/1.93.0/std/primitive.usize.html#impl-PartialEq-for-usize + // https://doc.rust-lang.org/1.93.0/std/primitive.u8.html#impl-PartialEq-for-u8 + // + // [28] https://doc.rust-lang.org/1.93.0/std/cmp/trait.PartialOrd.html#method.gt + // https://doc.rust-lang.org/1.93.0/std/primitive.usize.html#impl-PartialOrd-for-usize + // [29] https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/lib.rs#L255-L278 + // https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/arbitrary.rs#L32-L65 + // [30] https://doc.rust-lang.org/1.93.0/reference/types/boolean.html#logical-not + // https://doc.rust-lang.org/1.93.0/std/macro.assert.html + // [31] https://github.com/model-checking/kani/blob/kani-0.67.0/library/std/src/lib.rs#L19-L45 + // [32] https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/lib.rs#L228-L253 + // [33] https://doc.rust-lang.org/1.93.0/reference/expressions/literal-expr.html#r-expr.literal.int.suffix + // https://doc.rust-lang.org/1.93.0/reference/expressions/literal-expr.html#r-expr.literal.int.representation + // [34] Rust 1.93 specifies that local paths, dereferences, and field + // expressions are place expressions representing memory locations; that a + // field expression denotes its field's location and automatically + // dereferences its container as needed (`&mut T` implements `Deref` and + // `DerefMut` to `T`); that `&mut` applied to a place produces a reference to + // that location, which is borrowed for the reference's duration and may not + // otherwise be accessed until the mutable borrow expires; and that built-in + // `*` applied to a mutable reference denotes an assignable pointed-to + // location: + // https://doc.rust-lang.org/1.93.0/reference/expressions.html#r-expr.place-value.place-memory-location + // https://doc.rust-lang.org/1.93.0/reference/expressions.html#r-expr.place-value.place-expr-kinds + // https://doc.rust-lang.org/1.93.0/reference/expressions/field-expr.html#r-expr.field.intro + // https://doc.rust-lang.org/1.93.0/reference/expressions/field-expr.html#r-expr.field.autoref-deref + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#r-expr.operator.borrow.result + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#r-expr.operator.borrow.lifetime + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#r-expr.operator.borrow.mut + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#r-expr.deref.result + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#r-expr.deref.mut + // https://doc.rust-lang.org/1.93.0/std/ops/trait.Deref.html#impl-Deref-for-%26mut+T + // https://doc.rust-lang.org/1.93.0/std/ops/trait.DerefMut.html#impl-DerefMut-for-%26mut+T + // [35] Rust evaluates expression operands before the containing expression + // and left-to-right, tuple-expression fields are its operands in order, + // tuple patterns destructure tuple fields positionally, and identifier + // patterns bind their matched values: + // https://doc.rust-lang.org/1.93.0/reference/expressions.html#r-expr.operand-order.operands-before-primary + // https://doc.rust-lang.org/1.93.0/reference/expressions/tuple-expr.html#r-expr.tuple.fields + // https://doc.rust-lang.org/1.93.0/reference/patterns.html#r-patterns.tuple.intro + // https://doc.rust-lang.org/1.93.0/reference/patterns.html#r-patterns.ident.intro + // [36] Kani 0.67's raw-any function carries `AnyRawHook`; the pinned hook + // table maps that marker to `Nondet`, which assigns a nondeterministic + // expression of the destination type: + // https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/lib.rs#L345-L367 + // https://github.com/model-checking/kani/blob/kani-0.67.0/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs#L334-L375 + // https://github.com/model-checking/kani/blob/kani-0.67.0/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs#L1034-L1044 + // https://github.com/model-checking/kani/blob/kani-0.67.0/cprover_bindings/src/goto_program/expr.rs#L766-L769 + // [37] Kani 0.67 pins CBMC 6.8.0. CBMC's model permits nondeterministic + // choices and says separate calls can return different results: + // https://github.com/model-checking/kani/blob/kani-0.67.0/kani-dependencies#L1-L3 + // https://github.com/diffblue/cbmc/blob/cbmc-6.8.0/doc/cprover-manual/modeling-nondeterminism.md#L7-L13 + // https://github.com/diffblue/cbmc/blob/cbmc-6.8.0/doc/cprover-manual/modeling-nondeterminism.md#L46-L59 + // [38] Rust 1.93 specifies that a non-`move` closure infers captures while + // preferring shared references; capture modes borrow or move environmental + // places; local paths are place expressions; evaluating a place in value + // context obtains its stored value and copies it for `Copy` types; and + // `u8` implements `Copy`: + // https://doc.rust-lang.org/1.93.0/reference/expressions/closure-expr.html#r-expr.closure.capture-inference + // https://doc.rust-lang.org/1.93.0/reference/types/closure.html#capture-modes + // https://doc.rust-lang.org/1.93.0/reference/types/closure.html#copy-values + // https://doc.rust-lang.org/1.93.0/reference/expressions/path-expr.html#r-expr.path.place + // https://doc.rust-lang.org/1.93.0/reference/expressions.html#r-expr.move.intro + // https://doc.rust-lang.org/1.93.0/reference/expressions.html#r-expr.move.copy + // https://doc.rust-lang.org/1.93.0/std/primitive.u8.html#impl-Copy-for-u8 + // [39] Rust 1.93 specifies that `&&` is logical AND and evaluates its right + // operand only when its left operand is true: + // https://doc.rust-lang.org/1.93.0/reference/expressions/operator-expr.html#lazy-boolean-operators + #[repr(transparent)] + struct Byte(u8); + + #[repr(C)] + struct DropTracked<'a> { + value: u8, + drops: &'a mut u8, + } + + // `repr(C)` and the alignment-one `Unalign` field make `value` begin at + // byte offset one. The zero-length array contributes no bytes but gives the + // backing object `T`'s alignment. See the family proof above. + #[repr(C)] + struct Misaligned { + _prefix: u8, + value: Unalign, + _align: [T; 0], + } + + impl Misaligned { + fn new(value: T) -> Self { + Self { _prefix: 0, value: Unalign(value), _align: [] } + } + } + + impl Drop for DropTracked<'_> { + fn drop(&mut self) { + *self.drops += 1u8; + } + } + + fn any_unalign_update_values() -> (u8, u8, u8) { + (kani::any::(), kani::any::(), kani::any::()) + } + + fn cover_unalign_update_byte_partitions(old: u8, new: u8, result: u8) { + kani::cover!(old == new); + kani::cover!(old != new); + kani::cover!(result == old); + kani::cover!(result != old); + kani::cover!(result == new); + kani::cover!(result != new); + kani::cover!(result != old && result != new); + } + + #[kani::proof] + #[kani::unwind(1)] + fn prove_unalign_update_alignment_one() { + assert_same_usize(mem::size_of::(), 1usize); + assert_same_usize(mem::size_of::>(), 1usize); + assert_same_usize(mem::align_of::(), 1usize); + let (old, new, result) = any_unalign_update_values(); + let mut value = Unalign(Byte(old)); + + let returned = value.update(|value| { + assert_eq!(value.0, old); + value.0 = new; + result + }); + + assert_eq!(returned, result); + // Destructuring is a language operation independent of `into_inner`, + // which exercises the same representation-sensitive path as `update`. + let Unalign(restored) = value; + assert_eq!(restored.0, new); + cover_unalign_update_byte_partitions(old, new, result); + } + + #[kani::proof] + #[kani::unwind(1)] + fn prove_unalign_update_write_back() { + assert_same_usize(mem::size_of::>(), 16usize); + assert_same_usize(mem::size_of::>>(), 16usize); + assert_same_usize(mem::size_of::>>(), 24usize); + assert!(mem::align_of::>() > 1usize); + let (old, new, result) = any_unalign_update_values(); + let mut drops = 0u8; + + { + let mut backing = Misaligned::new(DropTracked { value: old, drops: &mut drops }); + assert_same_usize(core::mem::offset_of!(Misaligned>, value), 1usize); + assert_same_usize(core::mem::offset_of!(Unalign>, 0), 0usize); + assert_same_usize( + mem::align_of::>>(), + mem::align_of::>(), + ); + let receiver = ptr::addr_of!(backing.value.0); + assert!(!receiver.is_aligned()); + kani::cover!(!receiver.is_aligned(), "write-back receiver is physically misaligned"); + + let returned = backing.value.update(|value| { + assert_eq!(value.value, old); + value.value = new; + result + }); + + assert_eq!(returned, result); + // Use pattern matching as the independent observation of the + // packed wrapper's field instead of calling `into_inner`. + let Unalign(restored) = backing.value; + assert_eq!(restored.value, new); + drop(restored); + } + + // After the restored value is observed, its destructor runs exactly + // once before this scope exits. + assert_eq!(drops, 1u8); + cover_unalign_update_byte_partitions(old, new, result); + } +} + #[cfg(test)] mod tests { use core::panic::AssertUnwindSafe;