Report #23 — Exact integer writes and misuse checks in NoHashHasher

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

14 verified claims · 0 findings

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

nyuichi · 2026-11-05 00:24 UTC

Revision v5 · v4 · v3 · v2 · v1

Overview

For nohash-hasher 0.2.0 on x86_64 with std enabled or disabled, Default initializes the stored value to zero, Clone preserves state, and finish returns the stored integer. Each of the ten integer write methods stores the Rust conversion of its input to u64: unsigned values are widened and signed values are converted modulo 2^64. With debug assertions enabled, the first integer write succeeds and a later write fails its assertion. With debug assertions disabled, each integer write replaces the stored value. The generic byte-slice write always panics in both configurations. These are exact per-method state and result contracts over all inputs, proved from unchanged published Rust bodies. Separate original-body Kani evidence checks handwritten Debug::fmt for NoHashHasher<u8> after Default or one arbitrary write_u8, using default {:?} formatting into a fixed 64-byte writer. Successful output has exact tuple delimiters, canonical decimal state and, in debug mode, the correct written flag. A writer that errors on its first call propagates Err and leaves its buffer unchanged. All std/no_std dependency and debug/release combinations pass separately: 2175 debug and 2143 release checks in each feature configuration; the verification harness itself uses std. This is a bounded formatter/input-domain supplement, not another Aeneas API claim or a proof for arbitrary stored u64 values, writers, formatting options or partial-write failures. A separate Kani supplement executes the actual standard Clone::clone_from default body and original manual Clone for NoHashHasher<u64>, in all four configurations. Source and destination independently begin at Default or one arbitrary write_u64. Public finish checks destination replacement and source preservation; a distinct full-original-prefix fixture with read-only getters also checks the debug written flag. The eight jobs succeed (public-value stage 47 debug or 28 release checks, flag-observer stage 104 or 81 checks per feature configuration). This concrete reachable-state Rust-body guarantee is separate from the generic Lean composition through the official default model; arbitrary T, other std revisions and other state histories remain unproved. Separate generic Lean contracts cover actual public Hasher::write_length_prefix, write_u128 and write_i128 calls through compiler-inlined UFCS callers in std/no_std with debug assertions enabled/disabled. For every represented T under the original IsEnabled bound and every receiver state, debug length-prefix stores the usize-to-u64 cast and marks written when previously unwritten, or fails assertionFailure when already written. Without debug assertions it always overwrites the stored word. Both wide integer calls fail panic for every input and receiver state because their original standard defaults reach NoHashHasher::write. The separate900-check Kani evidence covers the ten original integer T instantiations: debug initial states and release default-or-once-written public states. Four further generic compiler-inlined caller contracts cover original Hasher::write_str in std/no_std with debug assertions enabled/disabled. For every represented T under IsEnabled, receiver state and string, including empty strings, the call fails panic: the original default first calls NoHashHasher::write on the string bytes, which unconditionally panics, so the trailing write_u8(0xff) is unreachable. There is no fixed string-length/content restriction.

Findings (0)

No findings reported.

APIs (14)

Trait implementations

`impl core::clone::Clone for NoHashHasher<T>`

pub fn clone(self: &Self) -> Self

Claim #2

`impl core::default::Default for NoHashHasher<T>`

pub fn default() -> Self

Claim #1

`impl core::hash::Hasher for NoHashHasher<T>`

pub fn finish(self: &Self) -> u64

Claim #4

pub fn write(self: &mut Self, _: &[u8])

Claim #3

pub fn write_i16(self: &mut Self, n: i16)

Claim #11

pub fn write_i32(self: &mut Self, n: i32)

Claim #12

pub fn write_i64(self: &mut Self, n: i64)

Claim #13

pub fn write_i8(self: &mut Self, n: i8)

Claim #10

pub fn write_isize(self: &mut Self, n: isize)

Claim #14

pub fn write_u16(self: &mut Self, n: u16)

Claim #6

pub fn write_u32(self: &mut Self, n: u32)

Claim #7

pub fn write_u64(self: &mut Self, n: u64)

Claim #8

pub fn write_u8(self: &mut Self, n: u8)

Claim #5

pub fn write_usize(self: &mut Self, n: usize)

Claim #9

Evidence

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

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/nyuichi/rust-crate-proofs report-23-source-1
git -C report-23-source-1 checkout --detach 9db263d0e4a64a25b8d39b54837ad0e64b827ce3
git -C report-23-source-1 submodule update --init --recursive --checkout
cd report-23-source-1/nohash-hasher/0.2.0/aeneas/2026-11-05/proofs

lake build +Proofs

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2026-11-05T17:46:04.238167911+00:00 · 116.9 seconds · Exit code 0

Recorded on the author’s machine.

Check	Result	Claim
Lean checked theorem Proofs.default_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.default_spec`	Passed	Claim #1
Lean checked theorem Proofs.clone_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.clone_spec`	Passed	Claim #2
Lean checked theorem Proofs.write_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.write_spec`	Passed	Claim #3
Lean checked theorem Proofs.finish_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.finish_spec`	Passed	Claim #4
Lean checked theorem Proofs.write_u8_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.write_u8_spec`	Passed	Claim #5
Lean checked theorem Proofs.write_u16_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.write_u16_spec`	Passed	Claim #6
Lean checked theorem Proofs.write_u32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.write_u32_spec`	Passed	Claim #7
Lean checked theorem Proofs.write_u64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.write_u64_spec`	Passed	Claim #8
Lean checked theorem Proofs.write_usize_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.write_usize_spec`	Passed	Claim #9
Lean checked theorem Proofs.write_i8_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.write_i8_spec`	Passed	Claim #10
Lean checked theorem Proofs.write_i16_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.write_i16_spec`	Passed	Claim #11
Lean checked theorem Proofs.write_i32_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.write_i32_spec`	Passed	Claim #12
Lean checked theorem Proofs.write_i64_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.write_i64_spec`	Passed	Claim #13
Lean checked theorem Proofs.write_isize_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.write_isize_spec`	Passed	Claim #14

Execution details

Started: 2026-11-05T17:46:04.238167911+00:00
Finished: 2026-11-05T17:48:01.134043320+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: nohash-hasher/0.2.0/aeneas/2026-11-05/proofs
Environment overrides: None recorded
Git repository: https://github.com/nyuichi/rust-crate-proofs
Git commit: 9db263d0e4a64a25b8d39b54837ad0e64b827ce3

Diagnostics & logs

=== stdout ===
⚠ [2/57] Ran aeneas:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
✔ [3/109] Built AeneasMeta.Simp.RegisterCommand (41s)
✔ [222/603] Built Aeneas.Std.Global (41s)
✔ [223/603] Built AeneasMeta.UtilsCore (41s)
✔ [250/603] Built AeneasMeta.BvEnumToBitVec (41s)
✔ [1575/1827] Built AeneasMeta.OptionConfig (42s)
✔ [1797/1827] Built NohashStdReleaseAll (2.6s)
✔ [1798/1827] Built NoStdGenerated.NohashHasher (2.7s)
✔ [1799/1827] Built ReleaseGenerated.NohashHasher (2.8s)
✔ [1800/1827] Built NoStdReleaseGenerated.NohashHasher (2.8s)
✔ [1801/1827] Built NohashNostdRelease (2.9s)
✔ [1802/1827] Built NohashStringStdRelease (2.4s)
✔ [1803/1827] Built NohashPrefixInline (2.4s)
✔ [1804/1827] Built NohashWidePanicInline (2.5s)
✔ [1805/1827] Built NohashNostdDebug (2.6s)
✔ [1806/1827] Built NohashStringNostdRelease (2.5s)
✔ [1807/1827] Built NohashStringInline (2.4s)
✔ [1808/1827] Built NohashStringNostdDebug (2.4s)
✔ [1809/1827] Built Generated.NohashHasher (2.4s)
ℹ [1810/1827] Built PrefixStdRelease (3.2s)
info: PrefixStdRelease.lean:11:0: 'PrefixStdRelease.exact_transition' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PrefixStdRelease.lean:12:0: 'PrefixStdRelease.wide_unsigned_panic' depends on axioms: [propext, Quot.sound]
info: PrefixStdRelease.lean:13:0: 'PrefixStdRelease.wide_signed_panic' depends on axioms: [propext, Quot.sound]
✔ [1811/1827] Built NoStdDebugProofs (3.1s)
ℹ [1812/1827] Built PrefixNoStdRelease (2.9s)
info: PrefixNoStdRelease.lean:11:0: 'PrefixNoStdRelease.exact_transition' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PrefixNoStdRelease.lean:12:0: 'PrefixNoStdRelease.wide_unsigned_panic' depends on axioms: [propext, Quot.sound]
info: PrefixNoStdRelease.lean:13:0: 'PrefixNoStdRelease.wide_signed_panic' depends on axioms: [propext, Quot.sound]
✔ [1813/1827] Built ReleaseProofs (3.1s)
✔ [1814/1827] Built NoStdReleaseProofs (3.2s)
ℹ [1815/1827] Built WriteStrStdRelease (2.9s)
info: WriteStrStdRelease.lean:8:0: 'WriteStrStdRelease.always_panics' depends on axioms: [propext, Quot.sound]
ℹ [1816/1827] Built WidePanicProofs (2.8s)
info: WidePanicProofs.lean:11:0: 'WidePanicProofs.unsigned_always_panics' depends on axioms: [propext, Quot.sound]
info: WidePanicProofs.lean:12:0: 'WidePanicProofs.signed_always_panics' depends on axioms: [propext, Quot.sound]
ℹ [1817/1827] Built PrefixProofs (3.1s)
info: PrefixProofs.lean:15:0: 'PrefixProofs.exact_transition' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PrefixProofs.lean:16:0: 'PrefixProofs.already_written_panics' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1818/1827] Built WriteStrNoStdRelease (2.9s)
info: WriteStrNoStdRelease.lean:8:0: 'WriteStrNoStdRelease.always_panics' depends on axioms: [propext, Quot.sound]
ℹ [1819/1827] Built PrefixNoStdDebug (3.2s)
info: PrefixNoStdDebug.lean:12:0: 'PrefixNoStdDebug.exact_transition' depends on axioms: [propext, Classical.choice, Quot.sound]
info: PrefixNoStdDebug.lean:13:0: 'PrefixNoStdDebug.wide_unsigned_panic' depends on axioms: [propext, Quot.sound]
info: PrefixNoStdDebug.lean:14:0: 'PrefixNoStdDebug.wide_signed_panic' depends on axioms: [propext, Quot.sound]
ℹ [1820/1827] Built WriteStrNoStdDebug (2.9s)
info: WriteStrNoStdDebug.lean:8:0: 'WriteStrNoStdDebug.always_panics' depends on axioms: [propext, Quot.sound]
ℹ [1821/1827] Built WriteStrProofs (3.0s)
info: WriteStrProofs.lean:8:0: 'WriteStrProofs.always_panics' depends on axioms: [propext, Quot.sound]
✔ [1822/1827] Built DebugProofs (2.5s)
ℹ [1823/1827] Built NoStdProofs (2.5s)
info: NoStdProofs.lean:161:0: 'NoStdProofs.default_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NoStdProofs.lean:162:0: 'NoStdProofs.clone_spec' depends on axioms: [propext, Quot.sound]
info: NoStdProofs.lean:163:0: 'NoStdProofs.finish_spec' depends on axioms: [propext, Quot.sound]
info: NoStdProofs.lean:164:0: 'NoStdProofs.write_spec' depends on axioms: [propext, Quot.sound]
info: NoStdProofs.lean:165:0: 'NoStdProofs.write_u8_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NoStdProofs.lean:166:0: 'NoStdProofs.write_u16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NoStdProofs.lean:167:0: 'NoStdProofs.write_u32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NoStdProofs.lean:168:0: 'NoStdProofs.write_u64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NoStdProofs.lean:169:0: 'NoStdProofs.write_usize_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NoStdProofs.lean:170:0: 'NoStdProofs.write_i8_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NoStdProofs.lean:171:0: 'NoStdProofs.write_i16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NoStdProofs.lean:172:0: 'NoStdProofs.write_i32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NoStdProofs.lean:173:0: 'NoStdProofs.write_i64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NoStdProofs.lean:174:0: 'NoStdProofs.write_isize_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1824/1827] Built HasherFamilyAudit (2.1s)
info: HasherFamilyAudit.lean:10:0: 'PrefixProofs.exact_transition' depends on axioms: [propext, Classical.choice, Quot.sound]
info: HasherFamilyAudit.lean:11:0: 'PrefixProofs.already_written_panics' depends on axioms: [propext, Classical.choice, Quot.sound]
info: HasherFamilyAudit.lean:12:0: 'WidePanicProofs.unsigned_always_panics' depends on axioms: [propext, Quot.sound]
info: HasherFamilyAudit.lean:13:0: 'WidePanicProofs.signed_always_panics' depends on axioms: [propext, Quot.sound]
info: HasherFamilyAudit.lean:14:0: 'PrefixNoStdDebug.exact_transition' depends on axioms: [propext, Classical.choice, Quot.sound]
info: HasherFamilyAudit.lean:15:0: 'PrefixNoStdDebug.wide_unsigned_panic' depends on axioms: [propext, Quot.sound]
info: HasherFamilyAudit.lean:16:0: 'PrefixNoStdDebug.wide_signed_panic' depends on axioms: [propext, Quot.sound]
info: HasherFamilyAudit.lean:17:0: 'PrefixNoStdRelease.exact_transition' depends on axioms: [propext, Classical.choice, Quot.sound]
info: HasherFamilyAudit.lean:18:0: 'PrefixNoStdRelease.wide_unsigned_panic' depends on axioms: [propext, Quot.sound]
info: HasherFamilyAudit.lean:19:0: 'PrefixNoStdRelease.wide_signed_panic' depends on axioms: [propext, Quot.sound]
info: HasherFamilyAudit.lean:20:0: 'PrefixStdRelease.exact_transition' depends on axioms: [propext, Classical.choice, Quot.sound]
info: HasherFamilyAudit.lean:21:0: 'PrefixStdRelease.wide_unsigned_panic' depends on axioms: [propext, Quot.sound]
info: HasherFamilyAudit.lean:22:0: 'PrefixStdRelease.wide_signed_panic' depends on axioms: [propext, Quot.sound]
info: HasherFamilyAudit.lean:24:0: 'WriteStrProofs.always_panics' depends on axioms: [propext, Quot.sound]
info: HasherFamilyAudit.lean:25:0: 'WriteStrNoStdDebug.always_panics' depends on axioms: [propext, Quot.sound]
info: HasherFamilyAudit.lean:26:0: 'WriteStrNoStdRelease.always_panics' depends on axioms: [propext, Quot.sound]
info: HasherFamilyAudit.lean:27:0: 'WriteStrStdRelease.always_panics' depends on axioms: [propext, Quot.sound]
ℹ [1825/1827] Built StdProofs (2.2s)
info: StdProofs.lean:161:0: 'StdProofs.default_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StdProofs.lean:162:0: 'StdProofs.clone_spec' depends on axioms: [propext, Quot.sound]
info: StdProofs.lean:163:0: 'StdProofs.finish_spec' depends on axioms: [propext, Quot.sound]
info: StdProofs.lean:164:0: 'StdProofs.write_spec' depends on axioms: [propext, Quot.sound]
info: StdProofs.lean:165:0: 'StdProofs.write_u8_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StdProofs.lean:166:0: 'StdProofs.write_u16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StdProofs.lean:167:0: 'StdProofs.write_u32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StdProofs.lean:168:0: 'StdProofs.write_u64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StdProofs.lean:169:0: 'StdProofs.write_usize_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StdProofs.lean:170:0: 'StdProofs.write_i8_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StdProofs.lean:171:0: 'StdProofs.write_i16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StdProofs.lean:172:0: 'StdProofs.write_i32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StdProofs.lean:173:0: 'StdProofs.write_i64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StdProofs.lean:174:0: 'StdProofs.write_isize_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1826/1827] Built SupplementalProofs (2.1s)
info: SupplementalProofs.lean:27:0: 'SupplementalProofs.clone_from_spec' depends on axioms: [propext, Quot.sound]
ℹ [1827/1827] Built Proofs (2.3s)
info: Proofs.lean:256:0: 'Proofs.default_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:257:0: 'Proofs.clone_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:258:0: 'Proofs.finish_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:259:0: 'Proofs.write_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:260:0: 'Proofs.write_u8_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:261:0: 'Proofs.write_u16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:262:0: 'Proofs.write_u32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:263:0: 'Proofs.write_u64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:264:0: 'Proofs.write_usize_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:265:0: 'Proofs.write_i8_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:266:0: 'Proofs.write_i16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:267:0: 'Proofs.write_i32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:268:0: 'Proofs.write_i64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:269:0: 'Proofs.write_isize_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
Build completed successfully (1827 jobs).

$ lake env lean --stdin (proofs.rs theorem/axiom audit)
proofs.rs:checked:Proofs.default_spec
proofs.rs:checked:Proofs.clone_spec
proofs.rs:checked:Proofs.write_spec
proofs.rs:checked:Proofs.finish_spec
proofs.rs:checked:Proofs.write_u8_spec
proofs.rs:checked:Proofs.write_u16_spec
proofs.rs:checked:Proofs.write_u32_spec
proofs.rs:checked:Proofs.write_u64_spec
proofs.rs:checked:Proofs.write_usize_spec
proofs.rs:checked:Proofs.write_i8_spec
proofs.rs:checked:Proofs.write_i16_spec
proofs.rs:checked:Proofs.write_i32_spec
proofs.rs:checked:Proofs.write_i64_spec
proofs.rs:checked:Proofs.write_isize_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

Unmodified crates.io nohash-hasher 0.2.0; x86_64-unknown-linux-gnu, std enabled and disabled; debug_assertions true and false. Charon 08d7c9d50144bd84848212c24701253585e90d1f, Aeneas be86ab0f1989d04944292b345b24c435be3ad10a, Rust nightly-2026-09-17, Lean 4.35.0. Official start-from roots select the actual method bodies; the official namespace option separates debug/release translations. Fourteen public theorems each conjoin all four std/no-std and debug/release configurations. The supplementary clone_from composition is included in the fresh Lean build without adding an API mapping. cargo-proofs 0.4.1 has the documented TLS-CA and upstream audit-variable compatibility fixes; the allowed-axiom policy is unchanged. Added evidence/hasher-inherited-family preserves generic3API across four configurations (twelve contracts plus one helper), and separate900 Kani checks with zero failures. Generic extraction uses pinned September compiler/official frontend with Inline/DCE; Kani uses its separately pinned August compiler. Import-only integration connects HasherFamilyAudit to the configured primary Proofs module, so the actual CLI targets must print all13 supplemental axiom audits. All old14 mappings and preconditions remain unchanged. evidence/write-str-inline4 preserves the new103-file frozen packet and source/type/evidence reviews. Existing HasherFamilyAudit imports the four new proof modules and audits17 unique supplementary declarations (old13 plus new4); the actual +Proofs CLI target must include all17 markers. Original14 mappings and all prior13/900 evidence remain preserved.

What is trusted

The Rust compiler, Charon/Aeneas translation, their standard-library models, and the Lean kernel are trusted. The checked theorems use no extra local axioms; their transitive dependencies are limited to Lean's propext, Classical.choice, and Quot.sound. Generic inherited-call proofs additionally trust the pinned Rust optimized MIR compiler Inline pass and, for wide calls, SimplifyLocals-final dead-code elimination before official Charon/Aeneas extraction. The caller/stdlib/original-method source guards and configuration layouts are retained. This is not a compiler-correctness or direct default-declaration source-card proof; no source/LLBC/generated edits, new model or panic stub is introduced. write_str additionally uses the pinned official rustc Inline, RemoveStorageMarkers, ReferencePropagation, DeadStoreElimination-final and SimplifyLocals-final passes through optimized MIR/official Charon and unchanged Aeneas. Source/IR guards connect the actual UFCS caller, standard default and original panic source spans. The final generated body does not read the string or call another function. This trusts compiler inlining/cleanup, not a compiler-correctness proof, panic stub or direct default-method API-card binding.

Technical limitations

Coverage consists of Default, Clone, ten integer writers, write, and finish in the stated debug/release configurations. General Debug behavior beyond the separate u8/default-format/fixed-writer Kani domain, other inherited Hasher default methods beyond the four supplemental actual-caller API families described here, full trait-instance integration, custom Hash implementations, BuildHasherDefault, and HashMap/HashSet behavior are not verified. In particular, this does not establish that a custom IsEnabled type obeys the required single-integer-write Hash protocol. Other targets were not checked. The upstream no-std IsEnabled doctest refers to the std-only IntMap alias and does not compile; the no-std unit tests and proved method bodies pass. A supplementary clone_from theorem composes the actual clone body with the official standard-library default model and proves exact replacement by source; it is not an independent std-body proof or a separate published API claim. write_length_prefix is the pinned nightly hasher_prefixfree_extras API, not a stable-interface guarantee. The new inherited-family results are supplemental actual-caller contracts, not new registered machine API claims; primary coverage stays14. The generic contracts distinguish debug and release receiver layouts and retain IsEnabled/trait correspondence assumptions. Panic messages, unwinding, global effects, other targets/profiles and const evaluation are not established. Kani900 has narrower concrete-T/reachable-state domains and is not a premise of the generic Lean proofs. The producer consolidated regeneration script was not rerun; earlier successful individual extractions/source guards and complete kernel audits are retained, and the formal recorded build recompiles all13 supplemental declarations. The producer READY compiled_sidecars0 flag was inaccurate; twenty listed compiler sidecars are excluded from this public source subset, with an exact erratum list. write_str is also a pinned nightly hasher_prefixfree_extras API, not a stable-interface guarantee. Its producer READY zero-sidecar flag was inaccurate: sixteen listed compiler sidecars are excluded from this public87-file source subset, with exact hashes and an erratum retained. The write_str results remain supplemental actual-caller contracts with no new registered API claims. Modeled fail panic does not specify panic hooks, messages/locations, unwind/global effects or independent physical memory/alias/lifetime guarantees. Other targets/compiler settings and const evaluation are outside scope. Initial dead TwoPhaseMut-copy translation failures remain historical; the intermediate failing LLBC was not separately frozen before official re-extraction. No source, LLBC or generated body was hand edited. Consolidated portable regeneration/replay has not been run; individual generation, proof and coimport successes are retained.

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

No direct dependencies.

Comments (0)

No comments.