Claim #1 — Verification of block_padding::PaddedData::unwrap (with kani 0.68.0)
block_padding::PaddedData::unwrap
Tool: kani 0.68.0
Preconditions
(BlockSize :: USIZE == 16 && matches ! (& self , PaddedData :: Pad { blocks , .. } if blocks . len () <= 2))
Evidence
What is trusted
From the report
The results depend on Kani and CBMC translation and models, the Rust compiler and standard-library models, and the solver. The checked instance uses the actual locked hybrid-array dependency without a replacement array shim. The original release implementation bodies are retained; Kani-only contract attributes and a verification-only module add the harnesses and specifications.
Technical limitations
From the report
These are bounded checks for U16, not claims for other block sizes, longer inputs, arbitrary downstream Padding implementations, or the whole dependency. The unwrap contract excludes NoPad and Error. The typed pad checks use valid positions and do not establish invalid-position behavior. The count-byte raw decoders' empty and oversized inputs are outside these typed checks. The checks do not establish all Rust undefined-behavior obligations or cryptographic security. Native tests are separate from Kani verification.
Tool limitations
Verification is scoped to the selected harnesses, assumptions, concrete types, target architecture, and any stubs or models used. Kani does not detect every form of Rust undefined behavior. In particular, data races and violations of reference aliasing rules are not fully checked. Uninitialized-memory checks require experimental support. Concurrent execution and panic stack unwinding are not modeled. A successful run should not be interpreted as excluding all Rust UB. References: https://model-checking.github.io/kani/undefined-behaviour.html https://model-checking.github.io/kani/rust-feature-support.html