Claim #14 — Verification of <i8 as bit_field::BitField>::set_bit (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)
<i8 as bit_field::BitField>::set_bit
Tool: Aeneas be86ab0f1989d04944292b345b24c435be3ad10a
Preconditions
Arbitrary integer, index, and (for set_bit) boolean on x86_64/default/debug. Supported non-monomorphizing extraction uses Lean-only PrimitiveRustLayout implicit evidence at twelve statically resolved ground primitive calls, with the same byte sizes independently checked by Kani. The class is open; only the supplied instances and frozen call closure are covered. Pointer-sized theorems assume a 64-bit platform.
Evidence
What is trusted
From the report
The official Rust/Charon/Aeneas translation and integer/slice models, Lean, and Kani/CBMC are trusted. The size_of model uses Lean-only PrimitiveRustLayout evidence with twelve supplied primitive instances, including pointer size8 on x86_64. The original generated Funs is unchanged: each of its twelve ground calls statically elaborates to the expected instance dictionary, checked explicitly. This added implicit evidence is not a Rust trait or an in-Lean proof of std layout. The Lean class remains extensible; coverage is the frozen twelve-call closure, not class sealing. Bool lacks an instance in the audited environment, and there is no supplied fallback for arbitrary types. Kani checks the same twelve actual layouts and all primitive single-bit/returned-reference behavior for arbitrary valid values. Connecting Kani Rust and Lean representations is a reviewed bridge, not an in-Lean std layout proof; Rust nightlies differ. Generic slice theorems assume the complete stated observation/update callback contracts, including the final state after returned-reference writeback. They do not prove arbitrary callback implementations. Mapped audits allow only propext, Classical.choice and Quot.sound. The RangeFull supplement executes original public methods and actual std size_of under Kani0.68/CBMC6.11/nightly2026-08-21, default debug x86_64 with64-bit usize/isize. Its compiler, standard and validity/panic semantics are trusted; no source adaptation, model, stub or suppressed UB check is introduced. It is independent of the Lean-only layout evidence and supplies no formal cross-tool equivalence. The standard-range supplements use the same official compiler/Charon/Aeneas toolchain with original bodies inlined into actual UFCS callers. Their original generated and primitive layout provider bytes remain fixed. Each width is elaborated in its own Lean process and module environment, sharing only the pinned official dependency sources/artifacts. Every audit checks theorem declarations and transitive axioms against propext, Classical.choice and Quot.sound. The usize getter additionally assumes the Lean platform width is64, matching the recorded x86_64 Rust target; this is an explicit configuration premise, not an added axiom or proof about every platform.
Technical limitations
From the report
The registered primary contracts cover twenty-four primitive single-bit methods, twelve width constants and three callback-conditional slice bodies. General primitive and slice get_bits/set_bits range contracts beyond the scoped specializations described below remain unproved; the separate RangeFull-only Kani results described here cover closed primitive specializations. A separately Kani-checked example shows signed range behavior differs from ordinary masked updates: 112_i8.set_bits(0..4,1) yields 1, changing high bits outside the range; the unsigned example yields 113. The verified single-bit methods are unaffected. Generic callback side effects, failure/divergence outside the stated contracts, other targets and release extraction are not established. No generic Rust size_of property, panic text or unwinding-state guarantee is claimed. Signed-range diagnostic evidence: https://github.com/nyuichi/rust-crate-proofs/tree/57c4d16e1184f84353db90589bc3cb601f89cb85/batches/2026-11-05-full-public-api/diagnostics/bit-field-signed-range RangeFull denotes the whole primitive word and has no outside bits to preserve; these checks do not imply masked-update behavior for other signed intervals. Arbitrary RangeBounds implementations, bounds callbacks, other interval specializations, slice BitArray methods, invalid-range panic payload/unwind behavior, other targets or release configuration are not established. The separate signed small-range counterexample remains valid. All27 registered model contracts and their preconditions remain unchanged. The standard-range results concern only these unsigned Range<usize> specializations under the recorded checked/default debug configuration; arbitrary RangeBounds callbacks, signed intervals, other targets and all-input unchecked-release behavior remain outside them. Independent Kani138-check normal-case observations for each of u8 and u16 are distinct from the Lean exhaustive failure proofs; u32/u64/u128/usize add no new Kani run. The usize setter remains blocked by an emitted maximum-usize literal and the official conservative literal bound; no model, literal or IR change is used to bypass it. Global generated Bound-instance collisions prevent a simultaneous import with the primary27 environment, so the six workspaces are checked separately without a nominal-type/model bridge. Result failure and backward-function contracts do not establish Rust panic payloads, unwinding, physical aliasing/heap semantics or arbitrary side effects. The existing signed small-range counterexample and RangeFull24 limits remain in force; generic RangeBounds completion and whole-crate completion are not claimed.
Tool limitations
Lean backend only, requiring cargo-proofs 0.4.0 or later. The version identifies the official Aeneas Git revision pinned in lake-manifest.json (backends/lean); this revision uses Lean 4.35.0. The recorder checks committed Lean theorem declarations and permits only propext, Classical.choice, and Quot.sound as transitive axioms. It rejects sorryAx and custom axioms, including axiomatized external models. Charon/Aeneas extraction is not rerun. The author must review that the committed functional model matches the recorded Rust source, that the named theorem corresponds to the public API, and that the reported precondition matches the theorem. A checked theorem alone does not establish those links or the adequacy of the specification. The current adapter records the default Cargo configuration, with ordinary Lean module paths and a pinned official Git dependency. Other backends, custom Lake source directories, and local-path Aeneas dependencies are unsupported. See https://proofs.rs/book/aeneas.html and https://github.com/AeneasVerif/aeneas/tree/be86ab0f1989d04944292b345b24c435be3ad10a.
Aeneas be86ab0f1989d04944292b345b24c435be3ad10a — version details