Report #30 — Exact xoshiro outputs and complete little-endian state serialization

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

69 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:58 UTC

Revision v4 · v3 · v2 · v1

Overview

For rand_xoshiro 0.8.1 on x86_64 with default or serde features, 69 scoped contracts specify exact outputs and state updates for every internal word pattern, including zero states. Thirty-five direct original-body contracts cover native outputs, all fifteen little-endian state serializers, and Seed512 zero initialization, byte views, legal fixed-length mutable writeback and iterator initialization. Nine compiler-inlined original calls cover 64-to-32-bit projections: xoroshiro128++ and xoroshiro128** use low output bits; the other seven use high bits. Twenty-five further compiler-inlined calls cover the external rand_core 0.10.1 blanket Rng::next_u32/next_u64 specializations, preserving the exact original forwarding behavior and full resulting state. These are external trait specializations, not local declarations. The original selected translations agree under default and serde features; serde implementations themselves are not proved. Eleven two/four-word serializers use the explicitly bounded U32/U64 primitive layout dictionaries; three eight-word serializers prove termination of the original serialization loop. Separate Kani seed/state/composition results remain supplementary evidence, not additional Aeneas claims. Separately, two original-Rust Kani/Z3 harnesses cover the public Seed512 tuple-constructor operation for every64-byte input. Constructing Seed512(bytes) preserves all64 bytes in its public field and actual AsRef view. For every independent64-byte replacement, copying it through the constructed value's actual AsMut slice writes exactly those bytes back to its public field and AsRef view. These84 successful checks concern a data constructor operation, not a fabricated associated function or a new registered API claim. Existing Default, AsRef, AsMut and iteration mappings are observations/composition here and are not counted again.

Findings (0)

No findings reported.

APIs (69)

Recorded callables

<rand_xoshiro::Seed512 as AsMut<[u8]>>::as_mut recorded callable · signature and safety not recorded

Claim #28

<rand_xoshiro::Seed512 as AsRef<[u8]>>::as_ref recorded callable · signature and safety not recorded

Claim #27

<rand_xoshiro::Seed512 as Default>::default recorded callable · signature and safety not recorded

Claim #26

<rand_xoshiro::SplitMix64 as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #2

<rand_xoshiro::SplitMix64 as TryRng>::try_next_u64 recorded callable · signature and safety not recorded

Claim #1

<rand_xoshiro::SplitMix64 as rand_core::Rng>::next_u32 recorded callable · signature and safety not recorded

Claim #45

<rand_xoshiro::SplitMix64 as rand_core::Rng>::next_u64 recorded callable · signature and safety not recorded

Claim #46

<rand_xoshiro::Xoroshiro128Plus as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #17

<rand_xoshiro::Xoroshiro128Plus as TryRng>::try_next_u64 recorded callable · signature and safety not recorded

Claim #3

<rand_xoshiro::Xoroshiro128Plus as rand_core::Rng>::next_u32 recorded callable · signature and safety not recorded

Claim #47

<rand_xoshiro::Xoroshiro128Plus as rand_core::Rng>::next_u64 recorded callable · signature and safety not recorded

Claim #48

<rand_xoshiro::Xoroshiro128PlusPlus as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #18

<rand_xoshiro::Xoroshiro128PlusPlus as TryRng>::try_next_u64 recorded callable · signature and safety not recorded

Claim #4

<rand_xoshiro::Xoroshiro128PlusPlus as rand_core::Rng>::next_u32 recorded callable · signature and safety not recorded

Claim #49

<rand_xoshiro::Xoroshiro128PlusPlus as rand_core::Rng>::next_u64 recorded callable · signature and safety not recorded

Claim #50

<rand_xoshiro::Xoroshiro128StarStar as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #19

<rand_xoshiro::Xoroshiro128StarStar as TryRng>::try_next_u64 recorded callable · signature and safety not recorded

Claim #5

<rand_xoshiro::Xoroshiro128StarStar as rand_core::Rng>::next_u32 recorded callable · signature and safety not recorded

Claim #51

<rand_xoshiro::Xoroshiro128StarStar as rand_core::Rng>::next_u64 recorded callable · signature and safety not recorded

Claim #52

<rand_xoshiro::Xoroshiro64Star as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #6

<rand_xoshiro::Xoroshiro64Star as rand_core::Rng>::next_u32 recorded callable · signature and safety not recorded

Claim #53

<rand_xoshiro::Xoroshiro64StarStar as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #7

<rand_xoshiro::Xoroshiro64StarStar as rand_core::Rng>::next_u32 recorded callable · signature and safety not recorded

Claim #54

<rand_xoshiro::Xoshiro128Plus as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #8

<rand_xoshiro::Xoshiro128Plus as rand_core::Rng>::next_u32 recorded callable · signature and safety not recorded

Claim #55

<rand_xoshiro::Xoshiro128PlusPlus as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #9

<rand_xoshiro::Xoshiro128PlusPlus as rand_core::Rng>::next_u32 recorded callable · signature and safety not recorded

Claim #56

<rand_xoshiro::Xoshiro128StarStar as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #10

<rand_xoshiro::Xoshiro128StarStar as rand_core::Rng>::next_u32 recorded callable · signature and safety not recorded

Claim #57

<rand_xoshiro::Xoshiro256Plus as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #20

<rand_xoshiro::Xoshiro256Plus as TryRng>::try_next_u64 recorded callable · signature and safety not recorded

Claim #11

<rand_xoshiro::Xoshiro256Plus as rand_core::Rng>::next_u32 recorded callable · signature and safety not recorded

Claim #58

<rand_xoshiro::Xoshiro256Plus as rand_core::Rng>::next_u64 recorded callable · signature and safety not recorded

Claim #59

<rand_xoshiro::Xoshiro256PlusPlus as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #21

<rand_xoshiro::Xoshiro256PlusPlus as TryRng>::try_next_u64 recorded callable · signature and safety not recorded

Claim #12

<rand_xoshiro::Xoshiro256PlusPlus as rand_core::Rng>::next_u32 recorded callable · signature and safety not recorded

Claim #60

<rand_xoshiro::Xoshiro256PlusPlus as rand_core::Rng>::next_u64 recorded callable · signature and safety not recorded

Claim #61

<rand_xoshiro::Xoshiro256StarStar as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #22

<rand_xoshiro::Xoshiro256StarStar as TryRng>::try_next_u64 recorded callable · signature and safety not recorded

Claim #13

<rand_xoshiro::Xoshiro256StarStar as rand_core::Rng>::next_u32 recorded callable · signature and safety not recorded

Claim #62

<rand_xoshiro::Xoshiro256StarStar as rand_core::Rng>::next_u64 recorded callable · signature and safety not recorded

Claim #63

<rand_xoshiro::Xoshiro512Plus as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #23

<rand_xoshiro::Xoshiro512Plus as TryRng>::try_next_u64 recorded callable · signature and safety not recorded

Claim #14

<rand_xoshiro::Xoshiro512Plus as rand_core::Rng>::next_u32 recorded callable · signature and safety not recorded

Claim #64

<rand_xoshiro::Xoshiro512Plus as rand_core::Rng>::next_u64 recorded callable · signature and safety not recorded

Claim #65

<rand_xoshiro::Xoshiro512PlusPlus as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #24

<rand_xoshiro::Xoshiro512PlusPlus as TryRng>::try_next_u64 recorded callable · signature and safety not recorded

Claim #15

<rand_xoshiro::Xoshiro512PlusPlus as rand_core::Rng>::next_u32 recorded callable · signature and safety not recorded

Claim #66

<rand_xoshiro::Xoshiro512PlusPlus as rand_core::Rng>::next_u64 recorded callable · signature and safety not recorded

Claim #67

<rand_xoshiro::Xoshiro512StarStar as TryRng>::try_next_u32 recorded callable · signature and safety not recorded

Claim #25

<rand_xoshiro::Xoshiro512StarStar as TryRng>::try_next_u64 recorded callable · signature and safety not recorded

Claim #16

<rand_xoshiro::Xoshiro512StarStar as rand_core::Rng>::next_u32 recorded callable · signature and safety not recorded

Claim #68

<rand_xoshiro::Xoshiro512StarStar as rand_core::Rng>::next_u64 recorded callable · signature and safety not recorded

Claim #69

Seed512::iter recorded callable · signature and safety not recorded

Claim #29

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

Claim #30

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

Claim #31

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

Claim #32

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

Claim #33

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

Claim #34

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

Claim #35

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

Claim #36

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

Claim #37

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

Claim #38

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

Claim #39

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

Claim #40

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

Claim #41

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

Claim #42

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

Claim #43

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

Claim #44

Evidence

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

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/nyuichi/rust-crate-proofs report-30-source-1
git -C report-30-source-1 checkout --detach e7e01c0c19c984cc7e5fb182fd1007c9432766fe
git -C report-30-source-1 submodule update --init --recursive --checkout
cd report-30-source-1/rand_xoshiro/0.8.1/aeneas/2026-11-05/proofs

lake build +Proofs +RngProofs +SeedProofs +SerializerLoopProofs +SerializerProofs +StateProofs +WrapperProofs

printf '%s' 'import Lean
import Proofs
import RngProofs
import SeedProofs
import SerializerLoopProofs
import SerializerProofs
import StateProofs
import WrapperProofs
open Lean Elab Command

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2026-11-05T18:23:29.021142425+00:00 · 123.2 seconds · Exit code 0

Recorded on the author’s machine.

Check	Result	Claim
Lean checked theorem Proofs.SplitMix64_64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.SplitMix64_64_spec`	Passed	Claim #1
Lean checked theorem Proofs.SplitMix64_32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.SplitMix64_32_spec`	Passed	Claim #2
Lean checked theorem Proofs.Xoroshiro128Plus_64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.Xoroshiro128Plus_64_spec`	Passed	Claim #3
Lean checked theorem Proofs.Xoroshiro128PlusPlus_64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.Xoroshiro128PlusPlus_64_spec`	Passed	Claim #4
Lean checked theorem Proofs.Xoroshiro128StarStar_64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.Xoroshiro128StarStar_64_spec`	Passed	Claim #5
Lean checked theorem Proofs.Xoroshiro64Star_32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.Xoroshiro64Star_32_spec`	Passed	Claim #6
Lean checked theorem Proofs.Xoroshiro64StarStar_32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.Xoroshiro64StarStar_32_spec`	Passed	Claim #7
Lean checked theorem Proofs.Xoshiro128Plus_32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.Xoshiro128Plus_32_spec`	Passed	Claim #8
Lean checked theorem Proofs.Xoshiro128PlusPlus_32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.Xoshiro128PlusPlus_32_spec`	Passed	Claim #9
Lean checked theorem Proofs.Xoshiro128StarStar_32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.Xoshiro128StarStar_32_spec`	Passed	Claim #10
Lean checked theorem Proofs.Xoshiro256Plus_64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.Xoshiro256Plus_64_spec`	Passed	Claim #11
Lean checked theorem Proofs.Xoshiro256PlusPlus_64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.Xoshiro256PlusPlus_64_spec`	Passed	Claim #12
Lean checked theorem Proofs.Xoshiro256StarStar_64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.Xoshiro256StarStar_64_spec`	Passed	Claim #13
Lean checked theorem Proofs.Xoshiro512Plus_64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.Xoshiro512Plus_64_spec`	Passed	Claim #14
Lean checked theorem Proofs.Xoshiro512PlusPlus_64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.Xoshiro512PlusPlus_64_spec`	Passed	Claim #15
Lean checked theorem Proofs.Xoshiro512StarStar_64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.Xoshiro512StarStar_64_spec`	Passed	Claim #16
Lean checked theorem WrapperProofs.Xoroshiro128Plus_32_via_original_api_spec; axioms limited to propext, Classical.choice, Quot.sound `WrapperProofs.Xoroshiro128Plus_32_via_original_api_spec`	Passed	Claim #17
Lean checked theorem WrapperProofs.Xoroshiro128PlusPlus_32_via_original_api_spec; axioms limited to propext, Classical.choice, Quot.sound `WrapperProofs.Xoroshiro128PlusPlus_32_via_original_api_spec`	Passed	Claim #18
Lean checked theorem WrapperProofs.Xoroshiro128StarStar_32_via_original_api_spec; axioms limited to propext, Classical.choice, Quot.sound `WrapperProofs.Xoroshiro128StarStar_32_via_original_api_spec`	Passed	Claim #19
Lean checked theorem WrapperProofs.Xoshiro256Plus_32_via_original_api_spec; axioms limited to propext, Classical.choice, Quot.sound `WrapperProofs.Xoshiro256Plus_32_via_original_api_spec`	Passed	Claim #20
Lean checked theorem WrapperProofs.Xoshiro256PlusPlus_32_via_original_api_spec; axioms limited to propext, Classical.choice, Quot.sound `WrapperProofs.Xoshiro256PlusPlus_32_via_original_api_spec`	Passed	Claim #21
Lean checked theorem WrapperProofs.Xoshiro256StarStar_32_via_original_api_spec; axioms limited to propext, Classical.choice, Quot.sound `WrapperProofs.Xoshiro256StarStar_32_via_original_api_spec`	Passed	Claim #22
Lean checked theorem WrapperProofs.Xoshiro512Plus_32_via_original_api_spec; axioms limited to propext, Classical.choice, Quot.sound `WrapperProofs.Xoshiro512Plus_32_via_original_api_spec`	Passed	Claim #23
Lean checked theorem WrapperProofs.Xoshiro512PlusPlus_32_via_original_api_spec; axioms limited to propext, Classical.choice, Quot.sound `WrapperProofs.Xoshiro512PlusPlus_32_via_original_api_spec`	Passed	Claim #24
Lean checked theorem WrapperProofs.Xoshiro512StarStar_32_via_original_api_spec; axioms limited to propext, Classical.choice, Quot.sound `WrapperProofs.Xoshiro512StarStar_32_via_original_api_spec`	Passed	Claim #25
Lean checked theorem SeedProofs.default_spec; axioms limited to propext, Classical.choice, Quot.sound `SeedProofs.default_spec`	Passed	Claim #26
Lean checked theorem SeedProofs.as_ref_spec; axioms limited to propext, Classical.choice, Quot.sound `SeedProofs.as_ref_spec`	Passed	Claim #27
Lean checked theorem SeedProofs.as_mut_spec; axioms limited to propext, Classical.choice, Quot.sound `SeedProofs.as_mut_spec`	Passed	Claim #28
Lean checked theorem SeedProofs.iter_spec; axioms limited to propext, Classical.choice, Quot.sound `SeedProofs.iter_spec`	Passed	Claim #29
Lean checked theorem StateProofs.splitmix_state_spec; axioms limited to propext, Classical.choice, Quot.sound `StateProofs.splitmix_state_spec`	Passed	Claim #30
Lean checked theorem SerializerProofs.Xoroshiro128Plus_state_spec; axioms limited to propext, Classical.choice, Quot.sound `SerializerProofs.Xoroshiro128Plus_state_spec`	Passed	Claim #31
Lean checked theorem SerializerProofs.Xoroshiro128PlusPlus_state_spec; axioms limited to propext, Classical.choice, Quot.sound `SerializerProofs.Xoroshiro128PlusPlus_state_spec`	Passed	Claim #32
Lean checked theorem SerializerProofs.Xoroshiro128StarStar_state_spec; axioms limited to propext, Classical.choice, Quot.sound `SerializerProofs.Xoroshiro128StarStar_state_spec`	Passed	Claim #33
Lean checked theorem SerializerProofs.Xoroshiro64Star_state_spec; axioms limited to propext, Classical.choice, Quot.sound `SerializerProofs.Xoroshiro64Star_state_spec`	Passed	Claim #34
Lean checked theorem SerializerProofs.Xoroshiro64StarStar_state_spec; axioms limited to propext, Classical.choice, Quot.sound `SerializerProofs.Xoroshiro64StarStar_state_spec`	Passed	Claim #35
Lean checked theorem SerializerProofs.Xoshiro128Plus_state_spec; axioms limited to propext, Classical.choice, Quot.sound `SerializerProofs.Xoshiro128Plus_state_spec`	Passed	Claim #36
Lean checked theorem SerializerProofs.Xoshiro128PlusPlus_state_spec; axioms limited to propext, Classical.choice, Quot.sound `SerializerProofs.Xoshiro128PlusPlus_state_spec`	Passed	Claim #37
Lean checked theorem SerializerProofs.Xoshiro128StarStar_state_spec; axioms limited to propext, Classical.choice, Quot.sound `SerializerProofs.Xoshiro128StarStar_state_spec`	Passed	Claim #38
Lean checked theorem SerializerProofs.Xoshiro256Plus_state_spec; axioms limited to propext, Classical.choice, Quot.sound `SerializerProofs.Xoshiro256Plus_state_spec`	Passed	Claim #39
Lean checked theorem SerializerProofs.Xoshiro256PlusPlus_state_spec; axioms limited to propext, Classical.choice, Quot.sound `SerializerProofs.Xoshiro256PlusPlus_state_spec`	Passed	Claim #40
Lean checked theorem SerializerProofs.Xoshiro256StarStar_state_spec; axioms limited to propext, Classical.choice, Quot.sound `SerializerProofs.Xoshiro256StarStar_state_spec`	Passed	Claim #41
Lean checked theorem SerializerProofs.Xoshiro512Plus_state_spec; axioms limited to propext, Classical.choice, Quot.sound `SerializerProofs.Xoshiro512Plus_state_spec`	Passed	Claim #42
Lean checked theorem SerializerProofs.Xoshiro512PlusPlus_state_spec; axioms limited to propext, Classical.choice, Quot.sound `SerializerProofs.Xoshiro512PlusPlus_state_spec`	Passed	Claim #43
Lean checked theorem SerializerProofs.Xoshiro512StarStar_state_spec; axioms limited to propext, Classical.choice, Quot.sound `SerializerProofs.Xoshiro512StarStar_state_spec`	Passed	Claim #44
Lean checked theorem RngProofs.SplitMix64_rng_32_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.SplitMix64_rng_32_spec`	Passed	Claim #45
Lean checked theorem RngProofs.SplitMix64_rng_64_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.SplitMix64_rng_64_spec`	Passed	Claim #46
Lean checked theorem RngProofs.Xoroshiro128Plus_rng_32_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoroshiro128Plus_rng_32_spec`	Passed	Claim #47
Lean checked theorem RngProofs.Xoroshiro128Plus_rng_64_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoroshiro128Plus_rng_64_spec`	Passed	Claim #48
Lean checked theorem RngProofs.Xoroshiro128PlusPlus_rng_32_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoroshiro128PlusPlus_rng_32_spec`	Passed	Claim #49
Lean checked theorem RngProofs.Xoroshiro128PlusPlus_rng_64_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoroshiro128PlusPlus_rng_64_spec`	Passed	Claim #50
Lean checked theorem RngProofs.Xoroshiro128StarStar_rng_32_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoroshiro128StarStar_rng_32_spec`	Passed	Claim #51
Lean checked theorem RngProofs.Xoroshiro128StarStar_rng_64_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoroshiro128StarStar_rng_64_spec`	Passed	Claim #52
Lean checked theorem RngProofs.Xoroshiro64Star_rng_32_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoroshiro64Star_rng_32_spec`	Passed	Claim #53
Lean checked theorem RngProofs.Xoroshiro64StarStar_rng_32_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoroshiro64StarStar_rng_32_spec`	Passed	Claim #54
Lean checked theorem RngProofs.Xoshiro128Plus_rng_32_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoshiro128Plus_rng_32_spec`	Passed	Claim #55
Lean checked theorem RngProofs.Xoshiro128PlusPlus_rng_32_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoshiro128PlusPlus_rng_32_spec`	Passed	Claim #56
Lean checked theorem RngProofs.Xoshiro128StarStar_rng_32_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoshiro128StarStar_rng_32_spec`	Passed	Claim #57
Lean checked theorem RngProofs.Xoshiro256Plus_rng_32_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoshiro256Plus_rng_32_spec`	Passed	Claim #58
Lean checked theorem RngProofs.Xoshiro256Plus_rng_64_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoshiro256Plus_rng_64_spec`	Passed	Claim #59
Lean checked theorem RngProofs.Xoshiro256PlusPlus_rng_32_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoshiro256PlusPlus_rng_32_spec`	Passed	Claim #60
Lean checked theorem RngProofs.Xoshiro256PlusPlus_rng_64_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoshiro256PlusPlus_rng_64_spec`	Passed	Claim #61
Lean checked theorem RngProofs.Xoshiro256StarStar_rng_32_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoshiro256StarStar_rng_32_spec`	Passed	Claim #62
Lean checked theorem RngProofs.Xoshiro256StarStar_rng_64_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoshiro256StarStar_rng_64_spec`	Passed	Claim #63
Lean checked theorem RngProofs.Xoshiro512Plus_rng_32_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoshiro512Plus_rng_32_spec`	Passed	Claim #64
Lean checked theorem RngProofs.Xoshiro512Plus_rng_64_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoshiro512Plus_rng_64_spec`	Passed	Claim #65
Lean checked theorem RngProofs.Xoshiro512PlusPlus_rng_32_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoshiro512PlusPlus_rng_32_spec`	Passed	Claim #66
Lean checked theorem RngProofs.Xoshiro512PlusPlus_rng_64_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoshiro512PlusPlus_rng_64_spec`	Passed	Claim #67
Lean checked theorem RngProofs.Xoshiro512StarStar_rng_32_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoshiro512StarStar_rng_32_spec`	Passed	Claim #68
Lean checked theorem RngProofs.Xoshiro512StarStar_rng_64_spec; axioms limited to propext, Classical.choice, Quot.sound `RngProofs.Xoshiro512StarStar_rng_64_spec`	Passed	Claim #69

Execution details

Started: 2026-11-05T18:23:29.021142425+00:00
Finished: 2026-11-05T18:25:32.249007387+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_xoshiro/0.8.1/aeneas/2026-11-05/proofs
Environment overrides: None recorded
Git repository: https://github.com/nyuichi/rust-crate-proofs
Git commit: e7e01c0c19c984cc7e5fb182fd1007c9432766fe

Diagnostics & logs

=== stdout ===
⚠ [2/57] Ran aeneas:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
✔ [3/75] Built AeneasMeta.Simp.RegisterCommand (42s)
✔ [142/345] Built Aeneas.Std.Global (42s)
✔ [143/345] Built AeneasMeta.BvEnumToBitVec (42s)
✔ [293/594] Built AeneasMeta.UtilsCore (42s)
✔ [1575/1815] Built AeneasMeta.OptionConfig (43s)
✔ [1797/1815] Built Seed512.Types (2.6s)
✔ [1798/1815] Built SplitMixState.Types (2.7s)
✔ [1799/1815] Built XoshiroRngApiRoots.Types (2.7s)
✔ [1800/1815] Built Serializers.Types (2.8s)
✔ [1801/1815] Built RandXoshiro (4.3s)
✔ [1802/1815] Built Seed512.Funs (2.8s)
✔ [1803/1815] Built SplitMixState.Funs (2.8s)
✔ [1804/1815] Built XoshiroApiRoots.Types (2.0s)
✔ [1805/1815] Built Serializers.FunsExternal (3.0s)
✔ [1806/1815] Built XoshiroRngApiRoots.Funs (4.8s)
ℹ [1807/1815] Built StateProofs (3.0s)
info: StateProofs.lean:10:0: 'StateProofs.splitmix_state_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1808/1815] Built SeedProofs (3.3s)
info: SeedProofs.lean:28:0: 'SeedProofs.default_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SeedProofs.lean:29:0: 'SeedProofs.as_ref_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SeedProofs.lean:30:0: 'SeedProofs.as_mut_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SeedProofs.lean:31:0: 'SeedProofs.iter_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [1809/1815] Built XoshiroApiRoots.Funs (6.4s)
✔ [1810/1815] Built Serializers.Funs (6.9s)
⚠ [1811/1815] Built Proofs (11s)
warning: Proofs.lean:264:37: `simp` already closes the goal

Hint: Use `simp` instead of `simpa`:
  [apply] simp

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Proofs.lean:276:37: `simp` already closes the goal

Hint: Use `simp` instead of `simpa`:
  [apply] simp

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
info: Proofs.lean:369:0: 'Proofs.SplitMix64_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:370:0: 'Proofs.SplitMix64_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:371:0: 'Proofs.Xoroshiro128Plus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:372:0: 'Proofs.Xoroshiro128PlusPlus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:373:0: 'Proofs.Xoroshiro128StarStar_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:374:0: 'Proofs.Xoroshiro64Star_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:375:0: 'Proofs.Xoroshiro64StarStar_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:376:0: 'Proofs.Xoshiro128Plus_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:377:0: 'Proofs.Xoshiro128PlusPlus_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:378:0: 'Proofs.Xoshiro128StarStar_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:379:0: 'Proofs.Xoshiro256Plus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:380:0: 'Proofs.Xoshiro256PlusPlus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:381:0: 'Proofs.Xoshiro256StarStar_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:382:0: 'Proofs.Xoshiro512Plus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:383:0: 'Proofs.Xoshiro512PlusPlus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:384:0: 'Proofs.Xoshiro512StarStar_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:385:0: 'Proofs.arr4_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:386:0: 'Proofs.arr8_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:387:0: 'Proofs.inputXoroshiro128Plus_64_surjective' does not depend on any axioms
info: Proofs.lean:388:0: 'Proofs.inputXoroshiro128PlusPlus_64_surjective' does not depend on any axioms
info: Proofs.lean:389:0: 'Proofs.inputXoroshiro128StarStar_64_surjective' does not depend on any axioms
info: Proofs.lean:390:0: 'Proofs.inputXoroshiro64Star_32_surjective' does not depend on any axioms
info: Proofs.lean:391:0: 'Proofs.inputXoroshiro64StarStar_32_surjective' does not depend on any axioms
info: Proofs.lean:392:0: 'Proofs.inputXoshiro128Plus_32_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:393:0: 'Proofs.inputXoshiro128PlusPlus_32_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:394:0: 'Proofs.inputXoshiro128StarStar_32_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:395:0: 'Proofs.inputXoshiro256Plus_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:396:0: 'Proofs.inputXoshiro256PlusPlus_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:397:0: 'Proofs.inputXoshiro256StarStar_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:398:0: 'Proofs.inputXoshiro512Plus_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:399:0: 'Proofs.inputXoshiro512PlusPlus_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:400:0: 'Proofs.inputXoshiro512StarStar_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1812/1815] Built RngProofs (13s)
warning: RngProofs.lean:68:37: Variable name `b` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:83:32: Variable name `b` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:98:36: Variable name `b` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:113:31: Variable name `b` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:113:33: Variable name `c` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _c

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:129:35: Variable name `b` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:129:37: Variable name `c` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _c

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:145:33: Variable name `a` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _a

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:145:37: Variable name `c` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _c

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:145:39: Variable name `d` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _d

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:161:31: Variable name `b` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:161:33: Variable name `c` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _c

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:177:35: Variable name `b` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:177:37: Variable name `c` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _c

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:193:33: Variable name `a` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _a

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:193:37: Variable name `c` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _c

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:193:39: Variable name `d` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _d

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:209:31: Variable name `b` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:209:35: Variable name `d` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _d

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:209:37: Variable name `e` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _e

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:209:39: Variable name `f` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _f

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:209:41: Variable name `g` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _g

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:209:43: Variable name `h` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _h

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:227:35: Variable name `b` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:227:39: Variable name `d` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _d

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:227:41: Variable name `e` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _e

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:227:43: Variable name `f` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _f

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:227:45: Variable name `g` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _g

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:227:47: Variable name `h` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _h

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:245:33: Variable name `a` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _a

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:245:37: Variable name `c` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _c

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:245:39: Variable name `d` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _d

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:245:41: Variable name `e` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _e

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:245:43: Variable name `f` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _f

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:245:45: Variable name `g` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _g

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:245:47: Variable name `h` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _h

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: RngProofs.lean:263:37: `simp` already closes the goal

Hint: Use `simp` instead of `simpa`:
  [apply] simp

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: RngProofs.lean:275:37: `simp` already closes the goal

Hint: Use `simp` instead of `simpa`:
  [apply] simp

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: RngProofs.lean:373:2: Unused tactic linter: `all_goals rfl` does nothing.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
info: RngProofs.lean:543:0: 'RngProofs.SplitMix64_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:544:0: 'RngProofs.SplitMix64_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:545:0: 'RngProofs.Xoroshiro128Plus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:546:0: 'RngProofs.Xoroshiro128PlusPlus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:547:0: 'RngProofs.Xoroshiro128StarStar_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:548:0: 'RngProofs.Xoroshiro64Star_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:549:0: 'RngProofs.Xoroshiro64StarStar_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:550:0: 'RngProofs.Xoshiro128Plus_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:551:0: 'RngProofs.Xoshiro128PlusPlus_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:552:0: 'RngProofs.Xoshiro128StarStar_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:553:0: 'RngProofs.Xoshiro256Plus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:554:0: 'RngProofs.Xoshiro256PlusPlus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:555:0: 'RngProofs.Xoshiro256StarStar_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:556:0: 'RngProofs.Xoshiro512Plus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:557:0: 'RngProofs.Xoshiro512PlusPlus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:558:0: 'RngProofs.Xoshiro512StarStar_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:559:0: 'RngProofs.arr4_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:560:0: 'RngProofs.arr8_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:561:0: 'RngProofs.inputXoroshiro128Plus_64_surjective' does not depend on any axioms
info: RngProofs.lean:562:0: 'RngProofs.inputXoroshiro128PlusPlus_64_surjective' does not depend on any axioms
info: RngProofs.lean:563:0: 'RngProofs.inputXoroshiro128StarStar_64_surjective' does not depend on any axioms
info: RngProofs.lean:564:0: 'RngProofs.inputXoroshiro64Star_32_surjective' does not depend on any axioms
info: RngProofs.lean:565:0: 'RngProofs.inputXoroshiro64StarStar_32_surjective' does not depend on any axioms
info: RngProofs.lean:566:0: 'RngProofs.inputXoshiro128Plus_32_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:567:0: 'RngProofs.inputXoshiro128PlusPlus_32_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:568:0: 'RngProofs.inputXoshiro128StarStar_32_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:569:0: 'RngProofs.inputXoshiro256Plus_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:570:0: 'RngProofs.inputXoshiro256PlusPlus_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:571:0: 'RngProofs.inputXoshiro256StarStar_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:572:0: 'RngProofs.inputXoshiro512Plus_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:573:0: 'RngProofs.inputXoshiro512PlusPlus_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:574:0: 'RngProofs.inputXoshiro512StarStar_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:575:0: 'RngProofs.SplitMix64_rng_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:576:0: 'RngProofs.SplitMix64_rng_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:577:0: 'RngProofs.Xoroshiro128Plus_rng_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:578:0: 'RngProofs.Xoroshiro128Plus_rng_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:579:0: 'RngProofs.Xoroshiro128PlusPlus_rng_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:580:0: 'RngProofs.Xoroshiro128PlusPlus_rng_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:581:0: 'RngProofs.Xoroshiro128StarStar_rng_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:582:0: 'RngProofs.Xoroshiro128StarStar_rng_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:583:0: 'RngProofs.Xoroshiro64Star_rng_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:584:0: 'RngProofs.Xoroshiro64StarStar_rng_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:585:0: 'RngProofs.Xoshiro128Plus_rng_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:586:0: 'RngProofs.Xoshiro128PlusPlus_rng_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:587:0: 'RngProofs.Xoshiro128StarStar_rng_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:588:0: 'RngProofs.Xoshiro256Plus_rng_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:589:0: 'RngProofs.Xoshiro256Plus_rng_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:590:0: 'RngProofs.Xoshiro256PlusPlus_rng_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:591:0: 'RngProofs.Xoshiro256PlusPlus_rng_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:592:0: 'RngProofs.Xoshiro256StarStar_rng_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:593:0: 'RngProofs.Xoshiro256StarStar_rng_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:594:0: 'RngProofs.Xoshiro512Plus_rng_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:595:0: 'RngProofs.Xoshiro512Plus_rng_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:596:0: 'RngProofs.Xoshiro512PlusPlus_rng_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:597:0: 'RngProofs.Xoshiro512PlusPlus_rng_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:598:0: 'RngProofs.Xoshiro512StarStar_rng_32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RngProofs.lean:599:0: 'RngProofs.Xoshiro512StarStar_rng_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1813/1815] Built WrapperProofs (11s)
warning: WrapperProofs.lean:42:37: Variable name `b` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:57:31: Variable name `b` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:57:33: Variable name `c` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _c

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:73:35: Variable name `b` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:73:37: Variable name `c` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _c

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:89:33: Variable name `a` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _a

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:89:37: Variable name `c` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _c

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:89:39: Variable name `d` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _d

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:105:31: Variable name `b` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:105:35: Variable name `d` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _d

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:105:37: Variable name `e` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _e

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:105:39: Variable name `f` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _f

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:105:41: Variable name `g` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _g

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:105:43: Variable name `h` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _h

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:123:35: Variable name `b` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:123:39: Variable name `d` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _d

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:123:41: Variable name `e` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _e

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:123:43: Variable name `f` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _f

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:123:45: Variable name `g` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _g

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:123:47: Variable name `h` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _h

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:141:33: Variable name `a` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _a

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:141:37: Variable name `c` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _c

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:141:39: Variable name `d` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _d

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:141:41: Variable name `e` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _e

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:141:43: Variable name `f` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _f

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:141:45: Variable name `g` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _g

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:141:47: Variable name `h` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _h

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: WrapperProofs.lean:159:37: `simp` already closes the goal

Hint: Use `simp` instead of `simpa`:
  [apply] simp

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: WrapperProofs.lean:171:37: `simp` already closes the goal

Hint: Use `simp` instead of `simpa`:
  [apply] simp

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: WrapperProofs.lean:242:2: Unused tactic linter: `all_goals rfl` does nothing.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
info: WrapperProofs.lean:300:0: 'WrapperProofs.Xoroshiro128Plus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:301:0: 'WrapperProofs.Xoroshiro128PlusPlus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:302:0: 'WrapperProofs.Xoroshiro128StarStar_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:303:0: 'WrapperProofs.Xoshiro256Plus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:304:0: 'WrapperProofs.Xoshiro256PlusPlus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:305:0: 'WrapperProofs.Xoshiro256StarStar_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:306:0: 'WrapperProofs.Xoshiro512Plus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:307:0: 'WrapperProofs.Xoshiro512PlusPlus_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:308:0: 'WrapperProofs.Xoshiro512StarStar_64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:309:0: 'WrapperProofs.arr4_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:310:0: 'WrapperProofs.arr8_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:311:0: 'WrapperProofs.inputXoroshiro128Plus_64_surjective' does not depend on any axioms
info: WrapperProofs.lean:312:0: 'WrapperProofs.inputXoroshiro128PlusPlus_64_surjective' does not depend on any axioms
info: WrapperProofs.lean:313:0: 'WrapperProofs.inputXoroshiro128StarStar_64_surjective' does not depend on any axioms
info: WrapperProofs.lean:314:0: 'WrapperProofs.inputXoshiro256Plus_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:315:0: 'WrapperProofs.inputXoshiro256PlusPlus_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:316:0: 'WrapperProofs.inputXoshiro256StarStar_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:317:0: 'WrapperProofs.inputXoshiro512Plus_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:318:0: 'WrapperProofs.inputXoshiro512PlusPlus_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:319:0: 'WrapperProofs.inputXoshiro512StarStar_64_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:320:0: 'WrapperProofs.Xoroshiro128Plus_32_via_original_api_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:321:0: 'WrapperProofs.Xoroshiro128PlusPlus_32_via_original_api_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:322:0: 'WrapperProofs.Xoroshiro128StarStar_32_via_original_api_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:323:0: 'WrapperProofs.Xoshiro256Plus_32_via_original_api_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:324:0: 'WrapperProofs.Xoshiro256PlusPlus_32_via_original_api_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:325:0: 'WrapperProofs.Xoshiro256StarStar_32_via_original_api_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:326:0: 'WrapperProofs.Xoshiro512Plus_32_via_original_api_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:327:0: 'WrapperProofs.Xoshiro512PlusPlus_32_via_original_api_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: WrapperProofs.lean:328:0: 'WrapperProofs.Xoshiro512StarStar_32_via_original_api_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1814/1815] Built SerializerProofs (10s)
warning: SerializerProofs.lean:42:2: Unused tactic linter: `all_goals simp only [List.append_assoc]` does nothing.

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

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: SerializerProofs.lean:47:37: `simp` already closes the goal

Hint: Use `simp` instead of `simpa`:
  [apply] simp

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: SerializerProofs.lean:64:2: Unused tactic linter: `all_goals try scalar_tac` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: SerializerProofs.lean:78:2: Unused tactic linter: `all_goals try scalar_tac` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: SerializerProofs.lean:92:2: Unused tactic linter: `all_goals try scalar_tac` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: SerializerProofs.lean:106:2: Unused tactic linter: `all_goals try scalar_tac` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: SerializerProofs.lean:120:2: Unused tactic linter: `all_goals try scalar_tac` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: SerializerProofs.lean:139:4: Unused tactic linter: `all_goals try scalar_tac` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: SerializerProofs.lean:160:4: Unused tactic linter: `all_goals try scalar_tac` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: SerializerProofs.lean:182:4: Unused tactic linter: `all_goals try scalar_tac` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
info: SerializerProofs.lean:260:0: 'SerializerProofs.Xoroshiro64Star_state_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SerializerProofs.lean:261:0: 'SerializerProofs.Xoroshiro64StarStar_state_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SerializerProofs.lean:262:0: 'SerializerProofs.Xoroshiro128Plus_state_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SerializerProofs.lean:263:0: 'SerializerProofs.Xoroshiro128PlusPlus_state_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SerializerProofs.lean:264:0: 'SerializerProofs.Xoroshiro128StarStar_state_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SerializerProofs.lean:266:0: 'SerializerProofs.Xoshiro128Plus_state_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SerializerProofs.lean:268:0: 'SerializerProofs.Xoshiro128PlusPlus_state_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SerializerProofs.lean:269:0: 'SerializerProofs.Xoshiro128StarStar_state_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SerializerProofs.lean:270:0: 'SerializerProofs.Xoshiro256Plus_state_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SerializerProofs.lean:271:0: 'SerializerProofs.Xoshiro256PlusPlus_state_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SerializerProofs.lean:272:0: 'SerializerProofs.Xoshiro256StarStar_state_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1815/1815] Built SerializerLoopProofs (3.5s)
warning: SerializerLoopProofs.lean:16:1: This simp argument is unused:
  core.iter.traits.iterator.IteratorSliceIter

Hint: Omit it from the simp argument list.
  [apply] simp only [core.iter.adapters.enumerate.IteratorEnumerate.next, core.slice.iter.IteratorSliceIter.next]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: SerializerLoopProofs.lean:19:32: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [h, _root_.dite_true]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: SerializerLoopProofs.lean:22:1: Unused tactic linter: `all_goals
  try (subst_vars; simp_all only [Array.length_to_slice, Array.length]; scalar_tac)` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: SerializerLoopProofs.lean:22:11: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: SerializerLoopProofs.lean:41:1: This simp argument is unused:
  core.iter.traits.iterator.IteratorSliceIter

Hint: Omit it from the simp argument list.
  [apply] simp only [core.iter.adapters.enumerate.IteratorEnumerate.next, core.slice.iter.IteratorSliceIter.next]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: SerializerLoopProofs.lean:43:15: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp [hlen, he]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: SerializerLoopProofs.lean:45:0: 'SerializerProofs.body_cont' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: SerializerLoopProofs.lean:74:43: `simp` already closes the goal

Hint: Use `simp` instead of `simpa`:
  [apply] simp

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: SerializerLoopProofs.lean:86:39: `simp` already closes the goal

Hint: Use `simp` instead of `simpa`:
  [apply] simp

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: SerializerLoopProofs.lean:99:54: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.Slice.iter, core.iter.traits.iterator.Iterator.enumerate.trait_default,
    core.iter.traits.iterator.Iterator.enumerate.default]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: SerializerLoopProofs.lean:108:0: 'SerializerProofs.loop_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SerializerLoopProofs.lean:117:0: 'SerializerProofs.Xoshiro512Plus_state_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SerializerLoopProofs.lean:118:0: 'SerializerProofs.Xoshiro512PlusPlus_state_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SerializerLoopProofs.lean:119:0: 'SerializerProofs.Xoshiro512StarStar_state_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
Build completed successfully (1815 jobs).

$ lake env lean --stdin (proofs.rs theorem/axiom audit)
proofs.rs:checked:Proofs.SplitMix64_64_spec
proofs.rs:checked:Proofs.SplitMix64_32_spec
proofs.rs:checked:Proofs.Xoroshiro128Plus_64_spec
proofs.rs:checked:Proofs.Xoroshiro128PlusPlus_64_spec
proofs.rs:checked:Proofs.Xoroshiro128StarStar_64_spec
proofs.rs:checked:Proofs.Xoroshiro64Star_32_spec
proofs.rs:checked:Proofs.Xoroshiro64StarStar_32_spec
proofs.rs:checked:Proofs.Xoshiro128Plus_32_spec
proofs.rs:checked:Proofs.Xoshiro128PlusPlus_32_spec
proofs.rs:checked:Proofs.Xoshiro128StarStar_32_spec
proofs.rs:checked:Proofs.Xoshiro256Plus_64_spec
proofs.rs:checked:Proofs.Xoshiro256PlusPlus_64_spec
proofs.rs:checked:Proofs.Xoshiro256StarStar_64_spec
proofs.rs:checked:Proofs.Xoshiro512Plus_64_spec
proofs.rs:checked:Proofs.Xoshiro512PlusPlus_64_spec
proofs.rs:checked:Proofs.Xoshiro512StarStar_64_spec
proofs.rs:checked:WrapperProofs.Xoroshiro128Plus_32_via_original_api_spec
proofs.rs:checked:WrapperProofs.Xoroshiro128PlusPlus_32_via_original_api_spec
proofs.rs:checked:WrapperProofs.Xoroshiro128StarStar_32_via_original_api_spec
proofs.rs:checked:WrapperProofs.Xoshiro256Plus_32_via_original_api_spec
proofs.rs:checked:WrapperProofs.Xoshiro256PlusPlus_32_via_original_api_spec
proofs.rs:checked:WrapperProofs.Xoshiro256StarStar_32_via_original_api_spec
proofs.rs:checked:WrapperProofs.Xoshiro512Plus_32_via_original_api_spec
proofs.rs:checked:WrapperProofs.Xoshiro512PlusPlus_32_via_original_api_spec
proofs.rs:checked:WrapperProofs.Xoshiro512StarStar_32_via_original_api_spec
proofs.rs:checked:SeedProofs.default_spec
proofs.rs:checked:SeedProofs.as_ref_spec
proofs.rs:checked:SeedProofs.as_mut_spec
proofs.rs:checked:SeedProofs.iter_spec
proofs.rs:checked:StateProofs.splitmix_state_spec
proofs.rs:checked:SerializerProofs.Xoroshiro128Plus_state_spec
proofs.rs:checked:SerializerProofs.Xoroshiro128PlusPlus_state_spec
proofs.rs:checked:SerializerProofs.Xoroshiro128StarStar_state_spec
proofs.rs:checked:SerializerProofs.Xoroshiro64Star_state_spec
proofs.rs:checked:SerializerProofs.Xoroshiro64StarStar_state_spec
proofs.rs:checked:SerializerProofs.Xoshiro128Plus_state_spec
proofs.rs:checked:SerializerProofs.Xoshiro128PlusPlus_state_spec
proofs.rs:checked:SerializerProofs.Xoshiro128StarStar_state_spec
proofs.rs:checked:SerializerProofs.Xoshiro256Plus_state_spec
proofs.rs:checked:SerializerProofs.Xoshiro256PlusPlus_state_spec
proofs.rs:checked:SerializerProofs.Xoshiro256StarStar_state_spec
proofs.rs:checked:SerializerProofs.Xoshiro512Plus_state_spec
proofs.rs:checked:SerializerProofs.Xoshiro512PlusPlus_state_spec
proofs.rs:checked:SerializerProofs.Xoshiro512StarStar_state_spec
proofs.rs:checked:RngProofs.SplitMix64_rng_32_spec
proofs.rs:checked:RngProofs.SplitMix64_rng_64_spec
proofs.rs:checked:RngProofs.Xoroshiro128Plus_rng_32_spec
proofs.rs:checked:RngProofs.Xoroshiro128Plus_rng_64_spec
proofs.rs:checked:RngProofs.Xoroshiro128PlusPlus_rng_32_spec
proofs.rs:checked:RngProofs.Xoroshiro128PlusPlus_rng_64_spec
proofs.rs:checked:RngProofs.Xoroshiro128StarStar_rng_32_spec
proofs.rs:checked:RngProofs.Xoroshiro128StarStar_rng_64_spec
proofs.rs:checked:RngProofs.Xoroshiro64Star_rng_32_spec
proofs.rs:checked:RngProofs.Xoroshiro64StarStar_rng_32_spec
proofs.rs:checked:RngProofs.Xoshiro128Plus_rng_32_spec
proofs.rs:checked:RngProofs.Xoshiro128PlusPlus_rng_32_spec
proofs.rs:checked:RngProofs.Xoshiro128StarStar_rng_32_spec
proofs.rs:checked:RngProofs.Xoshiro256Plus_rng_32_spec
proofs.rs:checked:RngProofs.Xoshiro256Plus_rng_64_spec
proofs.rs:checked:RngProofs.Xoshiro256PlusPlus_rng_32_spec
proofs.rs:checked:RngProofs.Xoshiro256PlusPlus_rng_64_spec
proofs.rs:checked:RngProofs.Xoshiro256StarStar_rng_32_spec
proofs.rs:checked:RngProofs.Xoshiro256StarStar_rng_64_spec
proofs.rs:checked:RngProofs.Xoshiro512Plus_rng_32_spec
proofs.rs:checked:RngProofs.Xoshiro512Plus_rng_64_spec
proofs.rs:checked:RngProofs.Xoshiro512PlusPlus_rng_32_spec
proofs.rs:checked:RngProofs.Xoshiro512PlusPlus_rng_64_spec
proofs.rs:checked:RngProofs.Xoshiro512StarStar_rng_32_spec
proofs.rs:checked:RngProofs.Xoshiro512StarStar_rng_64_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_xoshiro 0.8.1 Rust sources and Cargo.toml, archive-compared unchanged. Rust nightly-2026-09-17; Charon 08d7c9d50144bd84848212c24701253585e90d1f; official Aeneas frontend/library be86ab0f1989d04944292b345b24c435be3ad10a; Lean 4.35.0. Official targeted extraction selects all sixteen original bodies, with macro-expanded transitions. Original tests, regeneration hashes, integrated build and transitive theorem audits are retained in evidence. Separate all-features (serde) extraction is retained in evidence/serde; generated Lean is byte-identical to the default extraction. For the nine selection-only forwarding callers, official Charon optimized MIR with mir-opt-level=4 and +Inline is used, with duplicate-defaulted-methods and remove-unused-self-clauses. Original dependency bodies retain dependency MIR. No original Rust source or Cargo manifest is changed. Path remapping affects provenance spelling only. A third official targeted extraction covers the four Seed512 bodies; default and serde generated Types/Funs are byte-identical and have no unknown externals. The additional fifteen-serializer original-root extraction is non-monomorphized, uses the official distinct XoshiroSerializationModel namespace, and has byte-identical default/serde Types/Funs. Fourteen claims are added; existing SplitMix64::state is retained without duplicate registration. Full LLBC traversal and all generated modules restrict custom size_of uses to five U32 and six U64 calls per configuration; the only custom external template declaration is size_of. All six claim modules are simultaneously imported and all theorem dependencies audited. External blanket opt-in: exact25 rand_core0.10.1 specializations, checksum-pinned source closure, CLI-owned independent compiler capture in default and serde configurations; exact singleton observations. CLI032640e536faffa600f4345b14cc51b40d827c322745d286b225858d84612d68. evidence/kani-seed512-constructor retains immutable producer hashes, exact lock, full commands/solver pins, two raw successful logs (33+51=84checks,0failed,4unreachable) and independent review. Cargo.producer.toml preserves the executed dependency location; only the portable manifest path changes to the archive-identical artifact root. This packaging performs no new solver run.

What is trusted

The Rust compiler, official Charon/Aeneas translation, official Aeneas array/scalar models and Lean kernel are trusted. No source adaptations or local helper axioms are used. Eleven newly covered two/four-word state serializers use a custom executable size_of model with explicit layout evidence only for U32=4 and U64=8 bytes. The original generated Types/Funs remain byte-for-byte official outputs. The Lean evidence class is open; this packet supplies exactly these two primitive instances and guards all eleven generated calls and their frozen elaborated instance bindings. Bool and array types have no supplied evidence and are rejected. This is not a universal type-layout theorem. The three eight-word serializers do not call size_of. Archived independent Kani layout checks confirm the Rust u32/u64 sizes under nightly-2026-08-21; Aeneas extraction uses nightly-2026-09-17. ABI agreement across those compilers and correspondence of Rust layout to the Lean evidence remains an explicit, non-mechanical model bridge. All API and supplementary direct/selector theorems have dependency audits permitting only propext, Classical.choice and Quot.sound. Standard shifts, rotations, wrapping arithmetic and array operations use official Aeneas models, rather than body proofs of Rust std implementations. The nine selector proofs additionally rely on Rust compiler inlining of the exact original API call; retained MIR scopes identify each original TryRng method and Rng wrapper. The selector does not replace or assume an opaque original API: generated native callees are body-proved and no unknown external definitions remain. Seed512 byte-view and iterator initialization proofs use the official array-to-slice and slice-iterator models. The mutable reference model specifies write-back of the fixed-length referent; resizing that referent is not a legal returned-slice operation in safe Rust. The Seed512 constructor supplement separately trusts pinned Kani0.68/CBMC/Z3, its August Rust/compiler memory semantics, exact rand_core0.10.1 and default x86_64 configuration. Enabled unwind70 covers all64-byte comparison/copy loops, without disabled checks, observer, private injection, model or original-source adaptation.

Technical limitations

The 69 mapped contracts comprise 35 direct bodies and 34 compiler-inlined original calls, including exactly 25 external blanket specializations. The five 32-bit-engine try_next_u64 compositions and corresponding external Rng::next_u64 specializations remain outside these Aeneas claims. Seed construction, buffer filling, jump/long_jump, Debug/formatting, serde implementations and other inherited/default/blanket methods are not completed. Seed512 iterator initialization does not prove iterator operation bodies. Serializer layout dictionaries cover only the frozen U32/U64 use closure; arbitrary type layout is not established. Separate Kani seed/state/composition evidence has its own documented compiler and domain boundaries. No seed reachability, period, distribution, independence or cryptographic property follows from these transition formulas. Other targets and feature/dependency combinations are not covered. The constructor check covers the complete64-byte input and replacement domains under that concrete default configuration. It does not establish arbitrary external aliasing, heap/provenance, physical address identity, serde, manual Debug, other targets/configurations or general Rust memory safety. Constructing this public tuple is a data operation; no additional function/source card is invented, and all69 primary mappings 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.

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 · optional—

Comments (0)

No comments.