Report #32 — Exact endian writes and selected prefix reads, with failure contracts

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

42 verified claims · 0 findings

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

nyuichi · 2026-11-05 05:04 UTC

Revision v5 · v4 · v3 · v2 · v1

Overview

byteorder 1.5.0: fixed-width unsigned and signed integer writes, plus BE/LE write_f32/write_f64, write their exact bit representations in the selected endian order and preserve trailing bytes when the output is long enough; shorter buffers panic before writing. Float proofs quantify over every 32/64-bit representation, including NaN payloads and signed zeros, under explicit bit-pattern and std to_bits models. No floating arithmetic is modeled. BE/LE read_u24 additionally returns the exact unsigned24 prefix decode below2^24, and asserts on shorter input. LittleEndian from_slice_u16/u32/u64/u128 additionally leave every slice unchanged on the verified little-endian target, including empty slices and arbitrary unsigned values. The two handwritten Default methods always panic. Four unsigned variable-width readers decode the exact selected prefix under their complete byte-count/input-length guard, and assert otherwise. Eight additional original concrete reader defaults are verified: BE/LE read_u48 returns the exact six-byte unsigned decode below 2^48; read_int, read_i24 and read_i48 return the selected-width two-complement signed decode. General signed counts must be1..8 with sufficient input; fixed readers need three or six bytes. Failed input/count guards return assertion failure before sign extension. Their original full read_uint callees are connected by definitional equality to the existing byteorder general-reader proofs; the actual original extend_sign body is proved directly with separately named pure bit-vector lemmas, without new models or Lite proof imports. BE/LE read_int128 additionally decode every valid1..16byte signed prefix, and assert on all invalid count/input guards before sign extension. The actual original read_uint128 bodies are connected by definitional equality to existing byteorder contracts; the actual original extend_sign128 body is proved directly using independently named pure bit-vector lemmas. No Lite proof module or new model is imported. Separate Kani checks compare the original BE/LE write_uint/write_uint128 methods with byteorder-lite for all fitting unsigned values and valid byte counts, arbitrary initial 32-byte arrays, and slice lengths from the byte count through 32. Both complete buffers agree and suffix bytes are preserved; four harnesses complete with 456 checks and no failures.

Findings (0)

No findings reported.

APIs (42)

Recorded callables

<byteorder::BigEndian as Default>::default recorded callable · signature and safety not recorded

Claim #9

<byteorder::BigEndian as byteorder::ByteOrder>::read_i24 recorded callable · signature and safety not recorded

Claim #35

<byteorder::BigEndian as byteorder::ByteOrder>::read_i48 recorded callable · signature and safety not recorded

Claim #36

<byteorder::BigEndian as byteorder::ByteOrder>::read_int recorded callable · signature and safety not recorded

Claim #34

<byteorder::BigEndian as byteorder::ByteOrder>::read_int128 recorded callable · signature and safety not recorded

Claim #41

<byteorder::BigEndian as byteorder::ByteOrder>::read_u24 recorded callable · signature and safety not recorded

Claim #27

<byteorder::BigEndian as byteorder::ByteOrder>::read_u48 recorded callable · signature and safety not recorded

Claim #33

<byteorder::BigEndian as byteorder::ByteOrder>::read_uint recorded callable · signature and safety not recorded

Claim #23

<byteorder::BigEndian as byteorder::ByteOrder>::read_uint128 recorded callable · signature and safety not recorded

Claim #24

<byteorder::BigEndian as byteorder::ByteOrder>::write_f32 recorded callable · signature and safety not recorded

Claim #19

<byteorder::BigEndian as byteorder::ByteOrder>::write_f64 recorded callable · signature and safety not recorded

Claim #20

<byteorder::BigEndian as byteorder::ByteOrder>::write_i128 recorded callable · signature and safety not recorded

Claim #14

<byteorder::BigEndian as byteorder::ByteOrder>::write_i16 recorded callable · signature and safety not recorded

Claim #11

<byteorder::BigEndian as byteorder::ByteOrder>::write_i32 recorded callable · signature and safety not recorded

Claim #12

<byteorder::BigEndian as byteorder::ByteOrder>::write_i64 recorded callable · signature and safety not recorded

Claim #13

<byteorder::BigEndian as byteorder::ByteOrder>::write_u128 recorded callable · signature and safety not recorded

Claim #4

<byteorder::BigEndian as byteorder::ByteOrder>::write_u16 recorded callable · signature and safety not recorded

Claim #1

<byteorder::BigEndian as byteorder::ByteOrder>::write_u32 recorded callable · signature and safety not recorded

Claim #2

<byteorder::BigEndian as byteorder::ByteOrder>::write_u64 recorded callable · signature and safety not recorded

Claim #3

<byteorder::LittleEndian as Default>::default recorded callable · signature and safety not recorded

Claim #10

<byteorder::LittleEndian as byteorder::ByteOrder>::from_slice_u128 recorded callable · signature and safety not recorded

Claim #32

<byteorder::LittleEndian as byteorder::ByteOrder>::from_slice_u16 recorded callable · signature and safety not recorded

Claim #29

<byteorder::LittleEndian as byteorder::ByteOrder>::from_slice_u32 recorded callable · signature and safety not recorded

Claim #30

<byteorder::LittleEndian as byteorder::ByteOrder>::from_slice_u64 recorded callable · signature and safety not recorded

Claim #31

<byteorder::LittleEndian as byteorder::ByteOrder>::read_i24 recorded callable · signature and safety not recorded

Claim #39

<byteorder::LittleEndian as byteorder::ByteOrder>::read_i48 recorded callable · signature and safety not recorded

Claim #40

<byteorder::LittleEndian as byteorder::ByteOrder>::read_int recorded callable · signature and safety not recorded

Claim #38

<byteorder::LittleEndian as byteorder::ByteOrder>::read_int128 recorded callable · signature and safety not recorded

Claim #42

<byteorder::LittleEndian as byteorder::ByteOrder>::read_u24 recorded callable · signature and safety not recorded

Claim #28

<byteorder::LittleEndian as byteorder::ByteOrder>::read_u48 recorded callable · signature and safety not recorded

Claim #37

<byteorder::LittleEndian as byteorder::ByteOrder>::read_uint recorded callable · signature and safety not recorded

Claim #25

<byteorder::LittleEndian as byteorder::ByteOrder>::read_uint128 recorded callable · signature and safety not recorded

Claim #26

<byteorder::LittleEndian as byteorder::ByteOrder>::write_f32 recorded callable · signature and safety not recorded

Claim #21

<byteorder::LittleEndian as byteorder::ByteOrder>::write_f64 recorded callable · signature and safety not recorded

Claim #22

<byteorder::LittleEndian as byteorder::ByteOrder>::write_i128 recorded callable · signature and safety not recorded

Claim #18

<byteorder::LittleEndian as byteorder::ByteOrder>::write_i16 recorded callable · signature and safety not recorded

Claim #15

<byteorder::LittleEndian as byteorder::ByteOrder>::write_i32 recorded callable · signature and safety not recorded

Claim #16

<byteorder::LittleEndian as byteorder::ByteOrder>::write_i64 recorded callable · signature and safety not recorded

Claim #17

<byteorder::LittleEndian as byteorder::ByteOrder>::write_u128 recorded callable · signature and safety not recorded

Claim #8

<byteorder::LittleEndian as byteorder::ByteOrder>::write_u16 recorded callable · signature and safety not recorded

Claim #5

<byteorder::LittleEndian as byteorder::ByteOrder>::write_u32 recorded callable · signature and safety not recorded

Claim #6

<byteorder::LittleEndian as byteorder::ByteOrder>::write_u64 recorded callable · signature and safety not recorded

Claim #7

Evidence

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

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/nyuichi/rust-crate-proofs report-32-source-1
git -C report-32-source-1 checkout --detach 252fa0c68a602ba06fe0378b951f98a89fba6a25
git -C report-32-source-1 submodule update --init --recursive --checkout
cd report-32-source-1/byteorder/1.5.0/aeneas/2026-11-05/proofs

lake build +Byte128ReadProofs +ByteRead48Proofs +ByteSignedReadProofs +FloatProofs +NativeIdentityProofs +Proofs +ReadVariableProofs +SignedProofs +U24Exact24

printf '%s' 'import Lean
import Byte128ReadProofs
import ByteRead48Proofs
import ByteSignedReadProofs
import FloatProofs
import NativeIdentityProofs
import Proofs
import ReadVariableProofs
import SignedProofs
import U24Exact24
open Lean Elab Command

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2026-11-05T08:18:59.893428097+00:00 · 118.5 seconds · Exit code 0

Recorded on the author’s machine.

Check	Result	Claim
Lean checked theorem Proofs.be_write_u16_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.be_write_u16_contract`	Passed	Claim #1
Lean checked theorem Proofs.be_write_u32_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.be_write_u32_contract`	Passed	Claim #2
Lean checked theorem Proofs.be_write_u64_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.be_write_u64_contract`	Passed	Claim #3
Lean checked theorem Proofs.be_write_u128_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.be_write_u128_contract`	Passed	Claim #4
Lean checked theorem Proofs.le_write_u16_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.le_write_u16_contract`	Passed	Claim #5
Lean checked theorem Proofs.le_write_u32_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.le_write_u32_contract`	Passed	Claim #6
Lean checked theorem Proofs.le_write_u64_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.le_write_u64_contract`	Passed	Claim #7
Lean checked theorem Proofs.le_write_u128_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.le_write_u128_contract`	Passed	Claim #8
Lean checked theorem Proofs.BigEndian_default_panics; axioms limited to propext, Classical.choice, Quot.sound `Proofs.BigEndian_default_panics`	Passed	Claim #9
Lean checked theorem Proofs.LittleEndian_default_panics; axioms limited to propext, Classical.choice, Quot.sound `Proofs.LittleEndian_default_panics`	Passed	Claim #10
Lean checked theorem SignedProofs.be_write_i16_contract; axioms limited to propext, Classical.choice, Quot.sound `SignedProofs.be_write_i16_contract`	Passed	Claim #11
Lean checked theorem SignedProofs.be_write_i32_contract; axioms limited to propext, Classical.choice, Quot.sound `SignedProofs.be_write_i32_contract`	Passed	Claim #12
Lean checked theorem SignedProofs.be_write_i64_contract; axioms limited to propext, Classical.choice, Quot.sound `SignedProofs.be_write_i64_contract`	Passed	Claim #13
Lean checked theorem SignedProofs.be_write_i128_contract; axioms limited to propext, Classical.choice, Quot.sound `SignedProofs.be_write_i128_contract`	Passed	Claim #14
Lean checked theorem SignedProofs.le_write_i16_contract; axioms limited to propext, Classical.choice, Quot.sound `SignedProofs.le_write_i16_contract`	Passed	Claim #15
Lean checked theorem SignedProofs.le_write_i32_contract; axioms limited to propext, Classical.choice, Quot.sound `SignedProofs.le_write_i32_contract`	Passed	Claim #16
Lean checked theorem SignedProofs.le_write_i64_contract; axioms limited to propext, Classical.choice, Quot.sound `SignedProofs.le_write_i64_contract`	Passed	Claim #17
Lean checked theorem SignedProofs.le_write_i128_contract; axioms limited to propext, Classical.choice, Quot.sound `SignedProofs.le_write_i128_contract`	Passed	Claim #18
Lean checked theorem FloatProofs.be_write_f32_contract; axioms limited to propext, Classical.choice, Quot.sound `FloatProofs.be_write_f32_contract`	Passed	Claim #19
Lean checked theorem FloatProofs.be_write_f64_contract; axioms limited to propext, Classical.choice, Quot.sound `FloatProofs.be_write_f64_contract`	Passed	Claim #20
Lean checked theorem FloatProofs.le_write_f32_contract; axioms limited to propext, Classical.choice, Quot.sound `FloatProofs.le_write_f32_contract`	Passed	Claim #21
Lean checked theorem FloatProofs.le_write_f64_contract; axioms limited to propext, Classical.choice, Quot.sound `FloatProofs.le_write_f64_contract`	Passed	Claim #22
Lean checked theorem ReadVariableProofs.be_read_uint_contract; axioms limited to propext, Classical.choice, Quot.sound `ReadVariableProofs.be_read_uint_contract`	Passed	Claim #23
Lean checked theorem ReadVariableProofs.be_read_uint128_contract; axioms limited to propext, Classical.choice, Quot.sound `ReadVariableProofs.be_read_uint128_contract`	Passed	Claim #24
Lean checked theorem ReadVariableProofs.le_read_uint_contract; axioms limited to propext, Classical.choice, Quot.sound `ReadVariableProofs.le_read_uint_contract`	Passed	Claim #25
Lean checked theorem ReadVariableProofs.le_read_uint128_contract; axioms limited to propext, Classical.choice, Quot.sound `ReadVariableProofs.le_read_uint128_contract`	Passed	Claim #26
Lean checked theorem U24Proofs.be_read_u24_contract; axioms limited to propext, Classical.choice, Quot.sound `U24Proofs.be_read_u24_contract`	Passed	Claim #27
Lean checked theorem U24Proofs.le_read_u24_contract; axioms limited to propext, Classical.choice, Quot.sound `U24Proofs.le_read_u24_contract`	Passed	Claim #28
Lean checked theorem NativeIdentityProofs.le_from_slice_u16_identity; axioms limited to propext, Classical.choice, Quot.sound `NativeIdentityProofs.le_from_slice_u16_identity`	Passed	Claim #29
Lean checked theorem NativeIdentityProofs.le_from_slice_u32_identity; axioms limited to propext, Classical.choice, Quot.sound `NativeIdentityProofs.le_from_slice_u32_identity`	Passed	Claim #30
Lean checked theorem NativeIdentityProofs.le_from_slice_u64_identity; axioms limited to propext, Classical.choice, Quot.sound `NativeIdentityProofs.le_from_slice_u64_identity`	Passed	Claim #31
Lean checked theorem NativeIdentityProofs.le_from_slice_u128_identity; axioms limited to propext, Classical.choice, Quot.sound `NativeIdentityProofs.le_from_slice_u128_identity`	Passed	Claim #32
Lean checked theorem ByteRead48Proofs.be_read_u48_contract; axioms limited to propext, Classical.choice, Quot.sound `ByteRead48Proofs.be_read_u48_contract`	Passed	Claim #33
Lean checked theorem ByteSignedReadProofs.be_read_int_contract; axioms limited to propext, Classical.choice, Quot.sound `ByteSignedReadProofs.be_read_int_contract`	Passed	Claim #34
Lean checked theorem ByteSignedReadProofs.be_read_i24_contract; axioms limited to propext, Classical.choice, Quot.sound `ByteSignedReadProofs.be_read_i24_contract`	Passed	Claim #35
Lean checked theorem ByteRead48Proofs.be_read_i48_contract; axioms limited to propext, Classical.choice, Quot.sound `ByteRead48Proofs.be_read_i48_contract`	Passed	Claim #36
Lean checked theorem ByteRead48Proofs.le_read_u48_contract; axioms limited to propext, Classical.choice, Quot.sound `ByteRead48Proofs.le_read_u48_contract`	Passed	Claim #37
Lean checked theorem ByteSignedReadProofs.le_read_int_contract; axioms limited to propext, Classical.choice, Quot.sound `ByteSignedReadProofs.le_read_int_contract`	Passed	Claim #38
Lean checked theorem ByteSignedReadProofs.le_read_i24_contract; axioms limited to propext, Classical.choice, Quot.sound `ByteSignedReadProofs.le_read_i24_contract`	Passed	Claim #39
Lean checked theorem ByteRead48Proofs.le_read_i48_contract; axioms limited to propext, Classical.choice, Quot.sound `ByteRead48Proofs.le_read_i48_contract`	Passed	Claim #40
Lean checked theorem Byte128ReadProofs.be_read_int128_contract; axioms limited to propext, Classical.choice, Quot.sound `Byte128ReadProofs.be_read_int128_contract`	Passed	Claim #41
Lean checked theorem Byte128ReadProofs.le_read_int128_contract; axioms limited to propext, Classical.choice, Quot.sound `Byte128ReadProofs.le_read_int128_contract`	Passed	Claim #42

Execution details

Started: 2026-11-05T08:18:59.893428097+00:00
Finished: 2026-11-05T08:20:58.419638747+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: byteorder/1.5.0/aeneas/2026-11-05/proofs
Environment overrides: None recorded
Git repository: https://github.com/nyuichi/rust-crate-proofs
Git commit: 252fa0c68a602ba06fe0378b951f98a89fba6a25

Diagnostics & logs

=== stdout ===
⚠ [2/57] Ran aeneas:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
✔ [3/127] Built AeneasMeta.Simp.RegisterCommand (39s)
✔ [290/623] Built AeneasMeta.BvEnumToBitVec (39s)
✔ [569/869] Built Aeneas.Std.Global (40s)
✔ [570/869] Built AeneasMeta.UtilsCore (40s)
✔ [1576/1829] Built AeneasMeta.OptionConfig (40s)
✔ [1798/1829] Built Byteorder.Types (2.2s)
✔ [1799/1829] Built ByteorderApiRoots.Types (2.3s)
✔ [1800/1829] Built Generated.Byteorder (2.3s)
✔ [1801/1829] Built ByteorderU24Roots.Types (2.3s)
⚠ [1802/1829] Built ByteReadDecodeMath (3.4s)
warning: ByteReadDecodeMath.lean:17:15: This simp argument is unused:
  hns

Hint: Omit it from the simp argument list.
  [apply] simp [hni, heq, hi, h, hw, hs, hlast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ByteReadDecodeMath.lean:17:20: This simp argument is unused:
  heq

Hint: Omit it from the simp argument list.
  [apply] simp [hni, hns, hi, h, hw, hs, hlast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ByteReadDecodeMath.lean:17:36: This simp argument is unused:
  hs

Hint: Omit it from the simp argument list.
  [apply] simp [hni, hns, heq, hi, h, hw, hlast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ByteReadDecodeMath.lean:17:40: This simp argument is unused:
  hlast

Hint: Omit it from the simp argument list.
  [apply] simp [hni, hns, heq, hi, h, hw, hs]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: ByteReadDecodeMath.lean:52:0: 'ByteReadDecodeMath.signed_low_bits' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ByteReadDecodeMath.lean:54:0: 'ByteReadDecodeMath.zero_padding_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ByteReadDecodeMath.lean:56:0: 'ByteReadDecodeMath.zero_padding_be_val' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [1803/1829] Built ByteorderReadPureRoots.Types (2.2s)
✔ [1804/1829] Built ByteorderRead128Roots.Types (2.1s)
✔ [1805/1829] Built ByteorderFloatRoots.Types (2.2s)
⚠ [1806/1829] Built Byte128Math (3.4s)
warning: Byte128Math.lean:17:15: This simp argument is unused:
  hns

Hint: Omit it from the simp argument list.
  [apply] simp [hni, heq, hi, h, hw, hs, hlast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Byte128Math.lean:17:20: This simp argument is unused:
  heq

Hint: Omit it from the simp argument list.
  [apply] simp [hni, hns, hi, h, hw, hs, hlast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Byte128Math.lean:17:36: This simp argument is unused:
  hs

Hint: Omit it from the simp argument list.
  [apply] simp [hni, hns, heq, hi, h, hw, hlast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Byte128Math.lean:17:40: This simp argument is unused:
  hlast

Hint: Omit it from the simp argument list.
  [apply] simp [hni, hns, heq, hi, h, hw, hs]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Byte128Math.lean:52:0: 'Byte128Math.signed_low_bits' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Byte128Math.lean:54:0: 'Byte128Math.zero_padding_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Byte128Math.lean:56:0: 'Byte128Math.zero_padding_be_val' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [1807/1829] Built ReadVariableGenerated.Byteorder (2.6s)
✔ [1808/1829] Built Byteorder.FunsExternal (2.2s)
✔ [1809/1829] Built ByteorderU24Roots.Funs (2.6s)
✔ [1810/1829] Built ByteorderApiRoots.Funs (2.6s)
✔ [1811/1829] Built ByteorderReadPureRoots.Funs (2.5s)
✔ [1812/1829] Built ByteorderRead128Roots.Funs (2.5s)
✔ [1813/1829] Built ByteorderFloatRoots.FunsExternal (2.3s)
✔ [1814/1829] Built Byteorder.Funs (2.1s)
✔ [1815/1829] Built ByteorderFloatRoots.Funs (2.8s)
⚠ [1816/1829] Built SignedProofs (5.6s)
info: SignedProofs.lean:142:0: 'SignedProofs.be_write_i16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedProofs.lean:143:0: 'SignedProofs.be_write_i32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedProofs.lean:144:0: 'SignedProofs.be_write_i64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedProofs.lean:145:0: 'SignedProofs.be_write_i128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedProofs.lean:146:0: 'SignedProofs.le_write_i16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedProofs.lean:147:0: 'SignedProofs.le_write_i32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedProofs.lean:148:0: 'SignedProofs.le_write_i64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedProofs.lean:149:0: 'SignedProofs.le_write_i128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: SignedProofs.lean:155:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: SignedProofs.lean:175:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: SignedProofs.lean:195:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: SignedProofs.lean:215:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: SignedProofs.lean:235:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: SignedProofs.lean:255:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: SignedProofs.lean:275:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: SignedProofs.lean:295:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: SignedProofs.lean:313:0: 'SignedProofs.be_write_i16_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedProofs.lean:314:0: 'SignedProofs.be_write_i32_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedProofs.lean:315:0: 'SignedProofs.be_write_i64_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedProofs.lean:316:0: 'SignedProofs.be_write_i128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedProofs.lean:317:0: 'SignedProofs.le_write_i16_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedProofs.lean:318:0: 'SignedProofs.le_write_i32_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedProofs.lean:319:0: 'SignedProofs.le_write_i64_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedProofs.lean:320:0: 'SignedProofs.le_write_i128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1817/1829] Built NativeIdentityProofs (4.6s)
info: NativeIdentityProofs.lean:13:0: 'NativeIdentityProofs.le_from_slice_u16_identity' depends on axioms: [propext, Quot.sound]
info: NativeIdentityProofs.lean:14:0: 'NativeIdentityProofs.le_from_slice_u32_identity' depends on axioms: [propext, Quot.sound]
info: NativeIdentityProofs.lean:15:0: 'NativeIdentityProofs.le_from_slice_u64_identity' depends on axioms: [propext, Quot.sound]
info: NativeIdentityProofs.lean:16:0: 'NativeIdentityProofs.le_from_slice_u128_identity' depends on axioms: [propext, Quot.sound]
⚠ [1818/1829] Built FloatProofs (4.5s)
warning: FloatProofs.lean:18:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FloatProofs.lean:55:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FloatProofs.lean:92:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FloatProofs.lean:129:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: FloatProofs.lean:154:0: 'FloatProofs.be_write_f32_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FloatProofs.lean:155:0: 'FloatProofs.be_write_f64_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FloatProofs.lean:156:0: 'FloatProofs.le_write_f32_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FloatProofs.lean:157:0: 'FloatProofs.le_write_f64_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1819/1829] Built Proofs (2.0s)
info: Proofs.lean:87:0: 'Proofs.be_write_u16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:88:0: 'Proofs.be_write_u32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:89:0: 'Proofs.be_write_u64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:90:0: 'Proofs.be_write_u128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:91:0: 'Proofs.le_write_u16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:92:0: 'Proofs.le_write_u32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:93:0: 'Proofs.le_write_u64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:94:0: 'Proofs.le_write_u128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:97:0: 'Proofs.BigEndian_default_panics' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:99:0: 'Proofs.LittleEndian_default_panics' depends on axioms: [propext, Quot.sound]
warning: Proofs.lean:105:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:119:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:133:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:147:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:161:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:175:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:189:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:203:47: This simp argument is unused:
  core.slice.index.SliceIndexRangeToUsizeSlice

Hint: Omit it from the simp argument list.
  [apply] simp only [core.slice.index.Slice.index_mut, core.slice.index.SliceIndexRangeToUsizeSlice.index_mut]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Proofs.lean:215:0: 'Proofs.be_write_u16_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:216:0: 'Proofs.be_write_u32_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:217:0: 'Proofs.be_write_u64_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:218:0: 'Proofs.be_write_u128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:219:0: 'Proofs.le_write_u16_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:220:0: 'Proofs.le_write_u32_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:221:0: 'Proofs.le_write_u64_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:222:0: 'Proofs.le_write_u128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1820/1829] Built ReadVariableProofs (17s)
warning: ReadVariableProofs.lean: imports `Mathlib.Tactic.IntervalCases` from package `mathlib`, which is designed for use with the module system; consider adding `module` to the start of this file
warning: ReadVariableProofs.lean:134:26: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [Std.bind_ok, Array.to_slice, Array.repeat_val, Slice.len, Slice.length, massert, lift,
    Slice.from_val, List.length_replicate]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:135:15: This simp argument is unused:
  Slice.length

Hint: Omit it from the simp argument list.
  [apply] simp only [Std.bind_ok, bind_tc_ok, Array.to_slice, Array.repeat_val, Slice.len, massert, lift,
    Slice.from_val, List.length_replicate]

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

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:142:59: This simp argument is unused:
  bind_tc_fail

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

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

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:143:57: This simp argument is unused:
  bind_tc_fail

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:144:15: This simp argument is unused:
  Std.bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_tc_ok, Std.bind_fail, bind_tc_fail]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:144:28: This simp argument is unused:
  bind_tc_ok

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:144:55: This simp argument is unused:
  bind_tc_fail

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:149:26: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [Std.bind_ok, Array.to_slice, Array.repeat_val, Slice.len, Slice.length, massert, lift,
    Slice.from_val, List.length_replicate]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:150:15: This simp argument is unused:
  Slice.length

Hint: Omit it from the simp argument list.
  [apply] simp only [Std.bind_ok, bind_tc_ok, Array.to_slice, Array.repeat_val, Slice.len, massert, lift,
    Slice.from_val, List.length_replicate]

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

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:157:59: This simp argument is unused:
  bind_tc_fail

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

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

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:158:57: This simp argument is unused:
  bind_tc_fail

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:159:15: This simp argument is unused:
  Std.bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_tc_ok, Std.bind_fail, bind_tc_fail]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:159:28: This simp argument is unused:
  bind_tc_ok

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:159:55: This simp argument is unused:
  bind_tc_fail

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:164:26: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [Std.bind_ok, Array.to_slice, Array.repeat_val, Slice.len, Slice.length, massert, lift,
    Slice.from_val, List.length_replicate]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:165:15: This simp argument is unused:
  Slice.length

Hint: Omit it from the simp argument list.
  [apply] simp only [Std.bind_ok, bind_tc_ok, Array.to_slice, Array.repeat_val, Slice.len, massert, lift,
    Slice.from_val, List.length_replicate]

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

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:172:59: This simp argument is unused:
  bind_tc_fail

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

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

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:173:57: This simp argument is unused:
  bind_tc_fail

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:174:15: This simp argument is unused:
  Std.bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_tc_ok, Std.bind_fail, bind_tc_fail]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:174:28: This simp argument is unused:
  bind_tc_ok

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:174:55: This simp argument is unused:
  bind_tc_fail

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:179:26: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [Std.bind_ok, Array.to_slice, Array.repeat_val, Slice.len, Slice.length, massert, lift,
    Slice.from_val, List.length_replicate]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:180:15: This simp argument is unused:
  Slice.length

Hint: Omit it from the simp argument list.
  [apply] simp only [Std.bind_ok, bind_tc_ok, Array.to_slice, Array.repeat_val, Slice.len, massert, lift,
    Slice.from_val, List.length_replicate]

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

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:187:59: This simp argument is unused:
  bind_tc_fail

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

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

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:188:57: This simp argument is unused:
  bind_tc_fail

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:189:15: This simp argument is unused:
  Std.bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [bind_tc_ok, Std.bind_fail, bind_tc_fail]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:189:28: This simp argument is unused:
  bind_tc_ok

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ReadVariableProofs.lean:189:55: This simp argument is unused:
  bind_tc_fail

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: ReadVariableProofs.lean:191:0: 'ReadVariableProofs.be_read_uint_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ReadVariableProofs.lean:193:0: 'ReadVariableProofs.be_read_uint128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ReadVariableProofs.lean:195:0: 'ReadVariableProofs.le_read_uint_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ReadVariableProofs.lean:197:0: 'ReadVariableProofs.le_read_uint128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ReadVariableProofs.lean:199:0: 'ReadVariableProofs.be_read_uint_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ReadVariableProofs.lean:201:0: 'ReadVariableProofs.le_read_uint_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ReadVariableProofs.lean:202:0: 'ReadVariableProofs.be_read_uint128_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ReadVariableProofs.lean:203:0: 'ReadVariableProofs.le_read_uint128_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: ReadVariableProofs.lean:207:8: Variable name `minimum` is not explicitly referenced.

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

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ReadVariableProofs.lean:207:35: Variable name `maximum` is not explicitly referenced.

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

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ReadVariableProofs.lean:208:8: Variable name `buffer` is not explicitly referenced.

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

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ReadVariableProofs.lean:216:8: Variable name `minimum` is not explicitly referenced.

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

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ReadVariableProofs.lean:216:35: Variable name `maximum` is not explicitly referenced.

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

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ReadVariableProofs.lean:217:8: Variable name `buffer` is not explicitly referenced.

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

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ReadVariableProofs.lean:225:8: Variable name `minimum` is not explicitly referenced.

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

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ReadVariableProofs.lean:225:35: Variable name `maximum` is not explicitly referenced.

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

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ReadVariableProofs.lean:226:8: Variable name `buffer` is not explicitly referenced.

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

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ReadVariableProofs.lean:234:8: Variable name `minimum` is not explicitly referenced.

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

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ReadVariableProofs.lean:234:35: Variable name `maximum` is not explicitly referenced.

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

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ReadVariableProofs.lean:235:8: Variable name `buffer` is not explicitly referenced.

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

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: ReadVariableProofs.lean:243:0: 'ReadVariableProofs.be_read_uint_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ReadVariableProofs.lean:244:0: 'ReadVariableProofs.be_read_uint128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ReadVariableProofs.lean:245:0: 'ReadVariableProofs.le_read_uint_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ReadVariableProofs.lean:246:0: 'ReadVariableProofs.le_read_uint128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [1821/1829] Built Byte128Support (2.0s)
ℹ [1822/1829] Built U24Bodies (2.3s)
info: U24Bodies.lean:13:0: 'U24Proofs.be_read_uint_body_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24Bodies.lean:14:0: 'U24Proofs.le_read_uint_body_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [1823/1829] Built ByteReadSupport (2.3s)
ℹ [1824/1829] Built U24Decode24 (2.8s)
info: U24Decode24.lean:23:0: '_private.U24Decode24.0.U24Proofs.be_padding' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24Decode24.lean:37:0: 'U24Proofs.be_three_decode' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24Decode24.lean:45:0: 'U24Proofs.le_three_decode' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1825/1829] Built U24WrapperProofs (2.4s)
info: U24WrapperProofs.lean:23:0: 'U24Proofs.be_read_u24_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24WrapperProofs.lean:24:0: 'U24Proofs.le_read_u24_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: U24WrapperProofs.lean:36:28: This simp argument is unused:
  bind_tc_fail

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: U24WrapperProofs.lean:46:28: This simp argument is unused:
  bind_tc_fail

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: U24WrapperProofs.lean:48:0: 'U24Proofs.be_read_u24_short' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24WrapperProofs.lean:49:0: 'U24Proofs.le_read_u24_short' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1826/1829] Built Byte128ReadProofs (2.9s)
info: Byte128ReadProofs.lean:103:0: 'Byte128ReadProofs.be_read_int128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Byte128ReadProofs.lean:104:0: 'Byte128ReadProofs.le_read_int128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1827/1829] Built ByteSignedReadProofs (3.3s)
info: ByteSignedReadProofs.lean:29:0: 'ByteSignedReadProofs.extend_sign_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ByteSignedReadProofs.lean:75:0: 'ByteSignedReadProofs.be_read_int_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ByteSignedReadProofs.lean:76:0: 'ByteSignedReadProofs.le_read_int_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ByteSignedReadProofs.lean:124:0: 'ByteSignedReadProofs.be_read_int_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ByteSignedReadProofs.lean:125:0: 'ByteSignedReadProofs.be_read_i24_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ByteSignedReadProofs.lean:126:0: 'ByteSignedReadProofs.le_read_int_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ByteSignedReadProofs.lean:127:0: 'ByteSignedReadProofs.le_read_i24_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ByteSignedReadProofs.lean:181:0: 'ByteSignedReadProofs.be_read_int_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ByteSignedReadProofs.lean:182:0: 'ByteSignedReadProofs.be_read_i24_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ByteSignedReadProofs.lean:183:0: 'ByteSignedReadProofs.le_read_int_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ByteSignedReadProofs.lean:184:0: 'ByteSignedReadProofs.le_read_i24_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1828/1829] Built U24Exact24 (2.1s)
info: U24Exact24.lean:44:0: 'U24Proofs.be_read_u24_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24Exact24.lean:45:0: 'U24Proofs.le_read_u24_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24Exact24.lean:61:0: 'U24Proofs.be_read_u24_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24Exact24.lean:62:0: 'U24Proofs.le_read_u24_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1829/1829] Built ByteRead48Proofs (2.0s)
info: ByteRead48Proofs.lean:98:0: 'ByteRead48Proofs.be_read_u48_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ByteRead48Proofs.lean:99:0: 'ByteRead48Proofs.be_read_i48_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ByteRead48Proofs.lean:100:0: 'ByteRead48Proofs.le_read_u48_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ByteRead48Proofs.lean:101:0: 'ByteRead48Proofs.le_read_i48_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
Build completed successfully (1829 jobs).

$ lake env lean --stdin (proofs.rs theorem/axiom audit)
proofs.rs:checked:Proofs.be_write_u16_contract
proofs.rs:checked:Proofs.be_write_u32_contract
proofs.rs:checked:Proofs.be_write_u64_contract
proofs.rs:checked:Proofs.be_write_u128_contract
proofs.rs:checked:Proofs.le_write_u16_contract
proofs.rs:checked:Proofs.le_write_u32_contract
proofs.rs:checked:Proofs.le_write_u64_contract
proofs.rs:checked:Proofs.le_write_u128_contract
proofs.rs:checked:Proofs.BigEndian_default_panics
proofs.rs:checked:Proofs.LittleEndian_default_panics
proofs.rs:checked:SignedProofs.be_write_i16_contract
proofs.rs:checked:SignedProofs.be_write_i32_contract
proofs.rs:checked:SignedProofs.be_write_i64_contract
proofs.rs:checked:SignedProofs.be_write_i128_contract
proofs.rs:checked:SignedProofs.le_write_i16_contract
proofs.rs:checked:SignedProofs.le_write_i32_contract
proofs.rs:checked:SignedProofs.le_write_i64_contract
proofs.rs:checked:SignedProofs.le_write_i128_contract
proofs.rs:checked:FloatProofs.be_write_f32_contract
proofs.rs:checked:FloatProofs.be_write_f64_contract
proofs.rs:checked:FloatProofs.le_write_f32_contract
proofs.rs:checked:FloatProofs.le_write_f64_contract
proofs.rs:checked:ReadVariableProofs.be_read_uint_contract
proofs.rs:checked:ReadVariableProofs.be_read_uint128_contract
proofs.rs:checked:ReadVariableProofs.le_read_uint_contract
proofs.rs:checked:ReadVariableProofs.le_read_uint128_contract
proofs.rs:checked:U24Proofs.be_read_u24_contract
proofs.rs:checked:U24Proofs.le_read_u24_contract
proofs.rs:checked:NativeIdentityProofs.le_from_slice_u16_identity
proofs.rs:checked:NativeIdentityProofs.le_from_slice_u32_identity
proofs.rs:checked:NativeIdentityProofs.le_from_slice_u64_identity
proofs.rs:checked:NativeIdentityProofs.le_from_slice_u128_identity
proofs.rs:checked:ByteRead48Proofs.be_read_u48_contract
proofs.rs:checked:ByteSignedReadProofs.be_read_int_contract
proofs.rs:checked:ByteSignedReadProofs.be_read_i24_contract
proofs.rs:checked:ByteRead48Proofs.be_read_i48_contract
proofs.rs:checked:ByteRead48Proofs.le_read_u48_contract
proofs.rs:checked:ByteSignedReadProofs.le_read_int_contract
proofs.rs:checked:ByteSignedReadProofs.le_read_i24_contract
proofs.rs:checked:ByteRead48Proofs.le_read_i48_contract
proofs.rs:checked:Byte128ReadProofs.be_read_int128_contract
proofs.rs:checked:Byte128ReadProofs.le_read_int128_contract

=== 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

Archive-identical Rust/Cargo.toml; x86_64 default features, debug extraction. Rust nightly-2026-09-17, Charon08d7c9d50144bd84848212c24701253585e90d1f, Aeneas be86ab0f1989d04944292b345b24c435be3ad10a, Lean4.35.0. Kani0.68.0/CBMC6.11.0/Rust nightly-2026-08-21: six harnesses, 276 checks, no failures per crate. Separate variable-width writer bridge: Kani0.68.0, Rust nightly-2026-08-21 versus Aeneas nightly-2026-09-17; four harnesses/456 checks, unwind34; evidence/kani-variable-writer-bridge.

What is trusted

F32/F64 are explicit 32/64-bit logical patterns; two executable std to_bits models preserve those patterns as unsigned words, with checked Lean value-preservation lemmas. Guards require original writer bodies and allow no other float operation. Kani checks std bit identity for every pattern and actual released writers with 6/10-byte buffers. Connecting these Rust checks to the Lean representation is reviewed, not mechanized; Rust nightlies differ. Official translation/standard integer and slice models, Lean, and Kani/CBMC are trusted. The four original native conversion bodies make no external calls after official target-branch translation. Five unused declarations remain in the unchanged, unimported template; the provider supplies zero definitions. Guards require exact identity bodies and zero external use. Mapped audits permit only propext, Classical.choice and Quot.sound.

Technical limitations

This covers 20 selected writer methods, eight unsigned and eight signed readers, four native-target unsigned identity conversions, and two handwritten Default methods, not all public APIs. Fixed 16/32/64/128-bit reads, variable-width writers, other bulk and in-place conversions, I/O extensions, other targets and release extraction remain unproved. The float result establishes bit serialization only: floating arithmetic, comparisons, rounding, numeric accuracy, NaN arithmetic and signaling behavior are not modeled. Kani public-writer buffer lengths are fixed at 6 and 10; arbitrary valid slice lengths are quantified separately by the Lean theorems. The signed from_slice defaults contain unsafe slice reinterpretation and are not covered; the floating conversions and opposite-endian/other-target paths are also unproved. The byteorder-lite eight-method result is not assumed transferable across versions. Panic messages and unwinding side effects are not specified. The separate variable-width writer comparison is limited to normal-success inputs and the 32-byte allocation shape. It does not establish failing inputs, arbitrary lengths/allocations, or independent memory safety. It adds no Aeneas API claims.

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

CrateReports

quickcheck ^0.9.2 · dev—

rand ^0.7 · dev—

Comments (0)

No comments.