Report #26 — Integer From conversions and generic bitwise result preservation

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

66 verified claims · 0 findings

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

nyuichi · 2026-11-05 01:21 UTC

Revision v2 · v1

Overview

For endian-type 0.2.0, six generic BigEndian/ LittleEndian bitwise methods preserve the underlying operator result. Sixty integer From method bodies additionally implement exact identity or byte reversal under explicitly supplied x86_64 little-endian scalar-operation models. LittleEndian construction and conversion to an integer preserve the stored word; BigEndian construction and conversion to an integer reverse its bytes; cross-wrapper conversion reverses the stored word. These contracts cover every bit pattern of u16/u32/u64/u128/usize and i16/i32/i64/i128/isize. Pointer-sized Lean theorems explicitly require System.Platform.numBits=64. Original source and Cargo.toml are unchanged. Fifty executable external-operation models compose official byte primitives and are proved against independent bitvector specifications; Kani separately checks native Rust operations against explicit reversed-byte references for all inputs. Separate ordinary Kani harnesses directly check forty concrete integer byte APIs (ten harnesses, 220 checks) and sixty integer instantiations of six slice methods (1030 checks, including 180 specification assertions and 20 unsupported-path guards). The slice checks are limited to initialized, correctly aligned exact-length repr(C) leading-field buffers with arbitrary contents and replacement values; they do not establish arbitrary-T, arbitrary allocation-context, invalid/short/misaligned-buffer, or Rust aliasing guarantees. These supplemental Kani checks are not among the 66 Aeneas machine claims.

Findings (0)

No findings reported.

APIs (66)

Recorded callables

<endian_type::BigEndian<T> as core::ops::BitAnd>::bitand recorded callable · signature and safety not recorded

Claim #1

<endian_type::BigEndian<T> as core::ops::BitOr>::bitor recorded callable · signature and safety not recorded

Claim #2

<endian_type::BigEndian<T> as core::ops::BitXor>::bitxor recorded callable · signature and safety not recorded

Claim #3

<endian_type::BigEndian<i128> as From<endian_type::LittleEndian<i128>>>::from recorded callable · signature and safety not recorded

Claim #59

<endian_type::BigEndian<i128> as From<i128>>::from recorded callable · signature and safety not recorded

Claim #55

<endian_type::BigEndian<i16> as From<endian_type::LittleEndian<i16>>>::from recorded callable · signature and safety not recorded

Claim #41

<endian_type::BigEndian<i16> as From<i16>>::from recorded callable · signature and safety not recorded

Claim #37

<endian_type::BigEndian<i32> as From<endian_type::LittleEndian<i32>>>::from recorded callable · signature and safety not recorded

Claim #47

<endian_type::BigEndian<i32> as From<i32>>::from recorded callable · signature and safety not recorded

Claim #43

<endian_type::BigEndian<i64> as From<endian_type::LittleEndian<i64>>>::from recorded callable · signature and safety not recorded

Claim #53

<endian_type::BigEndian<i64> as From<i64>>::from recorded callable · signature and safety not recorded

Claim #49

<endian_type::BigEndian<isize> as From<endian_type::LittleEndian<isize>>>::from recorded callable · signature and safety not recorded

Claim #65

<endian_type::BigEndian<isize> as From<isize>>::from recorded callable · signature and safety not recorded

Claim #61

<endian_type::BigEndian<u128> as From<endian_type::LittleEndian<u128>>>::from recorded callable · signature and safety not recorded

Claim #29

<endian_type::BigEndian<u128> as From<u128>>::from recorded callable · signature and safety not recorded

Claim #25

<endian_type::BigEndian<u16> as From<endian_type::LittleEndian<u16>>>::from recorded callable · signature and safety not recorded

Claim #11

<endian_type::BigEndian<u16> as From<u16>>::from recorded callable · signature and safety not recorded

Claim #7

<endian_type::BigEndian<u32> as From<endian_type::LittleEndian<u32>>>::from recorded callable · signature and safety not recorded

Claim #17

<endian_type::BigEndian<u32> as From<u32>>::from recorded callable · signature and safety not recorded

Claim #13

<endian_type::BigEndian<u64> as From<endian_type::LittleEndian<u64>>>::from recorded callable · signature and safety not recorded

Claim #23

<endian_type::BigEndian<u64> as From<u64>>::from recorded callable · signature and safety not recorded

Claim #19

<endian_type::BigEndian<usize> as From<endian_type::LittleEndian<usize>>>::from recorded callable · signature and safety not recorded

Claim #35

<endian_type::BigEndian<usize> as From<usize>>::from recorded callable · signature and safety not recorded

Claim #31

<endian_type::LittleEndian<T> as core::ops::BitAnd>::bitand recorded callable · signature and safety not recorded

Claim #4

<endian_type::LittleEndian<T> as core::ops::BitOr>::bitor recorded callable · signature and safety not recorded

Claim #5

<endian_type::LittleEndian<T> as core::ops::BitXor>::bitxor recorded callable · signature and safety not recorded

Claim #6

<endian_type::LittleEndian<i128> as From<endian_type::BigEndian<i128>>>::from recorded callable · signature and safety not recorded

Claim #60

<endian_type::LittleEndian<i128> as From<i128>>::from recorded callable · signature and safety not recorded

Claim #56

<endian_type::LittleEndian<i16> as From<endian_type::BigEndian<i16>>>::from recorded callable · signature and safety not recorded

Claim #42

<endian_type::LittleEndian<i16> as From<i16>>::from recorded callable · signature and safety not recorded

Claim #38

<endian_type::LittleEndian<i32> as From<endian_type::BigEndian<i32>>>::from recorded callable · signature and safety not recorded

Claim #48

<endian_type::LittleEndian<i32> as From<i32>>::from recorded callable · signature and safety not recorded

Claim #44

<endian_type::LittleEndian<i64> as From<endian_type::BigEndian<i64>>>::from recorded callable · signature and safety not recorded

Claim #54

<endian_type::LittleEndian<i64> as From<i64>>::from recorded callable · signature and safety not recorded

Claim #50

<endian_type::LittleEndian<isize> as From<endian_type::BigEndian<isize>>>::from recorded callable · signature and safety not recorded

Claim #66

<endian_type::LittleEndian<isize> as From<isize>>::from recorded callable · signature and safety not recorded

Claim #62

<endian_type::LittleEndian<u128> as From<endian_type::BigEndian<u128>>>::from recorded callable · signature and safety not recorded

Claim #30

<endian_type::LittleEndian<u128> as From<u128>>::from recorded callable · signature and safety not recorded

Claim #26

<endian_type::LittleEndian<u16> as From<endian_type::BigEndian<u16>>>::from recorded callable · signature and safety not recorded

Claim #12

<endian_type::LittleEndian<u16> as From<u16>>::from recorded callable · signature and safety not recorded

Claim #8

<endian_type::LittleEndian<u32> as From<endian_type::BigEndian<u32>>>::from recorded callable · signature and safety not recorded

Claim #18

<endian_type::LittleEndian<u32> as From<u32>>::from recorded callable · signature and safety not recorded

Claim #14

<endian_type::LittleEndian<u64> as From<endian_type::BigEndian<u64>>>::from recorded callable · signature and safety not recorded

Claim #24

<endian_type::LittleEndian<u64> as From<u64>>::from recorded callable · signature and safety not recorded

Claim #20

<endian_type::LittleEndian<usize> as From<endian_type::BigEndian<usize>>>::from recorded callable · signature and safety not recorded

Claim #36

<endian_type::LittleEndian<usize> as From<usize>>::from recorded callable · signature and safety not recorded

Claim #32

<i128 as From<endian_type::BigEndian<i128>>>::from recorded callable · signature and safety not recorded

Claim #57

<i128 as From<endian_type::LittleEndian<i128>>>::from recorded callable · signature and safety not recorded

Claim #58

<i16 as From<endian_type::BigEndian<i16>>>::from recorded callable · signature and safety not recorded

Claim #39

<i16 as From<endian_type::LittleEndian<i16>>>::from recorded callable · signature and safety not recorded

Claim #40

<i32 as From<endian_type::BigEndian<i32>>>::from recorded callable · signature and safety not recorded

Claim #45

<i32 as From<endian_type::LittleEndian<i32>>>::from recorded callable · signature and safety not recorded

Claim #46

<i64 as From<endian_type::BigEndian<i64>>>::from recorded callable · signature and safety not recorded

Claim #51

<i64 as From<endian_type::LittleEndian<i64>>>::from recorded callable · signature and safety not recorded

Claim #52

<isize as From<endian_type::BigEndian<isize>>>::from recorded callable · signature and safety not recorded

Claim #63

<isize as From<endian_type::LittleEndian<isize>>>::from recorded callable · signature and safety not recorded

Claim #64

<u128 as From<endian_type::BigEndian<u128>>>::from recorded callable · signature and safety not recorded

Claim #27

<u128 as From<endian_type::LittleEndian<u128>>>::from recorded callable · signature and safety not recorded

Claim #28

<u16 as From<endian_type::BigEndian<u16>>>::from recorded callable · signature and safety not recorded

Claim #9

<u16 as From<endian_type::LittleEndian<u16>>>::from recorded callable · signature and safety not recorded

Claim #10

<u32 as From<endian_type::BigEndian<u32>>>::from recorded callable · signature and safety not recorded

Claim #15

<u32 as From<endian_type::LittleEndian<u32>>>::from recorded callable · signature and safety not recorded

Claim #16

<u64 as From<endian_type::BigEndian<u64>>>::from recorded callable · signature and safety not recorded

Claim #21

<u64 as From<endian_type::LittleEndian<u64>>>::from recorded callable · signature and safety not recorded

Claim #22

<usize as From<endian_type::BigEndian<usize>>>::from recorded callable · signature and safety not recorded

Claim #33

<usize as From<endian_type::LittleEndian<usize>>>::from recorded callable · signature and safety not recorded

Claim #34

Evidence

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

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/nyuichi/rust-crate-proofs report-26-source-1
git -C report-26-source-1 checkout --detach e030b7f56f12a473c15376f01bb53e7920892b20
git -C report-26-source-1 submodule update --init --recursive --checkout
cd report-26-source-1/endian-type/0.2.0/aeneas/2026-11-05/proofs

lake build +FromProofs +Proofs

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Checks out the recorded source commit from GitHub. Install the report’s tool version before running.

Source on GitHub · SARIF with logs (.json)

Recorded run

Completed · 66 checks passed · 0 failed

2026-11-05T03:54:10.594723389+00:00 · 120.3 seconds · Exit code 0

Recorded on the author’s machine.

Check	Result	Claim
Lean checked theorem Proofs.bigendian_bitand_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.bigendian_bitand_spec`	Passed	Claim #1
Lean checked theorem Proofs.bigendian_bitor_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.bigendian_bitor_spec`	Passed	Claim #2
Lean checked theorem Proofs.bigendian_bitxor_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.bigendian_bitxor_spec`	Passed	Claim #3
Lean checked theorem Proofs.littleendian_bitand_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.littleendian_bitand_spec`	Passed	Claim #4
Lean checked theorem Proofs.littleendian_bitor_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.littleendian_bitor_spec`	Passed	Claim #5
Lean checked theorem Proofs.littleendian_bitxor_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.littleendian_bitxor_spec`	Passed	Claim #6
Lean checked theorem FromProofs.be_from_u16_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_from_u16_spec`	Passed	Claim #7
Lean checked theorem FromProofs.le_from_u16_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_from_u16_spec`	Passed	Claim #8
Lean checked theorem FromProofs.be_into_u16_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_into_u16_spec`	Passed	Claim #9
Lean checked theorem FromProofs.le_into_u16_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_into_u16_spec`	Passed	Claim #10
Lean checked theorem FromProofs.le_to_be_u16_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_to_be_u16_spec`	Passed	Claim #11
Lean checked theorem FromProofs.be_to_le_u16_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_to_le_u16_spec`	Passed	Claim #12
Lean checked theorem FromProofs.be_from_u32_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_from_u32_spec`	Passed	Claim #13
Lean checked theorem FromProofs.le_from_u32_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_from_u32_spec`	Passed	Claim #14
Lean checked theorem FromProofs.be_into_u32_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_into_u32_spec`	Passed	Claim #15
Lean checked theorem FromProofs.le_into_u32_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_into_u32_spec`	Passed	Claim #16
Lean checked theorem FromProofs.le_to_be_u32_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_to_be_u32_spec`	Passed	Claim #17
Lean checked theorem FromProofs.be_to_le_u32_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_to_le_u32_spec`	Passed	Claim #18
Lean checked theorem FromProofs.be_from_u64_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_from_u64_spec`	Passed	Claim #19
Lean checked theorem FromProofs.le_from_u64_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_from_u64_spec`	Passed	Claim #20
Lean checked theorem FromProofs.be_into_u64_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_into_u64_spec`	Passed	Claim #21
Lean checked theorem FromProofs.le_into_u64_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_into_u64_spec`	Passed	Claim #22
Lean checked theorem FromProofs.le_to_be_u64_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_to_be_u64_spec`	Passed	Claim #23
Lean checked theorem FromProofs.be_to_le_u64_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_to_le_u64_spec`	Passed	Claim #24
Lean checked theorem FromProofs.be_from_u128_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_from_u128_spec`	Passed	Claim #25
Lean checked theorem FromProofs.le_from_u128_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_from_u128_spec`	Passed	Claim #26
Lean checked theorem FromProofs.be_into_u128_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_into_u128_spec`	Passed	Claim #27
Lean checked theorem FromProofs.le_into_u128_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_into_u128_spec`	Passed	Claim #28
Lean checked theorem FromProofs.le_to_be_u128_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_to_be_u128_spec`	Passed	Claim #29
Lean checked theorem FromProofs.be_to_le_u128_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_to_le_u128_spec`	Passed	Claim #30
Lean checked theorem FromProofs.be_from_usize_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_from_usize_spec`	Passed	Claim #31
Lean checked theorem FromProofs.le_from_usize_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_from_usize_spec`	Passed	Claim #32
Lean checked theorem FromProofs.be_into_usize_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_into_usize_spec`	Passed	Claim #33
Lean checked theorem FromProofs.le_into_usize_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_into_usize_spec`	Passed	Claim #34
Lean checked theorem FromProofs.le_to_be_usize_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_to_be_usize_spec`	Passed	Claim #35
Lean checked theorem FromProofs.be_to_le_usize_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_to_le_usize_spec`	Passed	Claim #36
Lean checked theorem FromProofs.be_from_i16_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_from_i16_spec`	Passed	Claim #37
Lean checked theorem FromProofs.le_from_i16_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_from_i16_spec`	Passed	Claim #38
Lean checked theorem FromProofs.be_into_i16_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_into_i16_spec`	Passed	Claim #39
Lean checked theorem FromProofs.le_into_i16_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_into_i16_spec`	Passed	Claim #40
Lean checked theorem FromProofs.le_to_be_i16_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_to_be_i16_spec`	Passed	Claim #41
Lean checked theorem FromProofs.be_to_le_i16_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_to_le_i16_spec`	Passed	Claim #42
Lean checked theorem FromProofs.be_from_i32_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_from_i32_spec`	Passed	Claim #43
Lean checked theorem FromProofs.le_from_i32_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_from_i32_spec`	Passed	Claim #44
Lean checked theorem FromProofs.be_into_i32_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_into_i32_spec`	Passed	Claim #45
Lean checked theorem FromProofs.le_into_i32_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_into_i32_spec`	Passed	Claim #46
Lean checked theorem FromProofs.le_to_be_i32_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_to_be_i32_spec`	Passed	Claim #47
Lean checked theorem FromProofs.be_to_le_i32_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_to_le_i32_spec`	Passed	Claim #48
Lean checked theorem FromProofs.be_from_i64_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_from_i64_spec`	Passed	Claim #49
Lean checked theorem FromProofs.le_from_i64_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_from_i64_spec`	Passed	Claim #50
Lean checked theorem FromProofs.be_into_i64_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_into_i64_spec`	Passed	Claim #51
Lean checked theorem FromProofs.le_into_i64_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_into_i64_spec`	Passed	Claim #52
Lean checked theorem FromProofs.le_to_be_i64_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_to_be_i64_spec`	Passed	Claim #53
Lean checked theorem FromProofs.be_to_le_i64_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_to_le_i64_spec`	Passed	Claim #54
Lean checked theorem FromProofs.be_from_i128_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_from_i128_spec`	Passed	Claim #55
Lean checked theorem FromProofs.le_from_i128_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_from_i128_spec`	Passed	Claim #56
Lean checked theorem FromProofs.be_into_i128_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_into_i128_spec`	Passed	Claim #57
Lean checked theorem FromProofs.le_into_i128_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_into_i128_spec`	Passed	Claim #58
Lean checked theorem FromProofs.le_to_be_i128_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_to_be_i128_spec`	Passed	Claim #59
Lean checked theorem FromProofs.be_to_le_i128_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_to_le_i128_spec`	Passed	Claim #60
Lean checked theorem FromProofs.be_from_isize_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_from_isize_spec`	Passed	Claim #61
Lean checked theorem FromProofs.le_from_isize_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_from_isize_spec`	Passed	Claim #62
Lean checked theorem FromProofs.be_into_isize_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_into_isize_spec`	Passed	Claim #63
Lean checked theorem FromProofs.le_into_isize_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_into_isize_spec`	Passed	Claim #64
Lean checked theorem FromProofs.le_to_be_isize_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.le_to_be_isize_spec`	Passed	Claim #65
Lean checked theorem FromProofs.be_to_le_isize_spec; axioms limited to propext, Classical.choice, Quot.sound `FromProofs.be_to_le_isize_spec`	Passed	Claim #66

Execution details

Started: 2026-11-05T03:54:10.594723389+00:00
Finished: 2026-11-05T03:56:10.920008958+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: endian-type/0.2.0/aeneas/2026-11-05/proofs
Environment overrides: None recorded
Git repository: https://github.com/nyuichi/rust-crate-proofs
Git commit: e030b7f56f12a473c15376f01bb53e7920892b20

Diagnostics & logs

=== stdout ===
✔ [1796/1802] Built EndianVerificationDriver.Types (1.5s)
✔ [1797/1802] Built Generated.EndianType (1.6s)
✔ [1798/1802] Built EndianVerificationDriver.FunsExternal (2.5s)
✔ [1799/1802] Built EndianVerificationDriver.Funs (6.5s)
ℹ [1800/1802] Built ModelProofs (7.3s)
info: ModelProofs.lean:278:0: 'ModelProofs.u16_swap_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:279:0: 'ModelProofs.u16_to_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:280:0: 'ModelProofs.u16_from_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:281:0: 'ModelProofs.u16_to_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:282:0: 'ModelProofs.u16_from_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:283:0: 'ModelProofs.u32_swap_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:284:0: 'ModelProofs.u32_to_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:285:0: 'ModelProofs.u32_from_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:286:0: 'ModelProofs.u32_to_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:287:0: 'ModelProofs.u32_from_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:288:0: 'ModelProofs.u64_swap_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:289:0: 'ModelProofs.u64_to_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:290:0: 'ModelProofs.u64_from_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:291:0: 'ModelProofs.u64_to_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:292:0: 'ModelProofs.u64_from_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:293:0: 'ModelProofs.u128_swap_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:294:0: 'ModelProofs.u128_to_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:295:0: 'ModelProofs.u128_from_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:296:0: 'ModelProofs.u128_to_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:297:0: 'ModelProofs.u128_from_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:298:0: 'ModelProofs.i16_swap_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:299:0: 'ModelProofs.i16_to_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:300:0: 'ModelProofs.i16_from_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:301:0: 'ModelProofs.i16_to_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:302:0: 'ModelProofs.i16_from_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:303:0: 'ModelProofs.i32_swap_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:304:0: 'ModelProofs.i32_to_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:305:0: 'ModelProofs.i32_from_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:306:0: 'ModelProofs.i32_to_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:307:0: 'ModelProofs.i32_from_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:308:0: 'ModelProofs.i64_swap_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:309:0: 'ModelProofs.i64_to_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:310:0: 'ModelProofs.i64_from_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:311:0: 'ModelProofs.i64_to_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:312:0: 'ModelProofs.i64_from_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:313:0: 'ModelProofs.i128_swap_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:314:0: 'ModelProofs.i128_to_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:315:0: 'ModelProofs.i128_from_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:316:0: 'ModelProofs.i128_to_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:317:0: 'ModelProofs.i128_from_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:318:0: 'ModelProofs.usize_swap_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:319:0: 'ModelProofs.usize_to_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:320:0: 'ModelProofs.usize_from_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:321:0: 'ModelProofs.usize_to_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:322:0: 'ModelProofs.usize_from_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:323:0: 'ModelProofs.isize_swap_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:324:0: 'ModelProofs.isize_to_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:325:0: 'ModelProofs.isize_from_be_model' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ModelProofs.lean:326:0: 'ModelProofs.isize_to_le_model' depends on axioms: [propext, Quot.sound]
info: ModelProofs.lean:327:0: 'ModelProofs.isize_from_le_model' depends on axioms: [propext, Quot.sound]
⚠ [1801/1802] Built FromProofs (6.3s)
warning: FromProofs.lean:18:105: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.U16.Insts.CoreConvertFromBigEndianU16.from, u16_from_be_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:23:108: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.U16.Insts.CoreConvertFromLittleEndianU16.from, u16_from_le_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:48:105: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.U32.Insts.CoreConvertFromBigEndianU32.from, u32_from_be_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:53:108: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.U32.Insts.CoreConvertFromLittleEndianU32.from, u32_from_le_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:78:105: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.U64.Insts.CoreConvertFromBigEndianU64.from, u64_from_be_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:83:108: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.U64.Insts.CoreConvertFromLittleEndianU64.from, u64_from_le_model x]

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

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.U128.Insts.CoreConvertFromBigEndianU128.from, u128_from_be_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:113:111: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.U128.Insts.CoreConvertFromLittleEndianU128.from, u128_from_le_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:131:40: Variable name `h64` 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] _h64

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: FromProofs.lean:138:115: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.Usize.Insts.CoreConvertFromBigEndianUsize.from,
    usize_from_be_model x h64]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:141:40: Variable name `h64` 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] _h64

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: FromProofs.lean:143:114: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.Usize.Insts.CoreConvertFromLittleEndianUsize.from,
    usize_from_le_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:168:105: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.I16.Insts.CoreConvertFromBigEndianI16.from, i16_from_be_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:173:108: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.I16.Insts.CoreConvertFromLittleEndianI16.from, i16_from_le_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:198:105: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.I32.Insts.CoreConvertFromBigEndianI32.from, i32_from_be_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:203:108: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.I32.Insts.CoreConvertFromLittleEndianI32.from, i32_from_le_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:228:105: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.I64.Insts.CoreConvertFromBigEndianI64.from, i64_from_be_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:233:108: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.I64.Insts.CoreConvertFromLittleEndianI64.from, i64_from_le_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:258:108: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.I128.Insts.CoreConvertFromBigEndianI128.from, i128_from_be_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:263:111: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.I128.Insts.CoreConvertFromLittleEndianI128.from, i128_from_le_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:281:40: Variable name `h64` 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] _h64

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: FromProofs.lean:288:115: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.Isize.Insts.CoreConvertFromBigEndianIsize.from,
    isize_from_be_model x h64]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: FromProofs.lean:291:40: Variable name `h64` 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] _h64

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: FromProofs.lean:293:114: This simp argument is unused:
  bind_ok

Hint: Omit it from the simp argument list.
  [apply] simp only [endian_verification_driver.Isize.Insts.CoreConvertFromLittleEndianIsize.from,
    isize_from_le_model x]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: FromProofs.lean:306:0: 'FromProofs.be_from_u16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:307:0: 'FromProofs.le_from_u16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:308:0: 'FromProofs.be_into_u16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:309:0: 'FromProofs.le_into_u16_spec' depends on axioms: [propext, Quot.sound]
info: FromProofs.lean:310:0: 'FromProofs.le_to_be_u16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:311:0: 'FromProofs.be_to_le_u16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:312:0: 'FromProofs.be_from_u32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:313:0: 'FromProofs.le_from_u32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:314:0: 'FromProofs.be_into_u32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:315:0: 'FromProofs.le_into_u32_spec' depends on axioms: [propext, Quot.sound]
info: FromProofs.lean:316:0: 'FromProofs.le_to_be_u32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:317:0: 'FromProofs.be_to_le_u32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:318:0: 'FromProofs.be_from_u64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:319:0: 'FromProofs.le_from_u64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:320:0: 'FromProofs.be_into_u64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:321:0: 'FromProofs.le_into_u64_spec' depends on axioms: [propext, Quot.sound]
info: FromProofs.lean:322:0: 'FromProofs.le_to_be_u64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:323:0: 'FromProofs.be_to_le_u64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:324:0: 'FromProofs.be_from_u128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:325:0: 'FromProofs.le_from_u128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:326:0: 'FromProofs.be_into_u128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:327:0: 'FromProofs.le_into_u128_spec' depends on axioms: [propext, Quot.sound]
info: FromProofs.lean:328:0: 'FromProofs.le_to_be_u128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:329:0: 'FromProofs.be_to_le_u128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:330:0: 'FromProofs.be_from_usize_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:331:0: 'FromProofs.le_from_usize_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:332:0: 'FromProofs.be_into_usize_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:333:0: 'FromProofs.le_into_usize_spec' depends on axioms: [propext, Quot.sound]
info: FromProofs.lean:334:0: 'FromProofs.le_to_be_usize_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:335:0: 'FromProofs.be_to_le_usize_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:336:0: 'FromProofs.be_from_i16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:337:0: 'FromProofs.le_from_i16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:338:0: 'FromProofs.be_into_i16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:339:0: 'FromProofs.le_into_i16_spec' depends on axioms: [propext, Quot.sound]
info: FromProofs.lean:340:0: 'FromProofs.le_to_be_i16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:341:0: 'FromProofs.be_to_le_i16_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:342:0: 'FromProofs.be_from_i32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:343:0: 'FromProofs.le_from_i32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:344:0: 'FromProofs.be_into_i32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:345:0: 'FromProofs.le_into_i32_spec' depends on axioms: [propext, Quot.sound]
info: FromProofs.lean:346:0: 'FromProofs.le_to_be_i32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:347:0: 'FromProofs.be_to_le_i32_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:348:0: 'FromProofs.be_from_i64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:349:0: 'FromProofs.le_from_i64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:350:0: 'FromProofs.be_into_i64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:351:0: 'FromProofs.le_into_i64_spec' depends on axioms: [propext, Quot.sound]
info: FromProofs.lean:352:0: 'FromProofs.le_to_be_i64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:353:0: 'FromProofs.be_to_le_i64_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:354:0: 'FromProofs.be_from_i128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:355:0: 'FromProofs.le_from_i128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:356:0: 'FromProofs.be_into_i128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:357:0: 'FromProofs.le_into_i128_spec' depends on axioms: [propext, Quot.sound]
info: FromProofs.lean:358:0: 'FromProofs.le_to_be_i128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:359:0: 'FromProofs.be_to_le_i128_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:360:0: 'FromProofs.be_from_isize_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:361:0: 'FromProofs.le_from_isize_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:362:0: 'FromProofs.be_into_isize_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:363:0: 'FromProofs.le_into_isize_spec' depends on axioms: [propext, Quot.sound]
info: FromProofs.lean:364:0: 'FromProofs.le_to_be_isize_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FromProofs.lean:365:0: 'FromProofs.be_to_le_isize_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1802/1802] Built Proofs (2.5s)
info: Proofs.lean:25:0: 'Proofs.bigendian_bitand_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:26:0: 'Proofs.bigendian_bitor_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:27:0: 'Proofs.bigendian_bitxor_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:28:0: 'Proofs.littleendian_bitand_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:29:0: 'Proofs.littleendian_bitor_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:30:0: 'Proofs.littleendian_bitxor_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
Build completed successfully (1802 jobs).

$ lake env lean --stdin (proofs.rs theorem/axiom audit)
proofs.rs:checked:Proofs.bigendian_bitand_spec
proofs.rs:checked:Proofs.bigendian_bitor_spec
proofs.rs:checked:Proofs.bigendian_bitxor_spec
proofs.rs:checked:Proofs.littleendian_bitand_spec
proofs.rs:checked:Proofs.littleendian_bitor_spec
proofs.rs:checked:Proofs.littleendian_bitxor_spec
proofs.rs:checked:FromProofs.be_from_u16_spec
proofs.rs:checked:FromProofs.le_from_u16_spec
proofs.rs:checked:FromProofs.be_into_u16_spec
proofs.rs:checked:FromProofs.le_into_u16_spec
proofs.rs:checked:FromProofs.le_to_be_u16_spec
proofs.rs:checked:FromProofs.be_to_le_u16_spec
proofs.rs:checked:FromProofs.be_from_u32_spec
proofs.rs:checked:FromProofs.le_from_u32_spec
proofs.rs:checked:FromProofs.be_into_u32_spec
proofs.rs:checked:FromProofs.le_into_u32_spec
proofs.rs:checked:FromProofs.le_to_be_u32_spec
proofs.rs:checked:FromProofs.be_to_le_u32_spec
proofs.rs:checked:FromProofs.be_from_u64_spec
proofs.rs:checked:FromProofs.le_from_u64_spec
proofs.rs:checked:FromProofs.be_into_u64_spec
proofs.rs:checked:FromProofs.le_into_u64_spec
proofs.rs:checked:FromProofs.le_to_be_u64_spec
proofs.rs:checked:FromProofs.be_to_le_u64_spec
proofs.rs:checked:FromProofs.be_from_u128_spec
proofs.rs:checked:FromProofs.le_from_u128_spec
proofs.rs:checked:FromProofs.be_into_u128_spec
proofs.rs:checked:FromProofs.le_into_u128_spec
proofs.rs:checked:FromProofs.le_to_be_u128_spec
proofs.rs:checked:FromProofs.be_to_le_u128_spec
proofs.rs:checked:FromProofs.be_from_usize_spec
proofs.rs:checked:FromProofs.le_from_usize_spec
proofs.rs:checked:FromProofs.be_into_usize_spec
proofs.rs:checked:FromProofs.le_into_usize_spec
proofs.rs:checked:FromProofs.le_to_be_usize_spec
proofs.rs:checked:FromProofs.be_to_le_usize_spec
proofs.rs:checked:FromProofs.be_from_i16_spec
proofs.rs:checked:FromProofs.le_from_i16_spec
proofs.rs:checked:FromProofs.be_into_i16_spec
proofs.rs:checked:FromProofs.le_into_i16_spec
proofs.rs:checked:FromProofs.le_to_be_i16_spec
proofs.rs:checked:FromProofs.be_to_le_i16_spec
proofs.rs:checked:FromProofs.be_from_i32_spec
proofs.rs:checked:FromProofs.le_from_i32_spec
proofs.rs:checked:FromProofs.be_into_i32_spec
proofs.rs:checked:FromProofs.le_into_i32_spec
proofs.rs:checked:FromProofs.le_to_be_i32_spec
proofs.rs:checked:FromProofs.be_to_le_i32_spec
proofs.rs:checked:FromProofs.be_from_i64_spec
proofs.rs:checked:FromProofs.le_from_i64_spec
proofs.rs:checked:FromProofs.be_into_i64_spec
proofs.rs:checked:FromProofs.le_into_i64_spec
proofs.rs:checked:FromProofs.le_to_be_i64_spec
proofs.rs:checked:FromProofs.be_to_le_i64_spec
proofs.rs:checked:FromProofs.be_from_i128_spec
proofs.rs:checked:FromProofs.le_from_i128_spec
proofs.rs:checked:FromProofs.be_into_i128_spec
proofs.rs:checked:FromProofs.le_into_i128_spec
proofs.rs:checked:FromProofs.le_to_be_i128_spec
proofs.rs:checked:FromProofs.be_to_le_i128_spec
proofs.rs:checked:FromProofs.be_from_isize_spec
proofs.rs:checked:FromProofs.le_from_isize_spec
proofs.rs:checked:FromProofs.be_into_isize_spec
proofs.rs:checked:FromProofs.le_into_isize_spec
proofs.rs:checked:FromProofs.le_to_be_isize_spec
proofs.rs:checked:FromProofs.be_to_le_isize_spec

=== stderr ===
info: aeneas: materializing new dependency
info: aeneas: fetching revision 'be86ab0f1989d04944292b345b24c435be3ad10a' from https://github.com/AeneasVerif/aeneas
info: aeneas: checking out revision 'be86ab0f1989d04944292b345b24c435be3ad10a'
info: mathlib: materializing new dependency
info: mathlib: fetching revision '56a005855ea17e0b0958f73ec801ae140b0a1679' from https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '56a005855ea17e0b0958f73ec801ae140b0a1679'
info: plausible: materializing new dependency
info: plausible: fetching revision 'dfa4f38190d07c37e315953e08b90fe2d95b3c24' from https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'dfa4f38190d07c37e315953e08b90fe2d95b3c24'
info: LeanSearchClient: materializing new dependency
info: LeanSearchClient: fetching revision 'd6b4c7be5be75ec4917c873ac50c756dc1436372' from https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'd6b4c7be5be75ec4917c873ac50c756dc1436372'
info: importGraph: materializing new dependency
info: importGraph: fetching revision 'a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93' from https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93'
info: proofwidgets: materializing new dependency
info: proofwidgets: fetching revision 'df72b022e558978a1c50264cfc4d7fec86fa8e04' from https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'df72b022e558978a1c50264cfc4d7fec86fa8e04'
info: aesop: materializing new dependency
info: aesop: fetching revision '4a174c490d8707121c4a9290800489f105d85e07' from https://github.com/leanprover-community/aesop
info: aesop: checking out revision '4a174c490d8707121c4a9290800489f105d85e07'
info: Qq: materializing new dependency
info: Qq: fetching revision 'dce0ad79c486cb1fb504af04f953c3466b0c6db8' from https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'dce0ad79c486cb1fb504af04f953c3466b0c6db8'
info: batteries: materializing new dependency
info: batteries: fetching revision '66e469188fe07963e5cf666c7d4433f45b8131c5' from https://github.com/leanprover-community/batteries
info: batteries: checking out revision '66e469188fe07963e5cf666c7d4433f45b8131c5'
info: Cli: materializing new dependency
info: Cli: fetching revision 'c24fe6078c630e89b489bffe59b3e20ac30d12c8' from https://github.com/leanprover/lean4-cli
info: Cli: checking out revision 'c24fe6078c630e89b489bffe59b3e20ac30d12c8'

Environment

Original crates.io endian-type 0.2.0; x86_64-unknown-linux-gnu little-endian. Rust nightly-2026-09-17; Charon 08d7c9d50144bd84848212c24701253585e90d1f; Aeneas/official library be86ab0f1989d04944292b345b24c435be3ad10a; Lean 4.35.0. Official method roots verify the six generic methods. A pure caller driver with --include endian_type extracts all sixty actual dependency bodies. Official compiler source-path remapping supports reproducible spans. Exact model/function/type/use guards and transitive axiom audits are retained. Kani 0.68.0/CBMC 6.11.0/Rust nightly-2026-08-21: ten symbolic std-model harnesses, 216 checks, zero failures.

What is trusted

The Rust compiler, Charon/Aeneas, official scalar/byte primitives, Lean kernel, Kani and CBMC are trusted. Fifty native-endian std-operation models are explicitly supplied. Their Rust byte formulas and official Lean byte primitives are connected by review, not a mechanically checked cross-language theorem; std operator bodies are not independently proved in Lean. Kani and extraction use different Rust nightlies. The six bitwise results quantify arbitrary underlying operator dictionaries without proving user callback bodies. All 66 API contracts and 50 model specifications use only propext, Classical.choice and Quot.sound as transitive axioms.

Technical limitations

Coverage is limited to six bitwise methods and sixty concrete integer From implementations on the stated target/model domain. The forty-six byte/slice APIs and their unsafe layout/validity/aliasing obligations are not covered by these Aeneas claims. No generic arbitrary-T memory-safety, other target, endian, or pointer-width claim is established. Derived standard-trait methods are excluded. Remaining trait/default/blanket behavior is not verified. Type-specialized Rust identities and any erased server catalogue keys must be distinguished.

Tool limitations

Lean backend only, requiring cargo-proofs 0.4.0 or later. The version identifies the official Aeneas Git revision pinned in lake-manifest.json (backends/lean); this revision uses Lean 4.35.0. The recorder checks committed Lean theorem declarations and permits only propext, Classical.choice, and Quot.sound as transitive axioms. It rejects sorryAx and custom axioms, including axiomatized external models. Charon/Aeneas extraction is not rerun. The author must review that the committed functional model matches the recorded Rust source, that the named theorem corresponds to the public API, and that the reported precondition matches the theorem. A checked theorem alone does not establish those links or the adequacy of the specification. The current adapter records the default Cargo configuration, with ordinary Lean module paths and a pinned official Git dependency. Other backends, custom Lake source directories, and local-path Aeneas dependencies are unsupported. See https://proofs.rs/book/aeneas.html and https://github.com/AeneasVerif/aeneas/tree/be86ab0f1989d04944292b345b24c435be3ad10a.

Updated 2026-10-16 00:00 UTC

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a — version details

Dependencies (0)

No direct dependencies.

Comments (0)

No comments.