Report #24 — Exact next-word updates and separately checked seed/nonzero properties

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

1 verified claim · 0 findings

Recorded by the author; proofs.rs has not re-run it. How to read a report

nyuichi · 2026-11-05 00:34 UTC

Revision v7 · v6 · v5 · v4 · v3 · v2 · v1

Overview

For rand_xorshift 0.5.0, the Aeneas proof establishes the exact try_next_u32 word and state update for every four-u32 state, using three explicit std wrapping-operator models. With t=x XOR (x << 11), r=w XOR (w >> 19) XOR t XOR (t >> 8); the returned value is Ok(r) and state becomes (y,z,w,r), using 32-bit logical operations. A separate Lean theorem derives preservation of a nonzero state from this exact transition. Independently, Kani checks the unchanged from_seed body for every 16-byte seed: four little-endian u32 words are decoded, and the all-zero input is replaced by four 0x0BAD5EED words. The constructed state is nonzero. A second Kani harness checks that the original next_u32 body preserves every nonzero four-word state. These seed and preservation checks are supplementary Kani results, not an Aeneas seed-body claim. No original Rust source or manifest is changed. A further original-source Kani check covers every 16-byte seed, including the zero-seed fallback: from_seed followed by try_next_u64 returns the same little-endian low/high word composition as two try_next_u32 calls on an identical clone, and derived equality confirms every resulting state word agrees. This is a public-API relational guarantee over seed-constructed states, not an independent recurrence specification. Separate Kani also executes the original manual Debug formatter for every public from_seed input or seed_from_u64 input. With default formatting and a fixed64-byte writer it emits exactly "XorShiftRng {}" (13bytes), preserves the zero suffix and correct length; a writer rejecting the first write instead propagates fmt::Error with no bytes retained. A separate original try_fill_bytes relation is checked for every16-byte seed, every initial8-byte array and every requested prefix length0..8. Filling returns Ok, writes exactly the little-endian prefix from ceil(length/4) actual next32 calls, preserves the unused array suffix and yields an equal complete final generator state. Separate original from_rng/try_from_rng Kani relations cover concrete source protocols: every nonzero16-byte seed, optionally preceded by one all-zero block, produces the same complete state as public from_seed after exactly1or2 source fills. Fallible sources additionally propagate every u32 error payload after zero or one discarded zero block, preserving the expected call count even if the failing fill first writes arbitrary bytes. With the serde feature, a separate Kani check calls original Serialize for every public 16-byte seed through a fixed serializer: it emits the XorShiftRng struct with x/y/z/w u32 fields in order, matching little-endian seed words with the documented all-zero fallback, and leaves the RNG state unchanged. A failure at any of its ten serializer callback stages propagates the exact supplied u32 error and stops at that stage. A separate Kani check calls original Deserialize through a fixed sequence deserializer for every 16-byte wire value and lengths zero through four. Lengths below four return the concrete invalid_length error for that length; a supplied error at any reached callback stage propagates unchanged. Successful four-word deserialization, including all-zero state, serializes through the fixed serializer to the exact original 16 bytes and leaves that state unchanged.

Findings (0)

No findings reported.

APIs (1)

Trait implementations

`impl rand_core::TryRng for XorShiftRng`

pub fn try_next_u32(self: &mut Self) -> Result<u32, <Self as rand_core::TryRng>::Error>

Claim #1

Evidence

https://github.com/nyuichi/rust-crate-proofs/tree/ad4098c79bb4e8fe7d8d0ba3a63beffe184d5aef

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/nyuichi/rust-crate-proofs report-24-source-1
git -C report-24-source-1 checkout --detach ad4098c79bb4e8fe7d8d0ba3a63beffe184d5aef
git -C report-24-source-1 submodule update --init --recursive --checkout
cd report-24-source-1/rand_xorshift/0.5.0/aeneas/2026-11-05/proofs

lake build +Proofs

printf '%s' 'import Lean
import Proofs
open Lean Elab Command

run_cmd do
  let theorem_name := `Proofs.try_next_u32_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.try_next_u32_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.try_next_u32_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.try_next_u32_spec"
' | lake env lean --stdin

Checks out the recorded source commit from GitHub. Install the report’s tool version before running.

Source on GitHub · SARIF with logs (.json)

Recorded run

Completed · 1 checks passed · 0 failed

2026-11-05T11:39:08.594217588+00:00 · 88.5 seconds · Exit code 0

Recorded on the author’s machine.

Check	Result	Claim
Lean checked theorem Proofs.try_next_u32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.try_next_u32_spec`	Passed	Claim #1

Execution details

Started: 2026-11-05T11:39:08.594217588+00:00
Finished: 2026-11-05T11:40:37.111701944+00:00
Platform: linux x86_64
Rust compiler: rustc 1.100.0-nightly (923c95cdf 2026-09-16) binary: rustc commit-hash: 923c95cdf5ba65cea505aa2ea829f578e1506ed8 commit-date: 2026-09-16 host: x86_64-unknown-linux-gnu release: 1.100.0-nightly LLVM version: 23.1.1
Working directory: rand_xorshift/0.5.0/aeneas/2026-11-05/proofs
Environment overrides: None recorded
Git repository: https://github.com/nyuichi/rust-crate-proofs
Git commit: ad4098c79bb4e8fe7d8d0ba3a63beffe184d5aef

Diagnostics & logs

=== stdout ===
⚠ [2/57] Ran aeneas:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
✔ [3/176] Built AeneasMeta.Simp.RegisterCommand (38s)
✔ [121/496] Built Aeneas.Std.Global (38s)
✔ [122/496] Built AeneasMeta.BvEnumToBitVec (38s)
✔ [445/846] Built AeneasMeta.UtilsCore (38s)
✔ [1575/1800] Built AeneasMeta.OptionConfig (39s)
✔ [1797/1800] Built RandXorshift.Types (1.4s)
✔ [1798/1800] Built RandXorshift.FunsExternal (1.5s)
✔ [1799/1800] Built RandXorshift.Funs (1.6s)
ℹ [1800/1800] Built Proofs (2.1s)
info: Proofs.lean:32:0: 'Proofs.try_next_u32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
Build completed successfully (1800 jobs).

$ lake env lean --stdin (proofs.rs theorem/axiom audit)
proofs.rs:checked:Proofs.try_next_u32_spec

=== stderr ===
info: aeneas: materializing new dependency
info: aeneas: fetching revision 'be86ab0f1989d04944292b345b24c435be3ad10a' from https://github.com/AeneasVerif/aeneas
info: aeneas: checking out revision 'be86ab0f1989d04944292b345b24c435be3ad10a'
info: mathlib: materializing new dependency
info: mathlib: fetching revision '56a005855ea17e0b0958f73ec801ae140b0a1679' from https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '56a005855ea17e0b0958f73ec801ae140b0a1679'
info: plausible: materializing new dependency
info: plausible: fetching revision 'dfa4f38190d07c37e315953e08b90fe2d95b3c24' from https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'dfa4f38190d07c37e315953e08b90fe2d95b3c24'
info: LeanSearchClient: materializing new dependency
info: LeanSearchClient: fetching revision 'd6b4c7be5be75ec4917c873ac50c756dc1436372' from https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'd6b4c7be5be75ec4917c873ac50c756dc1436372'
info: importGraph: materializing new dependency
info: importGraph: fetching revision 'a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93' from https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93'
info: proofwidgets: materializing new dependency
info: proofwidgets: fetching revision 'df72b022e558978a1c50264cfc4d7fec86fa8e04' from https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'df72b022e558978a1c50264cfc4d7fec86fa8e04'
info: aesop: materializing new dependency
info: aesop: fetching revision '4a174c490d8707121c4a9290800489f105d85e07' from https://github.com/leanprover-community/aesop
info: aesop: checking out revision '4a174c490d8707121c4a9290800489f105d85e07'
info: Qq: materializing new dependency
info: Qq: fetching revision 'dce0ad79c486cb1fb504af04f953c3466b0c6db8' from https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'dce0ad79c486cb1fb504af04f953c3466b0c6db8'
info: batteries: materializing new dependency
info: batteries: fetching revision '66e469188fe07963e5cf666c7d4433f45b8131c5' from https://github.com/leanprover-community/batteries
info: batteries: checking out revision '66e469188fe07963e5cf666c7d4433f45b8131c5'
info: Cli: materializing new dependency
info: Cli: fetching revision 'c24fe6078c630e89b489bffe59b3e20ac30d12c8' from https://github.com/leanprover/lean4-cli
info: Cli: checking out revision 'c24fe6078c630e89b489bffe59b3e20ac30d12c8'

Environment

Original crates.io rand_xorshift 0.5.0; Rust nightly-2026-09-17; Charon 08d7c9d50144bd84848212c24701253585e90d1f; official Aeneas frontend/library be86ab0f1989d04944292b345b24c435be3ad10a; Lean 4.35.0. Official start-from and split-files options select the original body and three external operators. Kani 0.68.0 / CBMC 6.11.0 / Rust nightly-2026-08-21 provide the supplementary checks detailed below. The Lean theorem audit allows only propext, Classical.choice, and Quot.sound. cargo-proofs 0.4.1 uses the documented CA-trust, upstream audit-variable, and exact rand_core::TryRng catalogue-alias compatibility fixes without changing the allowed-axiom policy. Supplementary seed/nonzero Kani run: 2 harnesses, 327 checks, zero failures (237 seed plus 90 preservation), with unwind 20 and unwinding assertions enabled. All 128 seed bits and all nonzero four-word states are quantified. Nonzero.lean is independently built/audited with only the standard three axioms; it is supplementary to the unchanged single machine API mapping. See SEED-VERIFICATION.md and evidence/kani-seed for exact source-prefix hashes and verification-module provenance. Additional public composition supplement: ordinary Kani harness,294 checks/0fail/5unreachable, original11 archive files and actual rand_core0.10.0 19files authenticated, no observer/model; evidence/kani-public-composition. Additional original Debug Kani supplement:2217checks/0fail/133unreachable, default/core0.10.0/nightly2026-08-21; evidence/kani-debug. Ordinary Kani supplement; the single Aeneas mapping is unchanged. Further original fill8 Kani supplement:379checks/0fail/5unreachable, unwind20, default/rand_core0.10.0/nightly2026-08-21; evidence/kani-fill8. Aeneascount1 remains unchanged. Further original source-initialization Kani supplement:3harnesses/675checks/0fail/30unreachable, unwind20/default/rand_core0.10.0/nightly2026-08-21; evidence/kani-rng-init. One Aeneas mapping remains unchanged. Separate original Serialize Kani0.68/nightly2026-08-21: default+serde, rand_core0.10.0/serde1.0.228, one harness536checks/0fail/5unreachable; evidence/kani-serialize. Dependency path adapted only for portable artifact layout. Separate Deserialize Kani0.68/nightly2026-08-21: default+serde/core0.10.0/serde1.0.228, one harness600checks/0fail/1unreachable; evidence/kani-deserialize. Portable manifest dependency path only; prior Serialize536 and all other supplements retained.

What is trusted

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

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.

Updated 2026-10-16 00:00 UTC

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a — version details

Dependencies (3)

CrateReports

postcard ^1.1.3 · dev—

rand_core ^0.10.0—

serde ^1.0.118 · optional—

Comments (0)

No comments.