Report #29 — Exact PCG state, output and advance for all four generator types

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

25 verified claims · 0 findings

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

nyuichi · 2026-11-05 04:56 UTC

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

Overview

For rand_pcg 0.10.2, the four state getters return their stored word. The three LCG stream getters return increment>>1; from_state preserves its input state and stores increment=(stream<<1) OR 1, discarding the highest stream bit. Their new constructors initialize state=((input_state+increment)multiplier+increment) with modular arithmetic; the multipliers are 6364136223846793005, 47026247687942121848144207491837523525 and 15750249268501108917 respectively. Mcg128Xsl64::new stores input_state OR 1. Native output proofs retain Lcg64Xsh32::try_next_u32 and both word widths for the three 128-bit types. The XSL-RR variants permute the newly advanced state; CM-DXSM permutes the old state then advances. Their 32-bit methods return the low 32 bits of the 64-bit result with the same final state. Original Result::map and conversion closures are body-extracted. Mcg128Xsl64::advance additionally terminates normally for every u128 delta and every internal u128 state, returning state=M^deltainitial_state modulo 2^128, M=47026247687942121848144207491837523525. A well-founded halving-loop proof connects the original body to this ordinary power specification, covering all deltas without an artificial execution bound. These twenty-five direct original-body API guarantees apply under default and serde because the selected official translations are byte-identical; the serde implementations themselves remain unproved. Each of the three LCG advance methods also terminates normally for every full-width delta, state and increment, preserving the stored increment and producing exactly delta repetitions of the ordinary modular affine step x↦M*x+increment. An independent linear recurrence specifies this behavior; a generic affine-composition proof connects the original binary algorithm to it. Increments need not be odd for this state-transform identity. Separate Kani evidence calls the unchanged Mcg128Xsl64::from_seed and public state getter for every sixteen-byte seed. Its state equals the independently decoded little-endian u128 seed OR 1 (242 successful checks under each of default and serde). The exact rand_core 0.10.0 and serde 1.0.228 dependency lock is retained. This is a separate Kani body guarantee, not another Aeneas machine claim or a formal cross-tool equivalence proof. Separately, four Kani harnesses call the original manual Debug implementations through all typed inputs of the listed new/from_state/from_seed/seed_from_u64 constructors. Under default formatting and a fixed 64-byte writer that accepts all bytes or rejects the first write, they emit the fixed redacted type-name literal and propagate the writer error. All four baseline rand_core0.10.0 jobs complete with 8925 checks and no failures. For Lcg64Xsh32 with serde, a separate Kani check decodes every 16-byte wire value through a fixed sequence deserializer, including zero and even increments. For successful two-word decoding, public state() equals the first little-endian u64 and stream() equals the second u64 shifted right by one; successful concrete serialization reproduces all sixteen bytes, including the increment low bit, without changing the RNG. Short sequences of length0 or1 return the concrete invalid_length error, and errors at any reached one of five Deserialize callback stages propagate the supplied code. For Lcg128Xsl64 (Pcg64) with serde, another concrete sequence check covers every 32-byte wire value, including zero and even increments. Successful two-u128 decoding has public state() equal to the first little-endian u128 and stream() equal to the second shifted right by one; its successful serialization reproduces all32 bytes without changing state. Length0 or1 returns the concrete invalid_length error, and a supplied error at any reached one of five Deserialize callback stages propagates exactly. Separate original-Rust Kani evidence for Mcg128Xsl64 serde covers every 16-byte wire value, including zero/even states, through a fixed sequence protocol of length0..1. Successful decoding has public state equal to independent little-endian decoding; successful serialization reproduces the wire without state changes. Missing state returns the concrete invalid_length error and each reached one of three Deserialize callback errors propagates exactly. Actual Deserialize of zero yields state0, unlike new(state)|1; this is a configuration-specific observation, not a general RNG defect claim. Separate PCG32 composition checks establish actual try_next_u64 equals the little-endian combination of two successive actual try_next_u32 outputs, with equal complete final state, for all public from_state inputs. Eight concrete external rand_core::Rng next32/next64 calls across all four generators equal their actual TryRng calls in output and complete final state. The LCG domains are all public from_state state/stream inputs with odd increment; the MCG domain is all public new inputs with odd nonzero state.

Findings (0)

No findings reported.

APIs (25)

Recorded callables

<rand_pcg::Lcg128CmDxsm64 as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #20

<rand_pcg::Lcg128CmDxsm64 as TryRng>::try_next_u64 recorded callable · signature and safety not recorded

Claim #21

<rand_pcg::Lcg128Xsl64 as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #16

<rand_pcg::Lcg128Xsl64 as TryRng>::try_next_u64 recorded callable · signature and safety not recorded

Claim #17

<rand_pcg::Lcg64Xsh32 as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #1

<rand_pcg::Mcg128Xsl64 as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #18

<rand_pcg::Mcg128Xsl64 as TryRng>::try_next_u64 recorded callable · signature and safety not recorded

Claim #19

Lcg128CmDxsm64::advance recorded callable · signature and safety not recorded

Claim #25

Lcg128CmDxsm64::from_state recorded callable · signature and safety not recorded

Claim #12

Lcg128CmDxsm64::new recorded callable · signature and safety not recorded

Claim #13

Lcg128CmDxsm64::state recorded callable · signature and safety not recorded

Claim #10

Lcg128CmDxsm64::stream recorded callable · signature and safety not recorded

Claim #11

Lcg128Xsl64::advance recorded callable · signature and safety not recorded

Claim #24

Lcg128Xsl64::from_state recorded callable · signature and safety not recorded

Claim #8

Lcg128Xsl64::new recorded callable · signature and safety not recorded

Claim #9

Lcg128Xsl64::state recorded callable · signature and safety not recorded

Claim #6

Lcg128Xsl64::stream recorded callable · signature and safety not recorded

Claim #7

Lcg64Xsh32::advance recorded callable · signature and safety not recorded

Claim #23

Lcg64Xsh32::from_state recorded callable · signature and safety not recorded

Claim #4

Lcg64Xsh32::new recorded callable · signature and safety not recorded

Claim #5

Lcg64Xsh32::state recorded callable · signature and safety not recorded

Claim #2

Lcg64Xsh32::stream recorded callable · signature and safety not recorded

Claim #3

Mcg128Xsl64::advance recorded callable · signature and safety not recorded

Claim #22

Mcg128Xsl64::new recorded callable · signature and safety not recorded

Claim #15

Mcg128Xsl64::state recorded callable · signature and safety not recorded

Claim #14

Evidence

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

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/nyuichi/rust-crate-proofs report-29-source-1
git -C report-29-source-1 checkout --detach 3b2722d98fcb09ef58d010abf5a42361a4d094c5
git -C report-29-source-1 submodule update --init --recursive --checkout
cd report-29-source-1/rand_pcg/0.10.2/aeneas/2026-11-05/proofs

lake build +AdvanceProofs +AffineProofs +Proofs

printf '%s' 'import Lean
import AdvanceProofs
import AffineProofs
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"

run_cmd do
  let theorem_name := `Proofs.state_Lcg64Xsh32_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.state_Lcg64Xsh32_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.state_Lcg64Xsh32_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.state_Lcg64Xsh32_spec"

run_cmd do
  let theorem_name := `Proofs.stream_Lcg64Xsh32_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.stream_Lcg64Xsh32_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.stream_Lcg64Xsh32_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.stream_Lcg64Xsh32_spec"

run_cmd do
  let theorem_name := `Proofs.from_state_Lcg64Xsh32_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.from_state_Lcg64Xsh32_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.from_state_Lcg64Xsh32_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.from_state_Lcg64Xsh32_spec"

run_cmd do
  let theorem_name := `Proofs.new_Lcg64Xsh32_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.new_Lcg64Xsh32_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.new_Lcg64Xsh32_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.new_Lcg64Xsh32_spec"

run_cmd do
  let theorem_name := `Proofs.state_Lcg128Xsl64_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.state_Lcg128Xsl64_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.state_Lcg128Xsl64_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.state_Lcg128Xsl64_spec"

run_cmd do
  let theorem_name := `Proofs.stream_Lcg128Xsl64_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.stream_Lcg128Xsl64_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.stream_Lcg128Xsl64_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.stream_Lcg128Xsl64_spec"

run_cmd do
  let theorem_name := `Proofs.from_state_Lcg128Xsl64_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.from_state_Lcg128Xsl64_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.from_state_Lcg128Xsl64_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.from_state_Lcg128Xsl64_spec"

run_cmd do
  let theorem_name := `Proofs.new_Lcg128Xsl64_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.new_Lcg128Xsl64_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.new_Lcg128Xsl64_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.new_Lcg128Xsl64_spec"

run_cmd do
  let theorem_name := `Proofs.state_Lcg128CmDxsm64_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.state_Lcg128CmDxsm64_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.state_Lcg128CmDxsm64_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.state_Lcg128CmDxsm64_spec"

run_cmd do
  let theorem_name := `Proofs.stream_Lcg128CmDxsm64_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.stream_Lcg128CmDxsm64_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.stream_Lcg128CmDxsm64_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.stream_Lcg128CmDxsm64_spec"

run_cmd do
  let theorem_name := `Proofs.from_state_Lcg128CmDxsm64_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.from_state_Lcg128CmDxsm64_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.from_state_Lcg128CmDxsm64_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.from_state_Lcg128CmDxsm64_spec"

run_cmd do
  let theorem_name := `Proofs.new_Lcg128CmDxsm64_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.new_Lcg128CmDxsm64_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.new_Lcg128CmDxsm64_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.new_Lcg128CmDxsm64_spec"

run_cmd do
  let theorem_name := `Proofs.state_Mcg128Xsl64_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.state_Mcg128Xsl64_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.state_Mcg128Xsl64_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.state_Mcg128Xsl64_spec"

run_cmd do
  let theorem_name := `Proofs.new_Mcg128Xsl64_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.new_Mcg128Xsl64_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.new_Mcg128Xsl64_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.new_Mcg128Xsl64_spec"

run_cmd do
  let theorem_name := `Proofs.next32_Lcg128Xsl64_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.next32_Lcg128Xsl64_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.next32_Lcg128Xsl64_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.next32_Lcg128Xsl64_spec"

run_cmd do
  let theorem_name := `Proofs.next64_Lcg128Xsl64_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.next64_Lcg128Xsl64_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.next64_Lcg128Xsl64_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.next64_Lcg128Xsl64_spec"

run_cmd do
  let theorem_name := `Proofs.next32_Mcg128Xsl64_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.next32_Mcg128Xsl64_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.next32_Mcg128Xsl64_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.next32_Mcg128Xsl64_spec"

run_cmd do
  let theorem_name := `Proofs.next64_Mcg128Xsl64_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.next64_Mcg128Xsl64_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.next64_Mcg128Xsl64_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.next64_Mcg128Xsl64_spec"

run_cmd do
  let theorem_name := `Proofs.next32_Lcg128CmDxsm64_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.next32_Lcg128CmDxsm64_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.next32_Lcg128CmDxsm64_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.next32_Lcg128CmDxsm64_spec"

run_cmd do
  let theorem_name := `Proofs.next64_Lcg128CmDxsm64_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.next64_Lcg128CmDxsm64_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.next64_Lcg128CmDxsm64_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.next64_Lcg128CmDxsm64_spec"

run_cmd do
  let theorem_name := `AdvanceProofs.mcg_advance_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: AdvanceProofs.mcg_advance_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 AdvanceProofs.mcg_advance_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:AdvanceProofs.mcg_advance_spec"

run_cmd do
  let theorem_name := `AffineProofs.lcg64_advance_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: AffineProofs.lcg64_advance_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 AffineProofs.lcg64_advance_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:AffineProofs.lcg64_advance_spec"

run_cmd do
  let theorem_name := `AffineProofs.lcg128_advance_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: AffineProofs.lcg128_advance_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 AffineProofs.lcg128_advance_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:AffineProofs.lcg128_advance_spec"

run_cmd do
  let theorem_name := `AffineProofs.cm_advance_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: AffineProofs.cm_advance_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 AffineProofs.cm_advance_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:AffineProofs.cm_advance_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 · 25 checks passed · 0 failed

2026-11-05T16:36:05.403748801+00:00 · 101.7 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
Lean checked theorem Proofs.state_Lcg64Xsh32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.state_Lcg64Xsh32_spec`	Passed	Claim #2
Lean checked theorem Proofs.stream_Lcg64Xsh32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.stream_Lcg64Xsh32_spec`	Passed	Claim #3
Lean checked theorem Proofs.from_state_Lcg64Xsh32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.from_state_Lcg64Xsh32_spec`	Passed	Claim #4
Lean checked theorem Proofs.new_Lcg64Xsh32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.new_Lcg64Xsh32_spec`	Passed	Claim #5
Lean checked theorem Proofs.state_Lcg128Xsl64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.state_Lcg128Xsl64_spec`	Passed	Claim #6
Lean checked theorem Proofs.stream_Lcg128Xsl64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.stream_Lcg128Xsl64_spec`	Passed	Claim #7
Lean checked theorem Proofs.from_state_Lcg128Xsl64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.from_state_Lcg128Xsl64_spec`	Passed	Claim #8
Lean checked theorem Proofs.new_Lcg128Xsl64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.new_Lcg128Xsl64_spec`	Passed	Claim #9
Lean checked theorem Proofs.state_Lcg128CmDxsm64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.state_Lcg128CmDxsm64_spec`	Passed	Claim #10
Lean checked theorem Proofs.stream_Lcg128CmDxsm64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.stream_Lcg128CmDxsm64_spec`	Passed	Claim #11
Lean checked theorem Proofs.from_state_Lcg128CmDxsm64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.from_state_Lcg128CmDxsm64_spec`	Passed	Claim #12
Lean checked theorem Proofs.new_Lcg128CmDxsm64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.new_Lcg128CmDxsm64_spec`	Passed	Claim #13
Lean checked theorem Proofs.state_Mcg128Xsl64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.state_Mcg128Xsl64_spec`	Passed	Claim #14
Lean checked theorem Proofs.new_Mcg128Xsl64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.new_Mcg128Xsl64_spec`	Passed	Claim #15
Lean checked theorem Proofs.next32_Lcg128Xsl64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.next32_Lcg128Xsl64_spec`	Passed	Claim #16
Lean checked theorem Proofs.next64_Lcg128Xsl64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.next64_Lcg128Xsl64_spec`	Passed	Claim #17
Lean checked theorem Proofs.next32_Mcg128Xsl64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.next32_Mcg128Xsl64_spec`	Passed	Claim #18
Lean checked theorem Proofs.next64_Mcg128Xsl64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.next64_Mcg128Xsl64_spec`	Passed	Claim #19
Lean checked theorem Proofs.next32_Lcg128CmDxsm64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.next32_Lcg128CmDxsm64_spec`	Passed	Claim #20
Lean checked theorem Proofs.next64_Lcg128CmDxsm64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.next64_Lcg128CmDxsm64_spec`	Passed	Claim #21
Lean checked theorem AdvanceProofs.mcg_advance_spec; axioms limited to propext, Classical.choice, Quot.sound `AdvanceProofs.mcg_advance_spec`	Passed	Claim #22
Lean checked theorem AffineProofs.lcg64_advance_spec; axioms limited to propext, Classical.choice, Quot.sound `AffineProofs.lcg64_advance_spec`	Passed	Claim #23
Lean checked theorem AffineProofs.lcg128_advance_spec; axioms limited to propext, Classical.choice, Quot.sound `AffineProofs.lcg128_advance_spec`	Passed	Claim #24
Lean checked theorem AffineProofs.cm_advance_spec; axioms limited to propext, Classical.choice, Quot.sound `AffineProofs.cm_advance_spec`	Passed	Claim #25

Execution details

Started: 2026-11-05T16:36:05.403748801+00:00
Finished: 2026-11-05T16:37:47.053504309+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_pcg/0.10.2/aeneas/2026-11-05/proofs
Environment overrides: None recorded
Git repository: https://github.com/nyuichi/rust-crate-proofs
Git commit: 3b2722d98fcb09ef58d010abf5a42361a4d094c5

Diagnostics & logs

=== stdout ===
⚠ [2/57] Ran aeneas:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
✔ [3/129] Built AeneasMeta.Simp.RegisterCommand (39s)
✔ [248/573] Built Aeneas.Std.Global (39s)
✔ [249/573] Built AeneasMeta.UtilsCore (39s)
✔ [836/1140] Built AeneasMeta.BvEnumToBitVec (40s)
✔ [1575/1805] Built AeneasMeta.OptionConfig (40s)
✔ [1797/1805] Built PcgAdvance.Types (1.8s)
✔ [1798/1805] Built PcgAffineAdvance.Types (1.9s)
✔ [1799/1805] Built RandPcg (2.2s)
ℹ [1800/1805] Built Affine (2.6s)
info: Affine.lean:81:0: 'AffineAdvance.mul_assoc' depends on axioms: [propext]
info: Affine.lean:82:0: 'AffineAdvance.binary_power' depends on axioms: [propext, Quot.sound]
info: Affine.lean:83:0: 'AffineAdvance.apply_power' depends on axioms: [propext]
✔ [1801/1805] Built PcgAdvance.Funs (1.0s)
✔ [1802/1805] Built PcgAffineAdvance.Funs (2.1s)
⚠ [1803/1805] Built Proofs (2.9s)
warning: Proofs.lean:168:2: Unused tactic linter: `all_goals rfl` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:168:12: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Proofs.lean:186:2: Unused tactic linter: `all_goals rfl` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:186:12: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
info: Proofs.lean:213:0: 'Proofs.try_next_u32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:214:0: 'Proofs.state_Lcg64Xsh32_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:215:0: 'Proofs.stream_Lcg64Xsh32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:216:0: 'Proofs.from_state_Lcg64Xsh32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:217:0: 'Proofs.new_Lcg64Xsh32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:218:0: 'Proofs.state_Lcg128Xsl64_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:219:0: 'Proofs.stream_Lcg128Xsl64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:220:0: 'Proofs.from_state_Lcg128Xsl64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:221:0: 'Proofs.new_Lcg128Xsl64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:222:0: 'Proofs.state_Lcg128CmDxsm64_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:223:0: 'Proofs.stream_Lcg128CmDxsm64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:224:0: 'Proofs.from_state_Lcg128CmDxsm64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:225:0: 'Proofs.new_Lcg128CmDxsm64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:226:0: 'Proofs.state_Mcg128Xsl64_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:227:0: 'Proofs.new_Mcg128Xsl64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:228:0: 'Proofs.xslOutput_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:229:0: 'Proofs.dxsmOutput_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:230:0: 'Proofs.next32_Lcg128Xsl64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:231:0: 'Proofs.next64_Lcg128Xsl64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:232:0: 'Proofs.next32_Mcg128Xsl64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:233:0: 'Proofs.next64_Mcg128Xsl64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:234:0: 'Proofs.next32_Lcg128CmDxsm64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:235:0: 'Proofs.next64_Lcg128CmDxsm64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1804/1805] Built AdvanceProofs (4.9s)
info: AdvanceProofs.lean:105:0: 'AdvanceProofs.square_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
info: AdvanceProofs.lean:106:0: 'AdvanceProofs.binary_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
info: AdvanceProofs.lean:108:0: 'AdvanceProofs.body_zero_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: AdvanceProofs.lean:110:0: 'AdvanceProofs.loop_pow_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: AdvanceProofs.lean:112:0: 'AdvanceProofs.mcg_advance_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1805/1805] Built AffineProofs (4.0s)
warning: AffineProofs.lean:190:2: Unused tactic linter: `subst_vars` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
info: AffineProofs.lean:195:0: 'AffineProofs.body128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: AffineProofs.lean:197:0: 'AffineProofs.loop128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: AffineProofs.lean:198:0: 'AffineProofs.lcg128_advance_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: AffineProofs.lean:200:0: 'AffineProofs.body64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: AffineProofs.lean:201:0: 'AffineProofs.loop64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: AffineProofs.lean:202:0: 'AffineProofs.lcg64_advance_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: AffineProofs.lean:204:0: 'AffineProofs.cm_advance_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
Build completed successfully (1805 jobs).

$ lake env lean --stdin (proofs.rs theorem/axiom audit)
proofs.rs:checked:Proofs.try_next_u32_spec
proofs.rs:checked:Proofs.state_Lcg64Xsh32_spec
proofs.rs:checked:Proofs.stream_Lcg64Xsh32_spec
proofs.rs:checked:Proofs.from_state_Lcg64Xsh32_spec
proofs.rs:checked:Proofs.new_Lcg64Xsh32_spec
proofs.rs:checked:Proofs.state_Lcg128Xsl64_spec
proofs.rs:checked:Proofs.stream_Lcg128Xsl64_spec
proofs.rs:checked:Proofs.from_state_Lcg128Xsl64_spec
proofs.rs:checked:Proofs.new_Lcg128Xsl64_spec
proofs.rs:checked:Proofs.state_Lcg128CmDxsm64_spec
proofs.rs:checked:Proofs.stream_Lcg128CmDxsm64_spec
proofs.rs:checked:Proofs.from_state_Lcg128CmDxsm64_spec
proofs.rs:checked:Proofs.new_Lcg128CmDxsm64_spec
proofs.rs:checked:Proofs.state_Mcg128Xsl64_spec
proofs.rs:checked:Proofs.new_Mcg128Xsl64_spec
proofs.rs:checked:Proofs.next32_Lcg128Xsl64_spec
proofs.rs:checked:Proofs.next64_Lcg128Xsl64_spec
proofs.rs:checked:Proofs.next32_Mcg128Xsl64_spec
proofs.rs:checked:Proofs.next64_Mcg128Xsl64_spec
proofs.rs:checked:Proofs.next32_Lcg128CmDxsm64_spec
proofs.rs:checked:Proofs.next64_Lcg128CmDxsm64_spec
proofs.rs:checked:AdvanceProofs.mcg_advance_spec
proofs.rs:checked:AffineProofs.lcg64_advance_spec
proofs.rs:checked:AffineProofs.lcg128_advance_spec
proofs.rs:checked:AffineProofs.cm_advance_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

Unchanged crates.io rand_pcg 0.10.2 Rust sources and Cargo.toml; original archive/hash checks, tests and regeneration comparisons retained in evidence. Rust nightly-2026-09-17; Charon 08d7c9d50144bd84848212c24701253585e90d1f; official Aeneas frontend/library be86ab0f1989d04944292b345b24c435be3ad10a; Lean 4.35.0. Official targeted extraction includes each actual original body, macro-expanded state helpers and private constructor helpers. Separate all-features (serde) extraction is retained in evidence/serde; generated Lean is byte-identical to the default extraction. Six additional output bodies and core::result::Result::map are included via the official --include core::result selection. Two output-permutation helper theorems are audited separately. The MCG advance extraction uses the official PcgAdvanceModel namespace. Its full-delta power/termination proof uses BitVec algebra and a decreasing natural measure, and all configured proof modules are imported together for the final audit. Three LCG advance bodies use a separate official PcgAffineAdvanceModel namespace. BitVec affine algebra and halving induction prove all deltas with increment preservation; all configured proof modules are imported together. Separate Debug supplement: Kani0.68.0/Rust nightly-2026-08-21, rand_core0.10.0 exact lock, four jobs/8925 checks; evidence/kani-debug-baseline. The distinct0.10.1 execution packet is not substituted for this baseline. Separate Lcg64Xsh32 serde Kani0.68/nightly2026-08-21, exact core0.10.0/serde1.0.228/default+serde:691checks/0fail/1unreachable. evidence/kani-pcg32-serde; only dependency path adapted for portable artifact layout. All prior25 proofs/MCGseed/Debug evidence retained. PCG64 serde separate Kani supplement:621checks/0failed/1unreachable, unwind40; evidence/kani-pcg64-serde includes original failed-unwind20 logs and bound-revision evidence. Aeneas25 and all prior MCGseed/Debug/PCG32serde691 results retained. Four additional packets under evidence/kani-followup4 preserve MCGserde592, PCG32composition81, PCG32external158 and wideexternal393 successful checks, all with zero failures. Producer manifests/raw logs/locks and original source hashes are retained; dependency manifest path changes only make packaging portable.

What is trusted

The Rust compiler, official Charon/Aeneas translation, official Aeneas scalar models and Lean kernel are trusted. No custom external models, source adaptations or local trusted helper contracts are used. All twenty-one API theorem dependency audits permit only propext, Classical.choice and Quot.sound. Wrapping arithmetic, shifts, casts and rotations use official standard-library models, rather than proofs of Rust std implementation bodies. The original Result::map body is extracted and proved through its actual closure calls, rather than supplied by a custom model. This serde supplement trusts Kani0.68/CBMC and its August Rust compiler with exact rand_core0.10.0/serde1.0.228. Its concrete sequence backend, invalid_length handler and successful serializer define the observed protocol; they do not stand for arbitrary backends. The Lcg128Xsl64 supplement uses the same exact Kani/Rust/core0.10.0/serde1.0.228 trust boundary and concrete sequence/serializer protocol. Its successful run used unwind40 with unwinding assertions enabled. These supplemental checks trust pinned Kani/CBMC/Z3, Rust nightly2026-08-21 and exact rand_core0.10.0; MCG serde additionally pins serde1.0.228. External calls execute the actual conditional rand_core blanket implementations specialized to these concrete generator types, not a model of arbitrary blanket behavior.

Technical limitations

Coverage is the twenty-five named bodies on x86_64 under default or serde. Internal word states include zero/even values that usual seed constructors may not produce, but all are valid Rust scalar data; no seed-reachability claim is made. Stream getter behavior for arbitrary increments is proved, but no save/restore identity is claimed for an arbitrary even increment. Aeneas byte-seed/from_seed/seed_from_u64 contracts, Lcg64Xsh32::try_next_u64, buffer filling, RNG callbacks/forking, manual Debug, serde and inherited/external blanket APIs remain outside these Aeneas claims. No period, jump-back interpretation for wrapped negative strides, statistical quality or cryptographic security is established. Other targets and dependency feature combinations were not checked. The Debug supplement is limited to the listed constructor-input families, default formatting and the fixed writer behavior; it does not establish arbitrary internal-state provenance, other Formatter flags, partial-prefix failures, arbitrary writers or all constructor histories. It adds no Aeneas API claim. The Lcg64Xsh32 serde check covers only the fixed sequence protocol, lengths0..2, five Deserialize error stages and successful six-stage serialization. Serialize error stages and arbitrary backend/map/format implementations remain unproved; other PCG serde behavior is covered only by the additional concrete protocols explicitly described here. Arbitrary wire increments are accepted by this check; odd increment or generator invariants are not established. This Kani supplement adds no Aeneas machine claims. The Lcg128Xsl64 result is limited to that32-byte sequence protocol and successful six-callback serialization. Serialize errors, arbitrary backends/map formats, odd increment and nonzero invariants are not established. An earlier unwind20 run failed its unwinding assertion; it is retained as an insufficient-bound attempt, not a successful proof or a crate behavior counterexample. Only the unwind bound changed for the successful run. MCG serde is limited to the fixed sequence protocol, length0..1, three Deserialize callback error stages and successful four-callback serialization; Serialize errors and arbitrary backends/map/formats remain unproved. No odd/nonzero/period invariant follows for its arbitrary wire states. The default-only composition and eight external Rng relations cover constructor-image states, excluding even-increment serde states, zero MCG and all arbitrary private-state histories. They establish relational equivalence to actual TryRng behavior, not independent numeric output, distribution, security or general blanket correctness. A separate seed relation attempt failed in CBMC SMT SSA conversion with map::at before a property verdict; it remains unverified and is not a counterexample. All new evidence is supplemental; the machine count stays25.

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—

serde ^1 · optional—

Comments (0)

No comments.