Claim #1 — Verification of <rand_xorshift::XorShiftRng as TryRng>::try_next_u32 (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)
<rand_xorshift::XorShiftRng as TryRng>::try_next_u32
impl TryRng for XorShiftRng
pub fn try_next_u32(self: &mut Self) -> Result<u32, <Self as rand_core::TryRng>::Error>Tool: Aeneas be86ab0f1989d04944292b345b24c435be3ad10a
Preconditions
Any four-u32 internal state, including all zero; three explicit std Wrapping operator models are used and independently checked with Kani.
Evidence
What is trusted
From the report
The Rust compiler, Charon/Aeneas translation, existing Aeneas scalar primitives, Lean kernel, and Kani/CBMC toolchains are trusted. Three executable std Wrapping<u32> models connect shift-left, shift-right, and xor to existing Aeneas primitives. Kani checks their Rust correspondence for all u32 operands and all 64-bit usize shift amounts; the relation between these Rust formulas and the Lean definitions remains an explicitly reviewed semantic bridge, not an in-Lean proof of the std bodies. No extra local axiom occurs in the public theorem's transitive dependencies. The seed and preservation harnesses embed the entire original Rust implementation as an unchanged prefix, appending safe observers in a std verification module. This preserves the implementation text but retains the documented verification-module and compiler/toolchain boundary. The separate Nonzero.lean proof uses the existing Aeneas exact transition theorem, not an assumed new seed theorem. This Serialize supplement trusts Kani/CBMC, the August Rust compiler and the exact rand_core 0.10.0 / serde 1.0.228 implementations; its finite callback serializer is the observed protocol, not an assumption about arbitrary serializers. The Deserialize supplement additionally uses the concrete sequence access, DeserializeSeed and u32 visitor implementations with the same pinned Kani/Rust/serde dependencies. Its invalid_length handler returns the specified concrete error. The scalar-wrapper supplements additionally trust the exact rand_core0.10.0 and, for the wire domain, serde1.0.228 code with the recorded Kani0.68/CBMC6.11 and August Rust/std binaries. Successful CaDiCaL runs are distinguished from preserved unsuccessful Z3 translation diagnostics. The public-seed and concrete-Deserialize construction paths are executed unchanged; state equality uses the original derived Eq. No private observer, custom semantic model or adapted original Rust is introduced. The reflexive caller supplement uses official nightly2026-09-17 compiler/Charon/Aeneas and the corresponding standard library, with unchanged original Rust, generated output and models. Its compiler provenance addendum directly hashes and invokes the actual rustc binary with successful version/sysroot capture. The frozen earlier TOOL-PINS rustup-multiplexer version/exit-6 is a historical capture error, not a successful rustc pin. Matching configured toolchain evidence does not retroactively attest the process used by an earlier run.
Technical limitations
From the report
The single Aeneas API mapping remains try_next_u32 on x86_64 without serde. from_seed and original nonzero-state preservation are independent Kani body checks. Aeneas extraction of the original seed body remains blocked by mutable zip iteration. Kani uses Rust nightly-2026-08-21 while Aeneas extraction uses nightly-2026-09-17; these are not mechanically linked proofs of one toolchain's std bodies. The three wrapping models retain their reviewed Rust-to-Lean bridge. The all-zero state is still covered by the exact step theorem; the initial-nonzero guarantee is for from_seed, not every unverified initialization or serialization path. General-state numeric next_u64 correctness and unrestricted fill_bytes, external-RNG initialization, formatting, inherited Rng wrappers and serde behavior remain unverified beyond the scoped supplements below. No period, distribution or cryptographic property is established. The separate try_next_u64 composition check covers only states constructed from_seed under default features and rand_core0.10.0. Arbitrary Rust-valid all-zero internal states, serde states, other histories, independent mathematical output formulas and a formal Rust-to-Lean bridge remain outside that check. This Debug result is limited to these public constructor images, default format flags and the fixed accepting-or-first-error writer; arbitrary Formatter states, partial-prefix errors, general writers and arbitrary private states are not established. The fill supplement covers only lengths0..8 in an8-byte allocation and states from public from_seed; arbitrary lengths/allocations, serde and arbitrary private states remain unproved. A separate0..64 attempt timed out and supplies no completed guarantee. This is an original public-API relation, not an independent recurrence proof or Rust-to-Lean equivalence. Source-based initialization is checked only for these concrete TryRng implementations and zero-or-one preliminary-zero protocol. It does not establish arbitrary source behavior, unbounded zero retries, unconditional termination, generic callback effects or serde behavior. Equality with from_seed is a relational result, not literal delegation or an independent seed-decoding specification. Serialize is checked only for the fixed callback protocol and states produced by public from_seed, not arbitrary Serializer implementations, arbitrary private states, Deserialize or other encodings. The separate Kani result adds no Aeneas machine claim. Deserialize is checked only for this sequence protocol, lengths0..4, nine callback error stages and a successful fixed-serializer roundtrip. Arbitrary Deserializer implementations, map-based or other formats and general serialization roundtrip correctness are not established. Deserialized zero state is included; this result does not establish the nonzero state invariant for all deserialized values. External Rng scalar delegation is established only for these two construction domains/configurations and exact pinned implementations; arbitrary Deserializer callbacks, map/other formats, unrelated rand_core versions, trait dictionaries, allocation/aliasing behavior and other wrapper methods are not implied. Source reasoning that16-byte wires represent all four-u32 tuples is documented separately and is not an independent kernel representation theorem. The seed-image domain excludes arbitrary zero/private/serde states, while the concrete wire domain includes zero; the two must not be conflated. Preserved pending statements in STATE-DOMAIN and PREPARED are historical and are superseded by final656-check STATUS/raw logs. Packaging path relocation was not rerun. The actual-call relation does not establish an independent recurrence formula, period, distribution or an Aeneas-to-Kani compiler bridge. seed_from_u64 remains unverified; its solver and MIR-only diagnostic failures add no guarantee. Reflexive identities use the extracted four-word logical value and backward-function semantics; physical pointer identity, arbitrary aliasing/heap/provenance, Drop/global effects and general Rust memory safety are not established. The primary transition representation and the reflexive generated type remain distinct; importing both in one package does not supply a nominal type/model bridge or rerun a Rust-to-Lean equivalence proof. In the reflexive packet, reachable/generated opaque-function count is0 and all three bodies have zero runtime calls; whole LLBC still has22 declarations, comprising3 transparent bodies and19 unused opaque builtins. No claim that the whole LLBC has no opaque declarations is made. The corrected compiler capture and raw historical metadata are both preserved. Primary1, the three wrapping models and all prior Kani domains/limits 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