Report #25 — Integer state transitions and exact range traces with float supplements

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

20 verified claims · 0 findings

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

nyuichi · 2026-11-05 01:07 UTC

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

Overview

For oorandom 11.1.5, twelve original integer/state APIs have exact value/state proofs for every scalar input, including zero states and even restored increments. For both Rand32 and Rand64, new_inc sets increment to ((input_increment << 1) OR 1), advances from zero, adds the seed with wrapping arithmetic, then advances again; new uses DEFAULT_INC. state and from_state preserve the complete state/increment pair, with save/restore identity. Unsigned generation returns the specified PCG-XSH-RR permutation of the old state and advances to multiplier*state+increment modulo the state width. Signed generation returns the same output bits interpreted as i32/i64 and preserves that updated state. These calls terminate normally in the extracted model.

Separate Kani results cover both original rand_float methods for every complete state/increment pair. They return exactly n/2^24 or n/2^53, where n is the top24 or53 bits of the corresponding unsigned word, with the exact independent IEEE encoding and a value in [0,1). Their complete poststate equals an actual unsigned-word call. This follows from successful original-float/helper and all-word/helper specifications on the identical Rust helper; a direct Rand32 check independently confirms the same contract. State equality alone is not a call-count proof; original source/LLBC observations separately identify the sole word call.

Both original rand_range methods now have exact trace contracts in the extracted debug model. For valid width=end-start, each candidate consumes the next actual PCG word and advances the actual generator. If candidate n is accepted and every earlier candidate rejects against the proved canonical threshold, sampling returns exactly floor(product_n/2^b)+start and the candidate state after n+1 words, where b is32 or64. If every candidate rejects, it diverges. The classical first-accepted-or-all-rejected case split is exhaustive, not an executable termination decision. The specification’s auxiliary typed width must equal end.val-start.val. Invalid start>=end ranges produce assertion failure. Prior no-failure/normal-return bounds/increment preservation and the publicly restored(0,0) range0..3 divergence result remain included; constructor reachability of that pair is not claimed.

Additional Kani checks establish From<Self>, Borrow<Self> and BorrowMut<Self> identity and mutable replacement propagation for every public state/inc pair; Any matches its own TypeId and distinguishes Rand32 from Rand64 without changing state. CloneToUninit preserves the source and copies its complete state into a distinct valid aligned MaybeUninit stack slot.

Six generic conversion families have conditional original-body Lean contracts: Into delegates to From; TryInto forwards the complete TryFrom result; blanket TryFrom delegates to Into and wraps a normal result in Ok. Modeled failure/divergence propagate. These require the actual Rust trait bounds and matching dictionaries, not arbitrary conversion correctness or termination. TryFrom uses official generation; the four Into/TryInto owner specializations additionally use a separately pinned finite export-only translator patch, with the trust boundary below.

Findings (0)

No findings reported.

APIs (20)

Associated functions

`impl Rand32`

pub fn from_state(state: (u64, u64)) -> Self

Claim #4

pub fn new(seed: u64) -> Self

Claim #6

pub fn new_inc(seed: u64, increment: u64) -> Self

Claim #5

`impl Rand64`

pub fn from_state(state: (u128, u128)) -> Self

Claim #10

pub fn new(seed: u128) -> Self

Claim #12

pub fn new_inc(seed: u128, increment: u128) -> Self

Claim #11

Methods

`impl Rand32`

pub fn rand_i32(self: &mut Self) -> i32

Claim #2

pub fn rand_range(self: &mut Self, range: Range<u32>) -> u32

Claim #13

pub fn rand_u32(self: &mut Self) -> u32

Claim #1

pub fn state(self: &Self) -> (u64, u64)

Claim #3

`impl Rand64`

pub fn rand_i64(self: &mut Self) -> i64

Claim #8

pub fn rand_range(self: &mut Self, range: Range<u64>) -> u64

Claim #14

pub fn rand_u64(self: &mut Self) -> u64

Claim #7

pub fn state(self: &Self) -> (u128, u128)

Claim #9

Recorded callables

<oorandom::Rand32 as core::convert::Into>::into recorded callable · signature and safety not recorded

Claim #17

<oorandom::Rand32 as core::convert::TryFrom>::try_from recorded callable · signature and safety not recorded

Claim #18

<oorandom::Rand32 as core::convert::TryInto>::try_into recorded callable · signature and safety not recorded

Claim #15

<oorandom::Rand64 as core::convert::Into>::into recorded callable · signature and safety not recorded

Claim #16

<oorandom::Rand64 as core::convert::TryFrom>::try_from recorded callable · signature and safety not recorded

Claim #19

<oorandom::Rand64 as core::convert::TryInto>::try_into recorded callable · signature and safety not recorded

Claim #20

Evidence

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

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/nyuichi/rust-crate-proofs report-25-source-1
git -C report-25-source-1 checkout --detach 9df6f1a32a5521c68fe6807ba1de8596214dc849
git -C report-25-source-1 submodule update --init --recursive --checkout
cd report-25-source-1/oorandom/11.1.5/aeneas/2026-11-05/proofs

lake build +ExactRange +GenericConversionProofs +OriginalDelegationProofs +Proofs

printf '%s' 'import Lean
import ExactRange
import GenericConversionProofs
import OriginalDelegationProofs
import Proofs
open Lean Elab Command

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

run_cmd do
  let theorem_name := `OriginalDelegationProofs.rand64_try_into
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: OriginalDelegationProofs.rand64_try_into"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in OriginalDelegationProofs.rand64_try_into: {ax}"
  liftIO <| IO.println "proofs.rs:checked:OriginalDelegationProofs.rand64_try_into"
' | 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 · 20 checks passed · 0 failed

2026-11-05T15:43:35.587020956+00:00 · 117.4 seconds · Exit code 0

Recorded on the author’s machine.

Check	Result	Claim
Lean checked theorem Proofs.rand_u32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.rand_u32_spec`	Passed	Claim #1
Lean checked theorem Proofs.rand_i32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.rand_i32_spec`	Passed	Claim #2
Lean checked theorem Proofs.state32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.state32_spec`	Passed	Claim #3
Lean checked theorem Proofs.from_state32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.from_state32_spec`	Passed	Claim #4
Lean checked theorem Proofs.new_inc32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.new_inc32_spec`	Passed	Claim #5
Lean checked theorem Proofs.new32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.new32_spec`	Passed	Claim #6
Lean checked theorem Proofs.rand_u64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.rand_u64_spec`	Passed	Claim #7
Lean checked theorem Proofs.rand_i64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.rand_i64_spec`	Passed	Claim #8
Lean checked theorem Proofs.state64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.state64_spec`	Passed	Claim #9
Lean checked theorem Proofs.from_state64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.from_state64_spec`	Passed	Claim #10
Lean checked theorem Proofs.new_inc64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.new_inc64_spec`	Passed	Claim #11
Lean checked theorem Proofs.new64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.new64_spec`	Passed	Claim #12
Lean checked theorem ExactRange.rand32_contract; axioms limited to propext, Classical.choice, Quot.sound `ExactRange.rand32_contract`	Passed	Claim #13
Lean checked theorem ExactRange.rand64_contract; axioms limited to propext, Classical.choice, Quot.sound `ExactRange.rand64_contract`	Passed	Claim #14
Lean checked theorem OriginalDelegationProofs.rand32_try_into; axioms limited to propext, Classical.choice, Quot.sound `OriginalDelegationProofs.rand32_try_into`	Passed	Claim #15
Lean checked theorem OriginalDelegationProofs.rand64_into; axioms limited to propext, Classical.choice, Quot.sound `OriginalDelegationProofs.rand64_into`	Passed	Claim #16
Lean checked theorem OriginalDelegationProofs.rand32_into; axioms limited to propext, Classical.choice, Quot.sound `OriginalDelegationProofs.rand32_into`	Passed	Claim #17
Lean checked theorem GenericConversions.rand32_try_from; axioms limited to propext, Classical.choice, Quot.sound `GenericConversions.rand32_try_from`	Passed	Claim #18
Lean checked theorem GenericConversions.rand64_try_from; axioms limited to propext, Classical.choice, Quot.sound `GenericConversions.rand64_try_from`	Passed	Claim #19
Lean checked theorem OriginalDelegationProofs.rand64_try_into; axioms limited to propext, Classical.choice, Quot.sound `OriginalDelegationProofs.rand64_try_into`	Passed	Claim #20

Execution details

Started: 2026-11-05T15:43:35.587020956+00:00
Finished: 2026-11-05T15:45:33.024972279+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: oorandom/11.1.5/aeneas/2026-11-05/proofs
Environment overrides: None recorded
Git repository: https://github.com/nyuichi/rust-crate-proofs
Git commit: 9df6f1a32a5521c68fe6807ba1de8596214dc849

Diagnostics & logs

=== stdout ===
⚠ [1795/1821] Built NatRangeArithmetic (1.4s)
warning: NatRangeArithmetic.lean: imports `Mathlib.Data.Nat.Basic` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
info: NatRangeArithmetic.lean:19:0: 'NatRangeArithmetic.product_bound' depends on axioms: [propext]
info: NatRangeArithmetic.lean:20:0: 'NatRangeArithmetic.offset_bound' depends on axioms: [propext]
✔ [1797/1823] Built OorandomRangeOriginal.Types (3.1s)
✔ [1798/1823] Built Generated.CoreConversions (3.0s)
✔ [1799/1823] Built Oorandom (3.2s)
ℹ [1800/1823] Built GenericTrace (3.9s)
info: GenericTrace.lean:54:0: 'GenericTrace.finite' depends on axioms: [propext, Classical.choice, Quot.sound]
info: GenericTrace.lean:55:0: 'GenericTrace.infinite' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [1801/1823] Built GeneratedDelegations.CoreDelegations (2.9s)
✔ [1802/1823] Built OorandomRangeOriginal.Funs (2.7s)
ℹ [1803/1823] Built RangeArithmetic (2.9s)
info: RangeArithmetic.lean:56:0: 'RangeArithmetic.product32' depends on axioms: [propext]
info: RangeArithmetic.lean:57:0: 'RangeArithmetic.product64' depends on axioms: [propext]
info: RangeArithmetic.lean:58:0: 'RangeArithmetic.wrapping_product32' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RangeArithmetic.lean:59:0: 'RangeArithmetic.offset32' depends on axioms: [propext]
info: RangeArithmetic.lean:60:0: 'RangeArithmetic.offset64' depends on axioms: [propext]
✔ [1804/1823] Built GenericConversionProofs (2.0s)
✔ [1805/1823] Built OriginalDelegationProofs (2.7s)
⚠ [1806/1823] Built NegBridge (2.5s)
warning: NegBridge.lean:9:14: `if_neg` has been deprecated: Use `ite_eq_right` instead

Hint: Replace the deprecated name:
  i̵f̵_̵n̵e̵g̵i̲t̲e̲_̲e̲q̲_̲r̲i̲g̲h̲t̲
info: NegBridge.lean:19:0: 'NegBridge.u32_existing_sub' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NegBridge.lean:20:0: 'NegBridge.u64_existing_sub' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NegBridge.lean:21:0: 'NegBridge.u32_math' depends on axioms: [propext, Quot.sound]
info: NegBridge.lean:22:0: 'NegBridge.u64_math' depends on axioms: [propext, Quot.sound]
ℹ [1807/1823] Built PartialLoop (2.6s)
info: PartialLoop.lean:22:0: 'PartialLoop.loop_dspec' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1808/1823] Built Checkpoint (2.9s)
warning: Checkpoint.lean:30:10: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Checkpoint.lean:30:14: Unused tactic linter: `rfl` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Checkpoint.lean:30:14: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Checkpoint.lean:88:36: `simp` already closes the goal

Hint: Use `simp` instead of `simpa`:
  [apply] simp only [WP.spec_vis] at h

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Checkpoint.lean:89:32: `simp` already closes the goal

Hint: Use `simp` instead of `simpa`:
  [apply] simp only [WP.spec_div] at h

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
info: Checkpoint.lean:108:0: 'RangeProofs.zero32_step' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Checkpoint.lean:109:0: 'RangeProofs.zero32_body' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Checkpoint.lean:111:0: 'RangeProofs.loop_self_div' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Checkpoint.lean:112:0: 'RangeProofs.zero32_loop_div' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Checkpoint.lean:115:0: 'RangeProofs.prefix32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1809/1823] Built FullRange (2.4s)
warning: FullRange.lean:11:63: This simp argument is unused:
  Std.bind_assoc_eq

Hint: Omit it from the simp argument list.
  [apply] simp only [Rand32.rand_range, prefix32, finish32, Std.bind_assoc, bind_ok, bind_tc_ok, Std.uncurry]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FullRange.lean:11:89: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [Rand32.rand_range, prefix32, finish32, Std.bind_assoc, Std.bind_assoc_eq, bind_ok, Std.uncurry]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FullRange.lean:12:25: Unused tactic linter: `simp only [Std.bind_assoc, bind_ok, bind_tc_ok, Std.uncurry]` does nothing.

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

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: FullRange.lean:17:12: `if_pos` has been deprecated: Use `ite_eq_left` instead

Hint: Replace the deprecated name:
  i̵f̵_̵p̵o̵s̵i̲t̲e̲_̲e̲q̲_̲l̲e̲f̲t̲
info: FullRange.lean:21:0: 'FullRange.zero32_public_div' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1810/1823] Built RangePartial32 (2.4s)
warning: RangePartial32.lean:27:22: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, Std.uncurry, lift]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangePartial32.lean:49:14: This simp argument is unused:
  Std.uncurry

Hint: Omit it from the simp argument list.
  [apply] simp only

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: RangePartial32.lean:54:0: 'RangePartial32.body_safe' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RangePartial32.lean:55:0: 'RangePartial32.loop_safe' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1811/1823] Built Zero64 (2.7s)
warning: Zero64.lean:23:20: This simp argument is unused:
  Std.uncurry

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Zero64.lean:28:9: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Zero64.lean:28:13: Unused tactic linter: `rfl` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Zero64.lean:28:13: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Zero64.lean:37:36: This simp argument is unused:
  core.num.U128.wrapping_mul

Hint: Omit it from the simp argument list.
  [apply] simp [Rand64.rand_range_loop.body, zero_step, lift, Std.uncurry, core.convert.num.FromU128U64.from,
    UScalar.cast, HAnd.hAnd, UScalar.and, UScalar.wrapping_mul]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Zero64.lean:38:24: This simp argument is unused:
  UScalar.wrapping_mul

Hint: Omit it from the simp argument list.
  [apply] simp [Rand64.rand_range_loop.body, zero_step, lift, Std.uncurry, core.convert.num.FromU128U64.from,
    core.num.U128.wrapping_mul, UScalar.cast, HAnd.hAnd, UScalar.and]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Zero64.lean:89:71: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [Rand64.rand_range, prefix64, finish64, Std.bind_assoc, bind_ok, Std.uncurry]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Zero64.lean:95:12: `if_pos` has been deprecated: Use `ite_eq_left` instead

Hint: Replace the deprecated name:
  i̵f̵_̵p̵o̵s̵i̲t̲e̲_̲e̲q̲_̲l̲e̲f̲t̲
info: Zero64.lean:99:0: 'Zero64.next_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Zero64.lean:100:0: 'Zero64.public_div' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1812/1823] Built RangeComplete32 (2.6s)
warning: RangeComplete32.lean:22:20: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, Std.uncurry, lift]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangeComplete32.lean:25:12: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_tc_ok, Std.uncurry, lift, WP.spec_ok, RangePartial32.Inv]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangeComplete32.lean:25:20: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, Std.uncurry, lift, WP.spec_ok, RangePartial32.Inv]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangeComplete32.lean:25:31: This simp argument is unused:
  Std.uncurry

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, bind_tc_ok, lift, WP.spec_ok, RangePartial32.Inv]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangeComplete32.lean:25:43: This simp argument is unused:
  lift

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, bind_tc_ok, Std.uncurry, WP.spec_ok, RangePartial32.Inv]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangeComplete32.lean:55:25: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [lift, bind_ok]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangeComplete32.lean:97:67: This simp argument is unused:
  Std.bind_assoc_eq

Hint: Omit it from the simp argument list.
  [apply] simp only [Rand32.rand_range, draw, afterDraw, finish, Std.bind_assoc, bind_ok, bind_tc_ok, Std.uncurry]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangeComplete32.lean:97:93: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [Rand32.rand_range, draw, afterDraw, finish, Std.bind_assoc, Std.bind_assoc_eq, bind_ok,
    Std.uncurry]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangeComplete32.lean:98:25: Unused tactic linter: `simp only [Std.bind_assoc, bind_ok, bind_tc_ok, Std.uncurry]` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: RangeComplete32.lean:98:25: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: RangeComplete32.lean:106:20: `if_pos` has been deprecated: Use `ite_eq_left` instead

Hint: Replace the deprecated name:
  i̵f̵_̵p̵o̵s̵i̲t̲e̲_̲e̲q̲_̲l̲e̲f̲t̲
warning: RangeComplete32.lean:106:41: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [massert, if_pos valid, bind_ok]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: RangeComplete32.lean:114:0: 'RangeComplete32.public_valid_partial' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RangeComplete32.lean:115:0: 'RangeComplete32.afterDraw_safe' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RangeComplete32.lean:116:0: 'RangeComplete32.finish_safe' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RangeComplete32.lean:117:0: 'RangeComplete32.draw_safe' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1813/1823] Built PublicDomain (2.6s)
info: PublicDomain.lean:23:0: 'PublicDomain.from_state32_range3_div' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PublicDomain.lean:24:0: 'PublicDomain.from_state64_range3_div' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PublicDomain.lean:25:0: 'PublicDomain.range32_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PublicDomain.lean:26:0: 'PublicDomain.range64_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1814/1823] Built RangePartial64 (2.7s)
warning: RangePartial64.lean:27:22: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, Std.uncurry, lift]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangePartial64.lean:30:14: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_tc_ok, Std.uncurry, lift, WP.spec_ok, Inv]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangePartial64.lean:30:22: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, Std.uncurry, lift, WP.spec_ok, Inv]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangePartial64.lean:30:33: This simp argument is unused:
  Std.uncurry

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, bind_tc_ok, lift, WP.spec_ok, Inv]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangePartial64.lean:30:45: This simp argument is unused:
  lift

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, bind_tc_ok, Std.uncurry, WP.spec_ok, Inv]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangePartial64.lean:51:14: This simp argument is unused:
  Std.uncurry

Hint: Omit it from the simp argument list.
  [apply] simp only

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: RangePartial64.lean:56:0: 'RangePartial64.body_safe' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RangePartial64.lean:57:0: 'RangePartial64.loop_safe' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1815/1823] Built ActualLoop32 (2.5s)
warning: ActualLoop32.lean:22:22: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, lift, Std.uncurry, next]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ActualLoop32.lean:37:7: `if_pos` has been deprecated: Use `ite_eq_left` instead

Hint: Replace the deprecated name:
  i̵f̵_̵p̵o̵s̵i̲t̲e̲_̲e̲q̲_̲l̲e̲f̲t̲
warning: ActualLoop32.lean:38:21: `if_neg` has been deprecated: Use `ite_eq_right` instead

Hint: Replace the deprecated name:
  i̵f̵_̵n̵e̵g̵i̲t̲e̲_̲e̲q̲_̲r̲i̲g̲h̲t̲
warning: ActualLoop32.lean:51:7: `if_pos` has been deprecated: Use `ite_eq_left` instead

Hint: Replace the deprecated name:
  i̵f̵_̵p̵o̵s̵i̲t̲e̲_̲e̲q̲_̲l̲e̲f̲t̲
info: ActualLoop32.lean:54:0: 'ActualLoop32.infinite' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ActualLoop32.lean:55:0: 'ActualLoop32.body_equation' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ActualLoop32.lean:56:0: 'ActualLoop32.finite' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1816/1823] Built RangeComplete64 (2.8s)
warning: RangeComplete64.lean:22:20: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, Std.uncurry, lift]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangeComplete64.lean:25:12: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_tc_ok, Std.uncurry, lift, WP.spec_ok, RangePartial64.Inv]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangeComplete64.lean:25:20: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, Std.uncurry, lift, WP.spec_ok, RangePartial64.Inv]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangeComplete64.lean:25:31: This simp argument is unused:
  Std.uncurry

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, bind_tc_ok, lift, WP.spec_ok, RangePartial64.Inv]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangeComplete64.lean:25:43: This simp argument is unused:
  lift

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, bind_tc_ok, Std.uncurry, WP.spec_ok, RangePartial64.Inv]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangeComplete64.lean:55:25: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [lift, bind_ok]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangeComplete64.lean:100:83: This simp argument is unused:
  Std.bind_assoc_eq

Hint: Omit it from the simp argument list.
  [apply] simp only [Rand64.rand_range, draw, afterDraw, finish, wrapping_bridge, Std.bind_assoc, bind_ok, bind_tc_ok,
    Std.uncurry]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangeComplete64.lean:100:109: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [Rand64.rand_range, draw, afterDraw, finish, wrapping_bridge, Std.bind_assoc, Std.bind_assoc_eq,
    bind_ok, Std.uncurry]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: RangeComplete64.lean:101:25: Unused tactic linter: `simp only [Std.bind_assoc, bind_ok, bind_tc_ok, Std.uncurry]` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: RangeComplete64.lean:101:25: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: RangeComplete64.lean:109:20: `if_pos` has been deprecated: Use `ite_eq_left` instead

Hint: Replace the deprecated name:
  i̵f̵_̵p̵o̵s̵i̲t̲e̲_̲e̲q̲_̲l̲e̲f̲t̲
warning: RangeComplete64.lean:109:41: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [massert, if_pos valid, bind_ok]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: RangeComplete64.lean:117:0: 'RangeComplete64.public_valid_partial' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RangeComplete64.lean:118:0: 'RangeComplete64.afterDraw_safe' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RangeComplete64.lean:119:0: 'RangeComplete64.finish_safe' depends on axioms: [propext, Classical.choice, Quot.sound]
info: RangeComplete64.lean:120:0: 'RangeComplete64.draw_safe' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1817/1823] Built EstablishedRange (2.1s)
info: EstablishedRange.lean:19:0: 'EstablishedRange.rand32_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: EstablishedRange.lean:20:0: 'EstablishedRange.rand64_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1818/1823] Built PublicTrace32 (2.8s)
warning: PublicTrace32.lean:21:20: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, lift, Std.uncurry, hm, initial, ActualLoop32.next]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PublicTrace32.lean:61:25: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [lift, bind_ok]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PublicTrace32.lean:99:20: `if_pos` has been deprecated: Use `ite_eq_left` instead

Hint: Replace the deprecated name:
  i̵f̵_̵p̵o̵s̵i̲t̲e̲_̲e̲q̲_̲l̲e̲f̲t̲
warning: PublicTrace32.lean:99:41: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [massert, if_pos valid, bind_ok, hsub]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PublicTrace32.lean:109:98: `if_true` has been deprecated: Use `ite_true` instead

Hint: Replace the deprecated name:
  i̵f̵_̵t̵r̵u̵e̵i̲t̲e̲_̲t̲r̲u̲e̲
warning: PublicTrace32.lean:148:20: `if_pos` has been deprecated: Use `ite_eq_left` instead

Hint: Replace the deprecated name:
  i̵f̵_̵p̵o̵s̵i̲t̲e̲_̲e̲q̲_̲l̲e̲f̲t̲
warning: PublicTrace32.lean:158:5: `if_pos` has been deprecated: Use `ite_eq_left` instead

Hint: Replace the deprecated name:
  i̵f̵_̵p̵o̵s̵i̲t̲e̲_̲e̲q̲_̲l̲e̲f̲t̲
warning: PublicTrace32.lean:148:41: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [massert, if_pos valid, bind_ok, hsub]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: PublicTrace32.lean:165:0: 'PublicTrace32.public_all_rejected' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PublicTrace32.lean:166:0: 'PublicTrace32.threshold_value' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PublicTrace32.lean:167:0: 'PublicTrace32.public_first_accept' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PublicTrace32.lean:168:0: 'PublicTrace32.public_finite' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PublicTrace32.lean:169:0: 'PublicTrace32.finish_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PublicTrace32.lean:170:0: 'PublicTrace32.initial_draw' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PublicTrace32.lean:171:0: 'PublicTrace32.afterDraw_finite' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1819/1823] Built ActualLoop64 (2.3s)
warning: ActualLoop64.lean:36:22: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, lift, Std.uncurry]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ActualLoop64.lean:38:22: This simp argument is unused:
  lift

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, Std.uncurry, next]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ActualLoop64.lean:38:27: This simp argument is unused:
  Std.uncurry

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, lift, next]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ActualLoop64.lean:53:7: `if_pos` has been deprecated: Use `ite_eq_left` instead

Hint: Replace the deprecated name:
  i̵f̵_̵p̵o̵s̵i̲t̲e̲_̲e̲q̲_̲l̲e̲f̲t̲
warning: ActualLoop64.lean:54:36: `if_neg` has been deprecated: Use `ite_eq_right` instead

Hint: Replace the deprecated name:
  i̵f̵_̵n̵e̵g̵i̲t̲e̲_̲e̲q̲_̲r̲i̲g̲h̲t̲
warning: ActualLoop64.lean:67:7: `if_pos` has been deprecated: Use `ite_eq_left` instead

Hint: Replace the deprecated name:
  i̵f̵_̵p̵o̵s̵i̲t̲e̲_̲e̲q̲_̲l̲e̲f̲t̲
info: ActualLoop64.lean:70:0: 'ActualLoop64.infinite' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ActualLoop64.lean:71:0: 'ActualLoop64.body_equation' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ActualLoop64.lean:72:0: 'ActualLoop64.finite' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1820/1823] Built PublicTrace64 (2.4s)
warning: PublicTrace64.lean:21:20: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_ok, lift, Std.uncurry, hm, initial, ActualLoop64.next]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PublicTrace64.lean:61:25: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [lift, bind_ok]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PublicTrace64.lean:99:20: `if_pos` has been deprecated: Use `ite_eq_left` instead

Hint: Replace the deprecated name:
  i̵f̵_̵p̵o̵s̵i̲t̲e̲_̲e̲q̲_̲l̲e̲f̲t̲
warning: PublicTrace64.lean:99:41: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [massert, if_pos valid, bind_ok, hsub]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PublicTrace64.lean:109:98: `if_true` has been deprecated: Use `ite_true` instead

Hint: Replace the deprecated name:
  i̵f̵_̵t̵r̵u̵e̵i̲t̲e̲_̲t̲r̲u̲e̲
warning: PublicTrace64.lean:148:20: `if_pos` has been deprecated: Use `ite_eq_left` instead

Hint: Replace the deprecated name:
  i̵f̵_̵p̵o̵s̵i̲t̲e̲_̲e̲q̲_̲l̲e̲f̲t̲
warning: PublicTrace64.lean:158:5: `if_pos` has been deprecated: Use `ite_eq_left` instead

Hint: Replace the deprecated name:
  i̵f̵_̵p̵o̵s̵i̲t̲e̲_̲e̲q̲_̲l̲e̲f̲t̲
warning: PublicTrace64.lean:148:41: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [massert, if_pos valid, bind_ok, hsub]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: PublicTrace64.lean:165:0: 'PublicTrace64.public_all_rejected' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PublicTrace64.lean:166:0: 'PublicTrace64.threshold_value' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PublicTrace64.lean:167:0: 'PublicTrace64.public_first_accept' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PublicTrace64.lean:168:0: 'PublicTrace64.public_finite' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PublicTrace64.lean:169:0: 'PublicTrace64.finish_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PublicTrace64.lean:170:0: 'PublicTrace64.initial_draw' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PublicTrace64.lean:171:0: 'PublicTrace64.afterDraw_finite' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1821/1823] Built TraceAudit (1.9s)
info: TraceAudit.lean:16:0: 'TraceAudit.first_or_none' depends on axioms: [propext, Classical.choice, Quot.sound]
info: TraceAudit.lean:17:0: 'PublicTrace32.public_first_accept' depends on axioms: [propext, Classical.choice, Quot.sound]
info: TraceAudit.lean:18:0: 'PublicTrace64.public_first_accept' depends on axioms: [propext, Classical.choice, Quot.sound]
info: TraceAudit.lean:19:0: 'PublicTrace32.public_all_rejected' depends on axioms: [propext, Classical.choice, Quot.sound]
info: TraceAudit.lean:20:0: 'PublicTrace64.public_all_rejected' depends on axioms: [propext, Classical.choice, Quot.sound]
info: TraceAudit.lean:21:0: 'PublicDomain.range32_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: TraceAudit.lean:22:0: 'PublicDomain.range64_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1822/1823] Built ExactRange (2.2s)
info: ExactRange.lean:21:0: 'ExactRange.rand32_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ExactRange.lean:38:0: 'ExactRange.rand64_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1823/1823] Built Proofs (2.3s)
info: Proofs.lean:115:0: 'Proofs.rand_u32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:116:0: 'Proofs.rand_i32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:117:0: 'Proofs.state32_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:118:0: 'Proofs.from_state32_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:119:0: 'Proofs.restore32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:120:0: 'Proofs.new_inc32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:121:0: 'Proofs.new32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:122:0: 'Proofs.rand_u64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:123:0: 'Proofs.rand_i64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:124:0: 'Proofs.state64_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:125:0: 'Proofs.from_state64_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:126:0: 'Proofs.restore64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:127:0: 'Proofs.new_inc64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:128:0: 'Proofs.new64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
Build completed successfully (1823 jobs).

$ lake env lean --stdin (proofs.rs theorem/axiom audit)
proofs.rs:checked:Proofs.rand_u32_spec
proofs.rs:checked:Proofs.rand_i32_spec
proofs.rs:checked:Proofs.state32_spec
proofs.rs:checked:Proofs.from_state32_spec
proofs.rs:checked:Proofs.new_inc32_spec
proofs.rs:checked:Proofs.new32_spec
proofs.rs:checked:Proofs.rand_u64_spec
proofs.rs:checked:Proofs.rand_i64_spec
proofs.rs:checked:Proofs.state64_spec
proofs.rs:checked:Proofs.from_state64_spec
proofs.rs:checked:Proofs.new_inc64_spec
proofs.rs:checked:Proofs.new64_spec
proofs.rs:checked:ExactRange.rand32_contract
proofs.rs:checked:ExactRange.rand64_contract
proofs.rs:checked:OriginalDelegationProofs.rand32_try_into
proofs.rs:checked:OriginalDelegationProofs.rand64_into
proofs.rs:checked:OriginalDelegationProofs.rand32_into
proofs.rs:checked:GenericConversions.rand32_try_from
proofs.rs:checked:GenericConversions.rand64_try_from
proofs.rs:checked:OriginalDelegationProofs.rand64_try_into

=== 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 oorandom 11.1.5 src/Cargo.toml, archive-compared without changes. Rust nightly-2026-09-17; Charon 08d7c9d50144bd84848212c24701253585e90d1f; official Aeneas frontend/library be86ab0f1989d04944292b345b24c435be3ad10a; Lean 4.35.0. Official targeted extraction selects all twelve original bodies and their shared callees. Original tests, regeneration hashes and integrated Lean/axiom audits are retained in evidence. Separate Kani0.68/nightly2026-08-21: floatA32/A64Z3 each66checks0fail and allwordB32/B64 each11checks0fail, with immutable COMPOSITION/source-normalization evidence; external6 twojobs34each and external4 Any39each/CloneToUninit42each. Exact std08 source followup and old timeout/review records retained. Supplemental packaging relocates an original dependency or changes a manifest path only and is not a new solver run. Direct Rand32 Z3 reinforcement72checks/0fail; direct Rand64 alternative60s timeout retained, no further retry. Partial original range supplement in evidence/range-established and proofs/EstablishedRange: official nonmonomorphic extraction, original wrapping_neg2 included transparently, opaque0/provider0/newmodels0. Original frozen packet preserved; official-subdir output and import-only proof adaptation recorded. Supplemental libraries imported with the12 primary proofs. The stronger44-file range-partial freeze supersedes the minimum38-file supplemental theorem while preserving it as history;15 source modules are compiled together with the original12 proof module. Conditional generic6 packet: two official TryFrom bodies plus four finite-export Into/TryInto owner specializations,28 named theorems/helpers coimported with standard axioms; patch963996393e9f9c67106e2dd64a9cc2a4fb48f9ec06f5aeb127c568f6a79defd1/rawbinary96e2e328ec0b5a2e53599474ded998b450311f5d4fdf828b39b422885b03bb9b, reproducible snapshot in evidence/conditional-generic6. The six generic external families use finite compiler-owned source/body observations, giving twenty machine contracts under the stated bounds and trust conditions. Exact-range trace final116-file freeze2421cdf9e13e06519d1d45995d3bff786b96ecbd298b12e1dac9747f58c789f7 independently reviewed;22 bounded module jobs/rawlogs have63 unique audited declarations in aggregate, not63 from one finalcoimport. ExactRange2 map to original public bodies through the ordinary source scanner; sourcevalidation and old12 retention are separately recorded.

What is trusted

The Rust compiler, official Charon/Aeneas translation, official scalar models and Lean kernel are trusted. Wrapping, casts, shifts and rotations in the primary proofs use official models, not Rust std body proofs. Range proofs instead include the original std wrapping_neg bodies transparently, with no new provider or model. Lean dependency audits permit only propext, Classical.choice and Quot.sound.

The four supplemental Into/TryInto body specializations additionally trust a default-off finite export patch that emits exactly the original transparent core bodies and omits duplicate rust_fun registrations. It changes no body, type, callback or Std model. Original source/LLBC, patch/binary hashes, default-off comparison and enabled export guards are retained; no general translator equivalence is established.

Kani results trust Kani/CBMC, the pinned August Rust compiler and solver semantics. Float composition uses the identical Rust helper across two universal specifications; no general Aeneas floating-point model or mechanized cross-tool equivalence is asserted. Exact compiler-commit standard sources show Any uses a TypeId intrinsic. Sized CloneToUninit has a clone/write default and a TrivialClone nonoverlapping-copy specialization, which may apply to these Clone+Copy types; the fixed-slot result does not prove arbitrary pointer validity or a particular dispatch route.

Technical limitations

Twenty machine-readable claims cover fourteen original local APIs and six conditional external core conversion families. These six are not local declarations. Kani results remain separate supplements; this is not full crate completion. All apply only in their recorded target/configuration and tool boundaries.

Range proofs identify the exact sample and final state conditional on a finite first accepted candidate, and divergence for an all-rejected trace. They do not establish an accepted index exists for every state/range, general termination, uniformity, period or expected runtime. Debug assertion failure does not specify release behavior or Rust panic/unwinding effects. Save/restore is pure state identity, not a guarantee about arbitrary callbacks or destructors. No period, distribution, independence or cryptographic guarantee is established.

The external Kani checks do not prove global TypeId uniqueness, arbitrary CloneToUninit destinations or heap behavior: extent, alignment, nonoverlap and provenance obligations remain with the caller. Generic conversion contracts require actual trait instances and matching modeled dictionaries, preserve the selected associated error type, and do not establish arbitrary U has an instance. Callback correctness/termination, Drop/unwind/global effects, physical aliasing/layout, resource availability and const evaluation remain outside those contracts. The six generic families use a finite compiler-owned source/body binding; arbitrary trait instances, implementations or configurations are not inferred.

Earlier direct combined float attempts timed out and are retained. The later Rand32 direct Z3 check succeeds; Rand64 direct Z3 still times out, while its successful two-stage composition establishes the stated contract. Other targets/configurations were not checked.

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 (4)

CrateReports

rand_core ^0.5 · dev—

rand_pcg ^0.2 · dev—

random-fast-rng ^0.1 · dev—

randomize ^3.0.0 · dev—

Comments (0)

No comments.