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.
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 next_u64 correctness, fill_bytes, external-RNG initialization, formatting, inherited Rng wrappers and serde remain unverified. 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.
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