Report #33 — Exact integer and floating bit serialization, with explicit failure conditions

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

64 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:07 UTC

Revision v5 · v4 · v3 · v2 · v1

Overview

byteorder-lite 0.1.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. Signed write_i24 and write_int additionally serialize the low 24 or 8nbytes bits for every signed input value, preserving suffix bytes; no signed representability condition is required. Invalid byte counts or short buffers panic as specified. Signed read_int/read_i24 additionally return the exact two-complement prefix decode at the selected width; all invalid counts and short inputs assert before sign extension. LittleEndian from_slice_u16/u32/u64/u128 and from_slice_i16/i32/i64/i128 additionally leave every slice unchanged on the verified little-endian target, including empty slices and all element values. Native LittleEndian from_slice_f32/f64 also preserve every memory bit under the existing representations, including NaN payloads and signed zeros; this is not a Rust floating PartialEq claim. The two handwritten Default methods always panic. The four variable-width unsigned writers additionally have exact byte-count/space guards, selected-byte output on success and assertion failure otherwise. Unsigned 24-bit readers/writers additionally have exact 3-byte decoding/serialization, a 24-bit value domain and complete short-buffer/value-overflow failures. Four unsigned variable-width readers decode the exact selected prefix under their complete byte-count/input-length guard, and assert otherwise. Eight concrete original 48-bit default methods are also verified: unsigned reads decode six bytes below 2^48; unsigned writes require a value below 2^48; signed reads decode six-byte two-complement values; signed writes truncate every i64 input to its low 48 bits. Enough buffer space preserves the suffix; short buffers fail assertion. Each original default body is connected by definitional equality to its original concrete general-width callee with count six. BE/LE read_int128 and write_int128 also cover all values and counts: signed reads decode the selected prefix for counts1..16 with enough input and assert otherwise; signed writes serialize the low8count bits of every i128, preserving suffix bytes. Invalid write counts0 or above16 fail integerOverflow in unextend_sign128 before the writer; valid counts with insufficient output assert. Actual original unsigned128 callees are linked by definitional equality to existing general contracts; original extend_sign128/unextend_sign128 bodies are proved directly with no new models.

Findings (0)

No findings reported.

APIs (64)

Recorded callables

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

Claim #9

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

Claim #40

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

Claim #55

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

Claim #39

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

Claim #61

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

Claim #31

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

Claim #53

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

Claim #27

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

Claim #28

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

Claim #23

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

Claim #24

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

Claim #14

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

Claim #11

<byteorder_lite::BigEndian as byteorder_lite::ByteOrder>::write_i24 recorded callable · signature and safety not recorded

Claim #36

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

Claim #12

<byteorder_lite::BigEndian as byteorder_lite::ByteOrder>::write_i48 recorded callable · signature and safety not recorded

Claim #56

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

Claim #13

<byteorder_lite::BigEndian as byteorder_lite::ByteOrder>::write_int recorded callable · signature and safety not recorded

Claim #35

<byteorder_lite::BigEndian as byteorder_lite::ByteOrder>::write_int128 recorded callable · signature and safety not recorded

Claim #62

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

Claim #4

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

Claim #1

<byteorder_lite::BigEndian as byteorder_lite::ByteOrder>::write_u24 recorded callable · signature and safety not recorded

Claim #32

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

Claim #2

<byteorder_lite::BigEndian as byteorder_lite::ByteOrder>::write_u48 recorded callable · signature and safety not recorded

Claim #54

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

Claim #3

<byteorder_lite::BigEndian as byteorder_lite::ByteOrder>::write_uint recorded callable · signature and safety not recorded

Claim #19

<byteorder_lite::BigEndian as byteorder_lite::ByteOrder>::write_uint128 recorded callable · signature and safety not recorded

Claim #20

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

Claim #10

<byteorder_lite::LittleEndian as byteorder_lite::ByteOrder>::from_slice_f32 recorded callable · signature and safety not recorded

Claim #51

<byteorder_lite::LittleEndian as byteorder_lite::ByteOrder>::from_slice_f64 recorded callable · signature and safety not recorded

Claim #52

<byteorder_lite::LittleEndian as byteorder_lite::ByteOrder>::from_slice_i128 recorded callable · signature and safety not recorded

Claim #50

<byteorder_lite::LittleEndian as byteorder_lite::ByteOrder>::from_slice_i16 recorded callable · signature and safety not recorded

Claim #47

<byteorder_lite::LittleEndian as byteorder_lite::ByteOrder>::from_slice_i32 recorded callable · signature and safety not recorded

Claim #48

<byteorder_lite::LittleEndian as byteorder_lite::ByteOrder>::from_slice_i64 recorded callable · signature and safety not recorded

Claim #49

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

Claim #46

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

Claim #43

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

Claim #44

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

Claim #45

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

Claim #42

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

Claim #59

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

Claim #41

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

Claim #63

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

Claim #33

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

Claim #57

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

Claim #29

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

Claim #30

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

Claim #25

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

Claim #26

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

Claim #18

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

Claim #15

<byteorder_lite::LittleEndian as byteorder_lite::ByteOrder>::write_i24 recorded callable · signature and safety not recorded

Claim #38

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

Claim #16

<byteorder_lite::LittleEndian as byteorder_lite::ByteOrder>::write_i48 recorded callable · signature and safety not recorded

Claim #60

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

Claim #17

<byteorder_lite::LittleEndian as byteorder_lite::ByteOrder>::write_int recorded callable · signature and safety not recorded

Claim #37

<byteorder_lite::LittleEndian as byteorder_lite::ByteOrder>::write_int128 recorded callable · signature and safety not recorded

Claim #64

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

Claim #8

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

Claim #5

<byteorder_lite::LittleEndian as byteorder_lite::ByteOrder>::write_u24 recorded callable · signature and safety not recorded

Claim #34

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

Claim #6

<byteorder_lite::LittleEndian as byteorder_lite::ByteOrder>::write_u48 recorded callable · signature and safety not recorded

Claim #58

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

Claim #7

<byteorder_lite::LittleEndian as byteorder_lite::ByteOrder>::write_uint recorded callable · signature and safety not recorded

Claim #21

<byteorder_lite::LittleEndian as byteorder_lite::ByteOrder>::write_uint128 recorded callable · signature and safety not recorded

Claim #22

Evidence

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

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/nyuichi/rust-crate-proofs report-33-source-1
git -C report-33-source-1 checkout --detach a9e18dc8a6e7f56a7a77a6ed4b6cc00b635222e3
git -C report-33-source-1 submodule update --init --recursive --checkout
cd report-33-source-1/byteorder-lite/0.1.0/aeneas/2026-11-05/proofs

lake build +FloatProofs +NativeFloatIdentityProofs +NativeIdentityProofs +Proofs +ReadVariableProofs +Signed128Reads +Signed128WriteContracts +SignedProofs +SignedReadProofs +SignedVariableContracts +U24Exact24 +U24Write24 +U48Proofs +VariableProofs

printf '%s' 'import Lean
import FloatProofs
import NativeFloatIdentityProofs
import NativeIdentityProofs
import Proofs
import ReadVariableProofs
import Signed128Reads
import Signed128WriteContracts
import SignedProofs
import SignedReadProofs
import SignedVariableContracts
import U24Exact24
import U24Write24
import U48Proofs
import VariableProofs
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 := `VariableProofs.be_write_uint_contract
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: VariableProofs.be_write_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 VariableProofs.be_write_uint_contract: {ax}"
  liftIO <| IO.println "proofs.rs:checked:VariableProofs.be_write_uint_contract"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2026-11-05T08:08:04.483903382+00:00 · 144.4 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 VariableProofs.be_write_uint_contract; axioms limited to propext, Classical.choice, Quot.sound `VariableProofs.be_write_uint_contract`	Passed	Claim #19
Lean checked theorem VariableProofs.be_write_uint128_contract; axioms limited to propext, Classical.choice, Quot.sound `VariableProofs.be_write_uint128_contract`	Passed	Claim #20
Lean checked theorem VariableProofs.le_write_uint_contract; axioms limited to propext, Classical.choice, Quot.sound `VariableProofs.le_write_uint_contract`	Passed	Claim #21
Lean checked theorem VariableProofs.le_write_uint128_contract; axioms limited to propext, Classical.choice, Quot.sound `VariableProofs.le_write_uint128_contract`	Passed	Claim #22
Lean checked theorem FloatProofs.be_write_f32_contract; axioms limited to propext, Classical.choice, Quot.sound `FloatProofs.be_write_f32_contract`	Passed	Claim #23
Lean checked theorem FloatProofs.be_write_f64_contract; axioms limited to propext, Classical.choice, Quot.sound `FloatProofs.be_write_f64_contract`	Passed	Claim #24
Lean checked theorem FloatProofs.le_write_f32_contract; axioms limited to propext, Classical.choice, Quot.sound `FloatProofs.le_write_f32_contract`	Passed	Claim #25
Lean checked theorem FloatProofs.le_write_f64_contract; axioms limited to propext, Classical.choice, Quot.sound `FloatProofs.le_write_f64_contract`	Passed	Claim #26
Lean checked theorem ReadVariableProofs.be_read_uint_contract; axioms limited to propext, Classical.choice, Quot.sound `ReadVariableProofs.be_read_uint_contract`	Passed	Claim #27
Lean checked theorem ReadVariableProofs.be_read_uint128_contract; axioms limited to propext, Classical.choice, Quot.sound `ReadVariableProofs.be_read_uint128_contract`	Passed	Claim #28
Lean checked theorem ReadVariableProofs.le_read_uint_contract; axioms limited to propext, Classical.choice, Quot.sound `ReadVariableProofs.le_read_uint_contract`	Passed	Claim #29
Lean checked theorem ReadVariableProofs.le_read_uint128_contract; axioms limited to propext, Classical.choice, Quot.sound `ReadVariableProofs.le_read_uint128_contract`	Passed	Claim #30
Lean checked theorem U24Proofs.be_read_u24_contract; axioms limited to propext, Classical.choice, Quot.sound `U24Proofs.be_read_u24_contract`	Passed	Claim #31
Lean checked theorem U24Writes.be_write_u24_contract; axioms limited to propext, Classical.choice, Quot.sound `U24Writes.be_write_u24_contract`	Passed	Claim #32
Lean checked theorem U24Proofs.le_read_u24_contract; axioms limited to propext, Classical.choice, Quot.sound `U24Proofs.le_read_u24_contract`	Passed	Claim #33
Lean checked theorem U24Writes.le_write_u24_contract; axioms limited to propext, Classical.choice, Quot.sound `U24Writes.le_write_u24_contract`	Passed	Claim #34
Lean checked theorem SignedWrites.be_write_int_contract; axioms limited to propext, Classical.choice, Quot.sound `SignedWrites.be_write_int_contract`	Passed	Claim #35
Lean checked theorem SignedWrites.be_write_i24_contract; axioms limited to propext, Classical.choice, Quot.sound `SignedWrites.be_write_i24_contract`	Passed	Claim #36
Lean checked theorem SignedWrites.le_write_int_contract; axioms limited to propext, Classical.choice, Quot.sound `SignedWrites.le_write_int_contract`	Passed	Claim #37
Lean checked theorem SignedWrites.le_write_i24_contract; axioms limited to propext, Classical.choice, Quot.sound `SignedWrites.le_write_i24_contract`	Passed	Claim #38
Lean checked theorem SignedReadProofs.be_read_int_contract; axioms limited to propext, Classical.choice, Quot.sound `SignedReadProofs.be_read_int_contract`	Passed	Claim #39
Lean checked theorem SignedReadProofs.be_read_i24_contract; axioms limited to propext, Classical.choice, Quot.sound `SignedReadProofs.be_read_i24_contract`	Passed	Claim #40
Lean checked theorem SignedReadProofs.le_read_int_contract; axioms limited to propext, Classical.choice, Quot.sound `SignedReadProofs.le_read_int_contract`	Passed	Claim #41
Lean checked theorem SignedReadProofs.le_read_i24_contract; axioms limited to propext, Classical.choice, Quot.sound `SignedReadProofs.le_read_i24_contract`	Passed	Claim #42
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 #43
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 #44
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 #45
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 #46
Lean checked theorem NativeIdentityProofs.le_from_slice_i16_identity; axioms limited to propext, Classical.choice, Quot.sound `NativeIdentityProofs.le_from_slice_i16_identity`	Passed	Claim #47
Lean checked theorem NativeIdentityProofs.le_from_slice_i32_identity; axioms limited to propext, Classical.choice, Quot.sound `NativeIdentityProofs.le_from_slice_i32_identity`	Passed	Claim #48
Lean checked theorem NativeIdentityProofs.le_from_slice_i64_identity; axioms limited to propext, Classical.choice, Quot.sound `NativeIdentityProofs.le_from_slice_i64_identity`	Passed	Claim #49
Lean checked theorem NativeIdentityProofs.le_from_slice_i128_identity; axioms limited to propext, Classical.choice, Quot.sound `NativeIdentityProofs.le_from_slice_i128_identity`	Passed	Claim #50
Lean checked theorem NativeFloatIdentityProofs.le_from_slice_f32_bits_identity; axioms limited to propext, Classical.choice, Quot.sound `NativeFloatIdentityProofs.le_from_slice_f32_bits_identity`	Passed	Claim #51
Lean checked theorem NativeFloatIdentityProofs.le_from_slice_f64_bits_identity; axioms limited to propext, Classical.choice, Quot.sound `NativeFloatIdentityProofs.le_from_slice_f64_bits_identity`	Passed	Claim #52
Lean checked theorem U48Proofs.be_read_u48_final; axioms limited to propext, Classical.choice, Quot.sound `U48Proofs.be_read_u48_final`	Passed	Claim #53
Lean checked theorem U48Proofs.be_write_u48_plain; axioms limited to propext, Classical.choice, Quot.sound `U48Proofs.be_write_u48_plain`	Passed	Claim #54
Lean checked theorem U48Proofs.be_read_i48_final; axioms limited to propext, Classical.choice, Quot.sound `U48Proofs.be_read_i48_final`	Passed	Claim #55
Lean checked theorem U48Proofs.be_write_i48_final; axioms limited to propext, Classical.choice, Quot.sound `U48Proofs.be_write_i48_final`	Passed	Claim #56
Lean checked theorem U48Proofs.le_read_u48_final; axioms limited to propext, Classical.choice, Quot.sound `U48Proofs.le_read_u48_final`	Passed	Claim #57
Lean checked theorem U48Proofs.le_write_u48_plain; axioms limited to propext, Classical.choice, Quot.sound `U48Proofs.le_write_u48_plain`	Passed	Claim #58
Lean checked theorem U48Proofs.le_read_i48_final; axioms limited to propext, Classical.choice, Quot.sound `U48Proofs.le_read_i48_final`	Passed	Claim #59
Lean checked theorem U48Proofs.le_write_i48_final; axioms limited to propext, Classical.choice, Quot.sound `U48Proofs.le_write_i48_final`	Passed	Claim #60
Lean checked theorem Signed128Reads.be_read_int128_contract; axioms limited to propext, Classical.choice, Quot.sound `Signed128Reads.be_read_int128_contract`	Passed	Claim #61
Lean checked theorem Signed128Writes.be_write_int128_contract; axioms limited to propext, Classical.choice, Quot.sound `Signed128Writes.be_write_int128_contract`	Passed	Claim #62
Lean checked theorem Signed128Reads.le_read_int128_contract; axioms limited to propext, Classical.choice, Quot.sound `Signed128Reads.le_read_int128_contract`	Passed	Claim #63
Lean checked theorem Signed128Writes.le_write_int128_contract; axioms limited to propext, Classical.choice, Quot.sound `Signed128Writes.le_write_int128_contract`	Passed	Claim #64

Execution details

Started: 2026-11-05T08:08:04.483903382+00:00
Finished: 2026-11-05T08:10:28.859055408+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-lite/0.1.0/aeneas/2026-11-05/proofs
Environment overrides: None recorded
Git repository: https://github.com/nyuichi/rust-crate-proofs
Git commit: a9e18dc8a6e7f56a7a77a6ed4b6cc00b635222e3

Diagnostics & logs

=== stdout ===
⚠ [2/43] Ran aeneas:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
✔ [3/43] Built Aeneas.Std.Global (36s)
✔ [4/43] Built AeneasMeta.Simp.RegisterCommand (36s)
✔ [9/413] Built AeneasMeta.UtilsCore (36s)
✔ [1576/1848] Built AeneasMeta.BvEnumToBitVec (37s)
✔ [1798/1848] Built SignedReadRoots.Types (2.1s)
✔ [1799/1848] Built ByteorderLiteU24Roots.Types (2.2s)
✔ [1800/1848] Built LiteSigned128Roots.Types (2.3s)
✔ [1801/1848] Built SignedVariableRoots.Types (2.4s)
⚠ [1802/1848] Built Signed128Math (3.5s)
warning: Signed128Math.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: Signed128Math.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: Signed128Math.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: Signed128Math.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: Signed128Math.lean:52:0: 'Signed128Math.signed_low_bits' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Signed128Math.lean:54:0: 'Signed128Math.zero_padding_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Signed128Math.lean:56:0: 'Signed128Math.zero_padding_be_val' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [1803/1848] Built ByteorderLiteApiRoots.Types (2.2s)
✔ [1804/1848] Built ReadVariableGenerated.ByteorderLite (2.5s)
✔ [1805/1848] Built Generated.ByteorderLite (2.7s)
✔ [1806/1848] Built VariableGenerated.ByteorderLite (2.7s)
✔ [1807/1848] Built ByteorderLite.Types (2.4s)
✔ [1808/1848] Built ByteorderLiteFloatRoots.Types (2.2s)
✔ [1809/1848] Built ByteorderLiteU48Roots.Types (2.4s)
✔ [1810/1848] Built SignedReadRoots.Funs (2.6s)
✔ [1811/1848] Built ByteorderLiteU24Roots.Funs (2.7s)
✔ [1812/1848] Built LiteSigned128Roots.Funs (2.8s)
✔ [1813/1848] Built SignedVariableRoots.Funs (2.7s)
✔ [1814/1848] Built ByteorderLiteApiRoots.Funs (2.7s)
✔ [1815/1848] Built ByteorderLiteFloatRoots.FunsExternal (2.7s)
✔ [1816/1848] Built ByteorderLiteU48Roots.Funs (4.1s)
⚠ [1817/1848] Built VariableProofs (16s)
info: VariableProofs.lean:40:0: 'VariableProofs.pack_size_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: VariableProofs.lean:61:0: 'VariableProofs.be_write_uint_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: VariableProofs.lean:114:2: Unused tactic linter: `all_goals omega` does nothing.

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

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: VariableProofs.lean:151:2: Unused tactic linter: `all_goals omega` does nothing.

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

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
info: VariableProofs.lean:154:0: 'VariableProofs.be_write_uint_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: VariableProofs.lean:155:0: 'VariableProofs.be_write_uint128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: VariableProofs.lean:156:0: 'VariableProofs.le_write_uint_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: VariableProofs.lean:157:0: 'VariableProofs.le_write_uint128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: VariableProofs.lean:179: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: VariableProofs.lean:179: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: VariableProofs.lean:180: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: VariableProofs.lean:180: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: VariableProofs.lean:181: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: VariableProofs.lean:181: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: VariableProofs.lean:181: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: VariableProofs.lean:183:0: 'VariableProofs.be_write_uint_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: VariableProofs.lean:199: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: VariableProofs.lean:199: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: VariableProofs.lean:200: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: VariableProofs.lean:200: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: VariableProofs.lean:201: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: VariableProofs.lean:201: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: VariableProofs.lean:201: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: VariableProofs.lean:216: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: VariableProofs.lean:216: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: VariableProofs.lean:217: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: VariableProofs.lean:217: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: VariableProofs.lean:218: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: VariableProofs.lean:218: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: VariableProofs.lean:218: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: VariableProofs.lean:233: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: VariableProofs.lean:233: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: VariableProofs.lean:234: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: VariableProofs.lean:234: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: VariableProofs.lean:235: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: VariableProofs.lean:235: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: VariableProofs.lean:235: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: VariableProofs.lean:270:0: 'VariableProofs.be_write_uint_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: VariableProofs.lean:271:0: 'VariableProofs.be_write_uint128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: VariableProofs.lean:272:0: 'VariableProofs.le_write_uint_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: VariableProofs.lean:273:0: 'VariableProofs.le_write_uint128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1818/1848] Built SignedVariableWriteSupport (11s)
warning: SignedVariableWriteSupport.lean:76:2: Unused tactic linter: `all_goals omega` does nothing.

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

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: SignedVariableWriteSupport.lean:100: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: SignedVariableWriteSupport.lean:100: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: SignedVariableWriteSupport.lean:101: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: SignedVariableWriteSupport.lean:101: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: SignedVariableWriteSupport.lean:102: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: SignedVariableWriteSupport.lean:102: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: SignedVariableWriteSupport.lean:102: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: SignedVariableWriteSupport.lean:117: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: SignedVariableWriteSupport.lean:117: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: SignedVariableWriteSupport.lean:118: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: SignedVariableWriteSupport.lean:118: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: SignedVariableWriteSupport.lean:119: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: SignedVariableWriteSupport.lean:119: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: SignedVariableWriteSupport.lean:119: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`
✔ [1819/1848] Built ByteorderLiteFloatRoots.Funs (3.8s)
⚠ [1820/1848] Built SignedProofs (7.3s)
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]
✔ [1821/1848] Built ByteorderLite.FunsExternal (3.0s)
ℹ [1822/1848] Built SignedVariableProofs (3.7s)
info: SignedVariableProofs.lean:37:0: 'SignedWrites.unextend_sign_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1823/1848] Built FloatProofs (3.7s)
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]
⚠ [1824/1848] Built ReadVariableProofs (30s)
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]
✔ [1825/1848] Built ByteorderLite.Funs (2.6s)
⚠ [1826/1848] Built SignedReadSupport (29s)
warning: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.lean:191:0: 'SignedReadSupport.be_read_uint_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadSupport.lean:193:0: 'SignedReadSupport.be_read_uint128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadSupport.lean:195:0: 'SignedReadSupport.le_read_uint_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadSupport.lean:197:0: 'SignedReadSupport.le_read_uint128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadSupport.lean:199:0: 'SignedReadSupport.be_read_uint_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadSupport.lean:201:0: 'SignedReadSupport.le_read_uint_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadSupport.lean:202:0: 'SignedReadSupport.be_read_uint128_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadSupport.lean:203:0: 'SignedReadSupport.le_read_uint128_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.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: SignedReadSupport.lean:243:0: 'SignedReadSupport.be_read_uint_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadSupport.lean:244:0: 'SignedReadSupport.be_read_uint128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadSupport.lean:245:0: 'SignedReadSupport.le_read_uint_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadSupport.lean:246:0: 'SignedReadSupport.le_read_uint128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1827/1848] Built SignedVariableNormal (3.5s)
warning: SignedVariableNormal.lean:33:27: `if_neg` has been deprecated: Use `ite_eq_right` instead

Hint: Replace the deprecated name:
  i̵f̵_̵n̵e̵g̵i̲t̲e̲_̲e̲q̲_̲r̲i̲g̲h̲t̲
info: SignedVariableNormal.lean:78:0: 'SignedWrites.be_write_int_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedVariableNormal.lean:80:0: 'SignedWrites.le_write_int_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [1828/1848] Built Signed128Support (3.7s)
ℹ [1829/1848] Built NativeIdentityProofs (2.9s)
info: NativeIdentityProofs.lean:29:0: 'NativeIdentityProofs.le_from_slice_u16_identity' depends on axioms: [propext, Quot.sound]
info: NativeIdentityProofs.lean:30:0: 'NativeIdentityProofs.le_from_slice_u32_identity' depends on axioms: [propext, Quot.sound]
info: NativeIdentityProofs.lean:31:0: 'NativeIdentityProofs.le_from_slice_u64_identity' depends on axioms: [propext, Quot.sound]
info: NativeIdentityProofs.lean:32:0: 'NativeIdentityProofs.le_from_slice_u128_identity' depends on axioms: [propext, Quot.sound]
info: NativeIdentityProofs.lean:33:0: 'NativeIdentityProofs.le_from_slice_i16_identity' depends on axioms: [propext, Quot.sound]
info: NativeIdentityProofs.lean:34:0: 'NativeIdentityProofs.le_from_slice_i32_identity' depends on axioms: [propext, Quot.sound]
info: NativeIdentityProofs.lean:35:0: 'NativeIdentityProofs.le_from_slice_i64_identity' depends on axioms: [propext, Quot.sound]
info: NativeIdentityProofs.lean:36:0: 'NativeIdentityProofs.le_from_slice_i128_identity' depends on axioms: [propext, Quot.sound]
ℹ [1830/1848] Built NativeFloatIdentityProofs (3.1s)
info: NativeFloatIdentityProofs.lean:9:0: 'NativeFloatIdentityProofs.le_from_slice_f32_bits_identity' depends on axioms: [propext, Quot.sound]
info: NativeFloatIdentityProofs.lean:10:0: 'NativeFloatIdentityProofs.le_from_slice_f64_bits_identity' depends on axioms: [propext, Quot.sound]
⚠ [1831/1848] Built Proofs (4.7s)
info: Proofs.lean:88:0: 'Proofs.be_write_u16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:89:0: 'Proofs.be_write_u32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:90:0: 'Proofs.be_write_u64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:91:0: 'Proofs.be_write_u128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:92:0: 'Proofs.le_write_u16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:93:0: 'Proofs.le_write_u32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:94:0: 'Proofs.le_write_u64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:95:0: 'Proofs.le_write_u128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:98:0: 'Proofs.BigEndian_default_panics' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:100:0: 'Proofs.LittleEndian_default_panics' depends on axioms: [propext, Quot.sound]
warning: Proofs.lean:107: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:121: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:135: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:149: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:163: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:177: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:191: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:205: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:217:0: 'Proofs.be_write_u16_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:218:0: 'Proofs.be_write_u32_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:219:0: 'Proofs.be_write_u64_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:220:0: 'Proofs.be_write_u128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:221:0: 'Proofs.le_write_u16_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:222:0: 'Proofs.le_write_u32_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:223:0: 'Proofs.le_write_u64_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:224:0: 'Proofs.le_write_u128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1832/1848] Built U24ReadSupport (32s)
warning: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.lean:191:0: 'U24ReadSupport.be_read_uint_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24ReadSupport.lean:193:0: 'U24ReadSupport.be_read_uint128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24ReadSupport.lean:195:0: 'U24ReadSupport.le_read_uint_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24ReadSupport.lean:197:0: 'U24ReadSupport.le_read_uint128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24ReadSupport.lean:199:0: 'U24ReadSupport.be_read_uint_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24ReadSupport.lean:201:0: 'U24ReadSupport.le_read_uint_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24ReadSupport.lean:202:0: 'U24ReadSupport.be_read_uint128_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24ReadSupport.lean:203:0: 'U24ReadSupport.le_read_uint128_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.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: U24ReadSupport.lean:243:0: 'U24ReadSupport.be_read_uint_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24ReadSupport.lean:244:0: 'U24ReadSupport.be_read_uint128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24ReadSupport.lean:245:0: 'U24ReadSupport.le_read_uint_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24ReadSupport.lean:246:0: 'U24ReadSupport.le_read_uint128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1833/1848] Built SignedVariableFailure (3.0s)
warning: SignedVariableFailure.lean:23:10: `if_pos` has been deprecated: Use `ite_eq_left` instead

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

Hint: Replace the deprecated name:
  i̵f̵_̵n̵e̵g̵i̲t̲e̲_̲e̲q̲_̲r̲i̲g̲h̲t̲
info: SignedVariableFailure.lean:59:0: 'SignedWrites.unextend_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedVariableFailure.lean:60:0: 'SignedWrites.unextend_large' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedVariableFailure.lean:105:0: 'SignedWrites.be_write_int_bad_count' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedVariableFailure.lean:106:0: 'SignedWrites.be_write_int_short' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedVariableFailure.lean:107:0: 'SignedWrites.le_write_int_bad_count' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedVariableFailure.lean:108:0: 'SignedWrites.le_write_int_short' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1834/1848] Built Signed128WriteHelper (3.4s)
info: Signed128WriteHelper.lean:37:0: 'Signed128Writes.unextend_sign128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1835/1848] Built Signed128Reads (3.7s)
info: Signed128Reads.lean:103:0: 'Signed128Reads.be_read_int128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Signed128Reads.lean:104:0: 'Signed128Reads.le_read_int128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1836/1848] Built U24Decode24 (4.3s)
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]
⚠ [1837/1848] Built U24WriteSupport (4.6s)
warning: U24WriteSupport.lean:76:2: Unused tactic linter: `all_goals omega` does nothing.

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

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: U24WriteSupport.lean:100: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: U24WriteSupport.lean:100: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: U24WriteSupport.lean:101: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: U24WriteSupport.lean:101: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: U24WriteSupport.lean:102: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: U24WriteSupport.lean:102: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: U24WriteSupport.lean:102: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: U24WriteSupport.lean:117: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: U24WriteSupport.lean:117: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: U24WriteSupport.lean:118: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: U24WriteSupport.lean:118: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: U24WriteSupport.lean:119: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: U24WriteSupport.lean:119: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: U24WriteSupport.lean:119: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`
⚠ [1838/1848] Built U24WrapperProofs (3.2s)
info: U24WrapperProofs.lean:20:0: 'U24Proofs.be_read_u24_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24WrapperProofs.lean:21:0: 'U24Proofs.le_read_u24_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: U24WrapperProofs.lean:32: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:41: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:43:0: 'U24Proofs.be_read_u24_short' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24WrapperProofs.lean:44:0: 'U24Proofs.le_read_u24_short' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1839/1848] Built SignedVariableI24 (3.2s)
info: SignedVariableI24.lean:21:0: 'SignedWrites.i32_low24' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedVariableI24.lean:53:0: 'SignedWrites.be_write_i24_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedVariableI24.lean:54:0: 'SignedWrites.be_write_i24_short' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedVariableI24.lean:55:0: 'SignedWrites.le_write_i24_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedVariableI24.lean:56:0: 'SignedWrites.le_write_i24_short' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1840/1848] Built Signed128WriteNormal (3.3s)
warning: Signed128WriteNormal.lean:34:27: `if_neg` has been deprecated: Use `ite_eq_right` instead

Hint: Replace the deprecated name:
  i̵f̵_̵n̵e̵g̵i̲t̲e̲_̲e̲q̲_̲r̲i̲g̲h̲t̲
info: Signed128WriteNormal.lean:79:0: 'Signed128Writes.be_write_int128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Signed128WriteNormal.lean:81:0: 'Signed128Writes.le_write_int128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1841/1848] Built U24Exact24 (2.6s)
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]
⚠ [1842/1848] Built U24Write24 (2.6s)
warning: U24Write24.lean:39:27: `if_neg` has been deprecated: Use `ite_eq_right` instead

Hint: Replace the deprecated name:
  i̵f̵_̵n̵e̵g̵i̲t̲e̲_̲e̲q̲_̲r̲i̲g̲h̲t̲
info: U24Write24.lean:43:0: 'U24Writes.fits24' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24Write24.lean:91:0: 'U24Writes.be_write_u24_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24Write24.lean:92:0: 'U24Writes.be_write_u24_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24Write24.lean:93:0: 'U24Writes.le_write_u24_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24Write24.lean:94:0: 'U24Writes.le_write_u24_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24Write24.lean:114:0: 'U24Writes.be_write_u24_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U24Write24.lean:115:0: 'U24Writes.le_write_u24_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1843/1848] Built SignedVariableContracts (2.3s)
info: SignedVariableContracts.lean:46:0: 'SignedWrites.be_write_int_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedVariableContracts.lean:47:0: 'SignedWrites.be_write_i24_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedVariableContracts.lean:48:0: 'SignedWrites.le_write_int_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedVariableContracts.lean:49:0: 'SignedWrites.le_write_i24_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1844/1848] Built Signed128WriteFailure (2.7s)
warning: Signed128WriteFailure.lean:24:10: `if_pos` has been deprecated: Use `ite_eq_left` instead

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

Hint: Replace the deprecated name:
  i̵f̵_̵n̵e̵g̵i̲t̲e̲_̲e̲q̲_̲r̲i̲g̲h̲t̲
info: Signed128WriteFailure.lean:60:0: 'Signed128Writes.unextend_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Signed128WriteFailure.lean:61:0: 'Signed128Writes.unextend_large' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Signed128WriteFailure.lean:106:0: 'Signed128Writes.be_write_int128_bad_count' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Signed128WriteFailure.lean:107:0: 'Signed128Writes.be_write_int128_short' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Signed128WriteFailure.lean:108:0: 'Signed128Writes.le_write_int128_bad_count' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Signed128WriteFailure.lean:109:0: 'Signed128Writes.le_write_int128_short' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1845/1848] Built SignedDecodeMath (2.3s)
warning: SignedDecodeMath.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: SignedDecodeMath.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: SignedDecodeMath.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: SignedDecodeMath.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: SignedDecodeMath.lean:52:0: 'SignedDecodeMath.signed_low_bits' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedDecodeMath.lean:54:0: 'SignedDecodeMath.zero_padding_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedDecodeMath.lean:56:0: 'SignedDecodeMath.zero_padding_be_val' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1846/1848] Built Signed128WriteContracts (2.1s)
info: Signed128WriteContracts.lean:30:0: 'Signed128Writes.be_write_int128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Signed128WriteContracts.lean:31:0: 'Signed128Writes.le_write_int128_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1847/1848] Built SignedReadProofs (3.1s)
info: SignedReadProofs.lean:29:0: 'SignedReadProofs.extend_sign_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadProofs.lean:75:0: 'SignedReadProofs.be_read_int_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadProofs.lean:76:0: 'SignedReadProofs.le_read_int_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadProofs.lean:124:0: 'SignedReadProofs.be_read_int_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadProofs.lean:125:0: 'SignedReadProofs.be_read_i24_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadProofs.lean:126:0: 'SignedReadProofs.le_read_int_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadProofs.lean:127:0: 'SignedReadProofs.le_read_i24_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadProofs.lean:181:0: 'SignedReadProofs.be_read_int_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadProofs.lean:182:0: 'SignedReadProofs.be_read_i24_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadProofs.lean:183:0: 'SignedReadProofs.le_read_int_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SignedReadProofs.lean:184:0: 'SignedReadProofs.le_read_i24_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1848/1848] Built U48Proofs (2.7s)
warning: U48Proofs.lean:17: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: U48Proofs.lean:17:38: 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: U48Proofs.lean:18: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: U48Proofs.lean:49: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: U48Proofs.lean:49:38: 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: U48Proofs.lean:50: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: U48Proofs.lean:107:27: `if_neg` has been deprecated: Use `ite_eq_right` instead

Hint: Replace the deprecated name:
  i̵f̵_̵n̵e̵g̵i̲t̲e̲_̲e̲q̲_̲r̲i̲g̲h̲t̲
info: U48Proofs.lean:248:0: 'U48Proofs.be_read_u48_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:249:0: 'U48Proofs.be_write_u48_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:250:0: 'U48Proofs.be_read_i48_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:251:0: 'U48Proofs.be_write_i48_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:252:0: 'U48Proofs.le_read_u48_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:253:0: 'U48Proofs.le_write_u48_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:254:0: 'U48Proofs.le_read_i48_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:255:0: 'U48Proofs.le_write_i48_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:257:0: 'U48Proofs.fits48' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:258:0: 'U48Proofs.signed_low48' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:260:0: 'U48Proofs.be_read_u48_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:261:0: 'U48Proofs.be_read_i48_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:262:0: 'U48Proofs.be_write_u48_plain' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:263:0: 'U48Proofs.le_read_u48_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:264:0: 'U48Proofs.le_read_i48_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:265:0: 'U48Proofs.le_write_u48_plain' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:267:0: 'U48Proofs.be_read_u48_final' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:268:0: 'U48Proofs.be_read_i48_final' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:269:0: 'U48Proofs.be_write_i48_final' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:270:0: 'U48Proofs.le_read_u48_final' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:271:0: 'U48Proofs.le_read_i48_final' depends on axioms: [propext, Classical.choice, Quot.sound]
info: U48Proofs.lean:272:0: 'U48Proofs.le_write_i48_final' depends on axioms: [propext, Classical.choice, Quot.sound]
Build completed successfully (1848 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:VariableProofs.be_write_uint_contract
proofs.rs:checked:VariableProofs.be_write_uint128_contract
proofs.rs:checked:VariableProofs.le_write_uint_contract
proofs.rs:checked:VariableProofs.le_write_uint128_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:U24Writes.be_write_u24_contract
proofs.rs:checked:U24Proofs.le_read_u24_contract
proofs.rs:checked:U24Writes.le_write_u24_contract
proofs.rs:checked:SignedWrites.be_write_int_contract
proofs.rs:checked:SignedWrites.be_write_i24_contract
proofs.rs:checked:SignedWrites.le_write_int_contract
proofs.rs:checked:SignedWrites.le_write_i24_contract
proofs.rs:checked:SignedReadProofs.be_read_int_contract
proofs.rs:checked:SignedReadProofs.be_read_i24_contract
proofs.rs:checked:SignedReadProofs.le_read_int_contract
proofs.rs:checked:SignedReadProofs.le_read_i24_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:NativeIdentityProofs.le_from_slice_i16_identity
proofs.rs:checked:NativeIdentityProofs.le_from_slice_i32_identity
proofs.rs:checked:NativeIdentityProofs.le_from_slice_i64_identity
proofs.rs:checked:NativeIdentityProofs.le_from_slice_i128_identity
proofs.rs:checked:NativeFloatIdentityProofs.le_from_slice_f32_bits_identity
proofs.rs:checked:NativeFloatIdentityProofs.le_from_slice_f64_bits_identity
proofs.rs:checked:U48Proofs.be_read_u48_final
proofs.rs:checked:U48Proofs.be_write_u48_plain
proofs.rs:checked:U48Proofs.be_read_i48_final
proofs.rs:checked:U48Proofs.be_write_i48_final
proofs.rs:checked:U48Proofs.le_read_u48_final
proofs.rs:checked:U48Proofs.le_write_u48_plain
proofs.rs:checked:U48Proofs.le_read_i48_final
proofs.rs:checked:U48Proofs.le_write_i48_final
proofs.rs:checked:Signed128Reads.be_read_int128_contract
proofs.rs:checked:Signed128Writes.be_write_int128_contract
proofs.rs:checked:Signed128Reads.le_read_int128_contract
proofs.rs:checked:Signed128Writes.le_write_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.

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 ten native conversion bodies make no external calls after official target-branch translation. Thirteen native-path declarations remain in the unchanged, unimported external template. The native provider imports the existing bit-pattern representation module and supplies zero new definitions or operation models; native bodies invoke no external operation. Existing to_bits models remain used by the earlier float writers only. Guards require exactly the original identity bodies and zero external use. Mapped audits permit only propext, Classical.choice and Quot.sound.

Technical limitations

This covers 36 selected writer methods, sixteen scoped integer readers, ten native-target identity conversions, and two handwritten Default methods, not all public APIs. Fixed-width 16/32/64/128-bit reads, 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 write_int documentation says nonrepresentable values panic, while original-body theorems establish truncation for all i64 inputs when count/space guards hold; 176 finite native observations corroborate selected boundaries. This is a documentation/behavior mismatch, not a memory-safety finding. write_i24 documents only short-buffer panic and is not classified as a documentation problem. Other signed reads remain unproved. Opposite-endian conversion methods and other target configurations are not covered by the identity results. Panic messages and unwinding side effects are not specified. Separately, write_int128 documentation also says a nonrepresentable value panics; the original-body Lean theorem establishes truncation for all i128 inputs under valid count/space guards. This additional documentation contrast follows from the proof and source text, with no new native observation claimed; the176 native observations remain specific to the prior signed64/24 investigation.

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.