Claim #10 — Verification of <u128 as bit_field::BitField>::set_bit (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)
<u128 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.
Technical limitations
From the report
Only twenty-four primitive single-bit methods, twelve width constants and three callback-conditional slice bodies are established. General primitive and slice get_bits/set_bits range contracts 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, general intervals, 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.
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