Claim #12 — Verification of oorandom::Rand64::new (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)
impl Rand64
pub fn new(seed: u128) -> SelfTool: Aeneas be86ab0f1989d04944292b345b24c435be3ad10a
Preconditions
All well-typed scalar seeds, states and increments; default feature set on x86_64. No odd-increment or nonzero-state precondition.
Evidence
What is trusted
From the report
The Rust compiler, official Charon/Aeneas translation, official scalar models and Lean kernel are trusted. Wrapping, casts, shifts and rotations in the primary proofs use official models, not Rust std body proofs. Range proofs instead include the original std wrapping_neg bodies transparently, with no new provider or model. Lean dependency audits permit only propext, Classical.choice and Quot.sound.
The four supplemental Into/TryInto body specializations additionally trust a default-off finite export patch that emits exactly the original transparent core bodies and omits duplicate rust_fun registrations. It changes no body, type, callback or Std model. Original source/LLBC, patch/binary hashes, default-off comparison and enabled export guards are retained; no general translator equivalence is established.
Kani results trust Kani/CBMC, the pinned August Rust compiler and solver semantics. Float composition uses the identical Rust helper across two universal specifications; no general Aeneas floating-point model or mechanized cross-tool equivalence is asserted. Exact compiler-commit standard sources show Any uses a TypeId intrinsic. Sized CloneToUninit has a clone/write default and a TrivialClone nonoverlapping-copy specialization, which may apply to these Clone+Copy types; the fixed-slot result does not prove arbitrary pointer validity or a particular dispatch route.
Technical limitations
From the report
Twenty machine-readable claims cover fourteen original local APIs and six conditional external core conversion families. These six are not local declarations. Kani results remain separate supplements; this is not full crate completion. All apply only in their recorded target/configuration and tool boundaries.
Range proofs identify the exact sample and final state conditional on a finite first accepted candidate, and divergence for an all-rejected trace. They do not establish an accepted index exists for every state/range, general termination, uniformity, period or expected runtime. Debug assertion failure does not specify release behavior or Rust panic/unwinding effects. Save/restore is pure state identity, not a guarantee about arbitrary callbacks or destructors. No period, distribution, independence or cryptographic guarantee is established.
The external Kani checks do not prove global TypeId uniqueness, arbitrary CloneToUninit destinations or heap behavior: extent, alignment, nonoverlap and provenance obligations remain with the caller. Generic conversion contracts require actual trait instances and matching modeled dictionaries, preserve the selected associated error type, and do not establish arbitrary U has an instance. Callback correctness/termination, Drop/unwind/global effects, physical aliasing/layout, resource availability and const evaluation remain outside those contracts. The six generic families use a finite compiler-owned source/body binding; arbitrary trait instances, implementations or configurations are not inferred.
Earlier direct combined float attempts timed out and are retained. The later Rand32 direct Z3 check succeeds; Rand64 direct Z3 still times out, while its successful two-stage composition establishes the stated contract. Other targets/configurations were not checked.
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