Report #34 — Integer single-bit operations and generic slice routing, with exact failure cases

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

27 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:12 UTC

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

Overview

The unchanged bit_field 0.10.3 single-bit methods are verified for all twelve integer types: in-range indices read or update exactly that bit, returned mutable-reference writes propagate to the original value, and invalid indices fail at the assertion. All twelve primitive BIT_LENGTH values equal their widths. The original generic slice bit_length/get_bit/set_bit bodies are also composition-proved: assuming their declared BitField constant and per-element normal-return contracts, they use element index bit/width and local index bit%width, preserve other slice entries on update, and report zero-width/out-of-bounds errors. bit_length returns length times width or integerOverflow. Rust source and Cargo.toml are archive-identical. Separately, original-Rust Kani checks cover RangeFull specializations of get_bits and set_bits for each of the twelve primitive integer types. For every scalar value, get_bits(..) returns that exact word without changing it. For every receiver and replacement, set_bits(.., replacement) replaces the complete word, returns the mutable reference containing the replacement, and a subsequent arbitrary write through it updates the original word. Signed negative values and sign bits are included. These are twenty-four closed specializations with1284 successful checks, not completion of the generic RangeBounds method families or additional machine mappings.

Findings (0)

No findings reported.

APIs (27)

Recorded callables

<[T] as bit_field::BitArray<T>>::bit_length recorded callable · signature and safety not recorded

Claim #25

<[T] as bit_field::BitArray<T>>::get_bit recorded callable · signature and safety not recorded

Claim #26

<[T] as bit_field::BitArray<T>>::set_bit recorded callable · signature and safety not recorded

Claim #27

<i128 as bit_field::BitField>::get_bit recorded callable · signature and safety not recorded

Claim #21

<i128 as bit_field::BitField>::set_bit recorded callable · signature and safety not recorded

Claim #22

<i16 as bit_field::BitField>::get_bit recorded callable · signature and safety not recorded

Claim #15

<i16 as bit_field::BitField>::set_bit recorded callable · signature and safety not recorded

Claim #16

<i32 as bit_field::BitField>::get_bit recorded callable · signature and safety not recorded

Claim #17

<i32 as bit_field::BitField>::set_bit recorded callable · signature and safety not recorded

Claim #18

<i64 as bit_field::BitField>::get_bit recorded callable · signature and safety not recorded

Claim #19

<i64 as bit_field::BitField>::set_bit recorded callable · signature and safety not recorded

Claim #20

<i8 as bit_field::BitField>::get_bit recorded callable · signature and safety not recorded

Claim #13

<i8 as bit_field::BitField>::set_bit recorded callable · signature and safety not recorded

Claim #14

<isize as bit_field::BitField>::get_bit recorded callable · signature and safety not recorded

Claim #23

<isize as bit_field::BitField>::set_bit recorded callable · signature and safety not recorded

Claim #24

<u128 as bit_field::BitField>::get_bit recorded callable · signature and safety not recorded

Claim #9

<u128 as bit_field::BitField>::set_bit recorded callable · signature and safety not recorded

Claim #10

<u16 as bit_field::BitField>::get_bit recorded callable · signature and safety not recorded

Claim #3

<u16 as bit_field::BitField>::set_bit recorded callable · signature and safety not recorded

Claim #4

<u32 as bit_field::BitField>::get_bit recorded callable · signature and safety not recorded

Claim #5

<u32 as bit_field::BitField>::set_bit recorded callable · signature and safety not recorded

Claim #6

<u64 as bit_field::BitField>::get_bit recorded callable · signature and safety not recorded

Claim #7

<u64 as bit_field::BitField>::set_bit recorded callable · signature and safety not recorded

Claim #8

<u8 as bit_field::BitField>::get_bit recorded callable · signature and safety not recorded

Claim #1

<u8 as bit_field::BitField>::set_bit recorded callable · signature and safety not recorded

Claim #2

<usize as bit_field::BitField>::get_bit recorded callable · signature and safety not recorded

Claim #11

<usize as bit_field::BitField>::set_bit recorded callable · signature and safety not recorded

Claim #12

Evidence

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

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/nyuichi/rust-crate-proofs report-34-source-1
git -C report-34-source-1 checkout --detach d5937b4cd322bfbb83c581eba1ad17b5fad851fe
git -C report-34-source-1 submodule update --init --recursive --checkout
cd report-34-source-1/bit_field/0.10.3/aeneas/2026-11-05/proofs

lake build +ArrayBitsProofs +ArrayProofs +Proofs

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2026-11-05T17:33:19.598272215+00:00 · 100.7 seconds · Exit code 0

Recorded on the author’s machine.

Check	Result	Claim
Lean checked theorem Proofs.u8_get_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.u8_get_bit_contract`	Passed	Claim #1
Lean checked theorem Proofs.u8_set_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.u8_set_bit_contract`	Passed	Claim #2
Lean checked theorem Proofs.u16_get_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.u16_get_bit_contract`	Passed	Claim #3
Lean checked theorem Proofs.u16_set_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.u16_set_bit_contract`	Passed	Claim #4
Lean checked theorem Proofs.u32_get_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.u32_get_bit_contract`	Passed	Claim #5
Lean checked theorem Proofs.u32_set_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.u32_set_bit_contract`	Passed	Claim #6
Lean checked theorem Proofs.u64_get_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.u64_get_bit_contract`	Passed	Claim #7
Lean checked theorem Proofs.u64_set_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.u64_set_bit_contract`	Passed	Claim #8
Lean checked theorem Proofs.u128_get_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.u128_get_bit_contract`	Passed	Claim #9
Lean checked theorem Proofs.u128_set_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.u128_set_bit_contract`	Passed	Claim #10
Lean checked theorem Proofs.usize_get_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.usize_get_bit_contract`	Passed	Claim #11
Lean checked theorem Proofs.usize_set_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.usize_set_bit_contract`	Passed	Claim #12
Lean checked theorem Proofs.i8_get_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.i8_get_bit_contract`	Passed	Claim #13
Lean checked theorem Proofs.i8_set_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.i8_set_bit_contract`	Passed	Claim #14
Lean checked theorem Proofs.i16_get_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.i16_get_bit_contract`	Passed	Claim #15
Lean checked theorem Proofs.i16_set_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.i16_set_bit_contract`	Passed	Claim #16
Lean checked theorem Proofs.i32_get_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.i32_get_bit_contract`	Passed	Claim #17
Lean checked theorem Proofs.i32_set_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.i32_set_bit_contract`	Passed	Claim #18
Lean checked theorem Proofs.i64_get_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.i64_get_bit_contract`	Passed	Claim #19
Lean checked theorem Proofs.i64_set_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.i64_set_bit_contract`	Passed	Claim #20
Lean checked theorem Proofs.i128_get_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.i128_get_bit_contract`	Passed	Claim #21
Lean checked theorem Proofs.i128_set_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.i128_set_bit_contract`	Passed	Claim #22
Lean checked theorem Proofs.isize_get_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.isize_get_bit_contract`	Passed	Claim #23
Lean checked theorem Proofs.isize_set_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `Proofs.isize_set_bit_contract`	Passed	Claim #24
Lean checked theorem ArrayProofs.bit_length_contract; axioms limited to propext, Classical.choice, Quot.sound `ArrayProofs.bit_length_contract`	Passed	Claim #25
Lean checked theorem ArrayBitsProofs.get_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `ArrayBitsProofs.get_bit_contract`	Passed	Claim #26
Lean checked theorem ArrayBitsProofs.set_bit_contract; axioms limited to propext, Classical.choice, Quot.sound `ArrayBitsProofs.set_bit_contract`	Passed	Claim #27

Execution details

Started: 2026-11-05T17:33:19.598272215+00:00
Finished: 2026-11-05T17:35:00.314202743+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: bit_field/0.10.3/aeneas/2026-11-05/proofs
Environment overrides: None recorded
Git repository: https://github.com/nyuichi/rust-crate-proofs
Git commit: d5937b4cd322bfbb83c581eba1ad17b5fad851fe

Diagnostics & logs

=== stdout ===
✔ [1796/1802] Built BitField.Types (1.7s)
✔ [1797/1802] Built BitArrayGenerated.BitField (1.9s)
✔ [1798/1802] Built BitField.FunsExternal (2.2s)
⚠ [1799/1802] Built ArrayProofs (2.7s)
info: ArrayProofs.lean:15:0: 'ArrayProofs.bit_length_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: ArrayProofs.lean:23:26: This simp argument is unused:
  bind_tc_ok

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ArrayProofs.lean:30:64: This simp argument is unused:
  ↓reduceDIte

Hint: Omit it from the simp argument list.
  [apply] simp only [UScalar.mul, UScalar.tryMk, UScalar.tryMkOpt, bad, ofOption]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: ArrayProofs.lean:38:0: 'ArrayProofs.bit_length_overflow' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ArrayProofs.lean:39:0: 'ArrayProofs.bit_length_callback_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ArrayProofs.lean:51:0: 'ArrayProofs.bit_length_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1800/1802] Built ArrayBitsProofs (3.3s)
info: ArrayBitsProofs.lean:20:0: 'ArrayBitsProofs.get_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ArrayBitsProofs.lean:39:0: 'ArrayBitsProofs.set_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ArrayBitsProofs.lean:63:0: 'ArrayBitsProofs.get_bit_zero_width' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ArrayBitsProofs.lean:64:0: 'ArrayBitsProofs.set_bit_zero_width' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ArrayBitsProofs.lean:110:0: 'ArrayBitsProofs.get_bit_outside' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ArrayBitsProofs.lean:111:0: 'ArrayBitsProofs.set_bit_outside' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ArrayBitsProofs.lean:161:0: 'ArrayBitsProofs.get_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ArrayBitsProofs.lean:162:0: 'ArrayBitsProofs.set_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [1801/1802] Built BitField.Funs (2.4s)
ℹ [1802/1802] Built Proofs (5.2s)
info: Proofs.lean:653:0: 'Proofs.u8_get_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:654:0: 'Proofs.u8_set_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:655:0: 'Proofs.u16_get_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:656:0: 'Proofs.u16_set_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:657:0: 'Proofs.u32_get_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:658:0: 'Proofs.u32_set_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:659:0: 'Proofs.u64_get_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:660:0: 'Proofs.u64_set_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:661:0: 'Proofs.u128_get_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:662:0: 'Proofs.u128_set_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:663:0: 'Proofs.usize_get_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:664:0: 'Proofs.usize_set_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:665:0: 'Proofs.i8_get_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:666:0: 'Proofs.i8_set_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:667:0: 'Proofs.i16_get_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:668:0: 'Proofs.i16_set_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:669:0: 'Proofs.i32_get_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:670:0: 'Proofs.i32_set_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:671:0: 'Proofs.i64_get_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:672:0: 'Proofs.i64_set_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:673:0: 'Proofs.i128_get_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:674:0: 'Proofs.i128_set_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:675:0: 'Proofs.isize_get_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:676:0: 'Proofs.isize_set_bit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:980:0: 'Proofs.u8_get_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:981:0: 'Proofs.u8_set_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:982:0: 'Proofs.u16_get_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:983:0: 'Proofs.u16_set_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:984:0: 'Proofs.u32_get_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:985:0: 'Proofs.u32_set_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:986:0: 'Proofs.u64_get_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:987:0: 'Proofs.u64_set_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:988:0: 'Proofs.u128_get_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:989:0: 'Proofs.u128_set_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:990:0: 'Proofs.usize_get_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:991:0: 'Proofs.usize_set_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:992:0: 'Proofs.i8_get_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:993:0: 'Proofs.i8_set_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:994:0: 'Proofs.i16_get_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:995:0: 'Proofs.i16_set_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:996:0: 'Proofs.i32_get_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:997:0: 'Proofs.i32_set_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:998:0: 'Proofs.i64_get_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:999:0: 'Proofs.i64_set_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:1000:0: 'Proofs.i128_get_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:1001:0: 'Proofs.i128_set_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:1002:0: 'Proofs.isize_get_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:1003:0: 'Proofs.isize_set_bit_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:1004:0: 'Proofs.u8_length_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:1005:0: 'Proofs.u16_length_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:1006:0: 'Proofs.u32_length_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:1007:0: 'Proofs.u64_length_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:1008:0: 'Proofs.u128_length_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:1009:0: 'Proofs.usize_length_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:1010:0: 'Proofs.i8_length_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:1011:0: 'Proofs.i16_length_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:1012:0: 'Proofs.i32_length_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:1013:0: 'Proofs.i64_length_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:1014:0: 'Proofs.i128_length_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:1015:0: 'Proofs.isize_length_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.u8_get_bit_contract
proofs.rs:checked:Proofs.u8_set_bit_contract
proofs.rs:checked:Proofs.u16_get_bit_contract
proofs.rs:checked:Proofs.u16_set_bit_contract
proofs.rs:checked:Proofs.u32_get_bit_contract
proofs.rs:checked:Proofs.u32_set_bit_contract
proofs.rs:checked:Proofs.u64_get_bit_contract
proofs.rs:checked:Proofs.u64_set_bit_contract
proofs.rs:checked:Proofs.u128_get_bit_contract
proofs.rs:checked:Proofs.u128_set_bit_contract
proofs.rs:checked:Proofs.usize_get_bit_contract
proofs.rs:checked:Proofs.usize_set_bit_contract
proofs.rs:checked:Proofs.i8_get_bit_contract
proofs.rs:checked:Proofs.i8_set_bit_contract
proofs.rs:checked:Proofs.i16_get_bit_contract
proofs.rs:checked:Proofs.i16_set_bit_contract
proofs.rs:checked:Proofs.i32_get_bit_contract
proofs.rs:checked:Proofs.i32_set_bit_contract
proofs.rs:checked:Proofs.i64_get_bit_contract
proofs.rs:checked:Proofs.i64_set_bit_contract
proofs.rs:checked:Proofs.i128_get_bit_contract
proofs.rs:checked:Proofs.i128_set_bit_contract
proofs.rs:checked:Proofs.isize_get_bit_contract
proofs.rs:checked:Proofs.isize_set_bit_contract
proofs.rs:checked:ArrayProofs.bit_length_contract
proofs.rs:checked:ArrayBitsProofs.get_bit_contract
proofs.rs:checked:ArrayBitsProofs.set_bit_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

Original crates.io bit_field0.10.3; x86_64 default features, debug extraction. Rust nightly-2026-09-17, Charon08d7c9d50144bd84848212c24701253585e90d1f, Aeneas be86ab0f1989d04944292b345b24c435be3ad10a, Lean4.35.0. Official non-monomorphizing Aeneas-preset extraction for primitive roots and separate generic slice roots. The prior unsupported monomorphize/preset snapshot is retained as labeled evidence; all current contracts are rechecked from the supported path. Kani0.68.0/CBMC6.11.0/Rust nightly-2026-08-21: 24 supplementary primitive harnesses/600 checks, plus the separate concrete range observation. RangeFull24 frozen source/archive/harness/rawlogs and independent review are preserved under evidence/kani-rangefull24;1284checks0failed48unreachable, twelve primitive types times get/set. This supplemental evidence adds zero registered Aeneas claims.

What is trusted

The official Rust/Charon/Aeneas translation and integer/slice models, Lean, and Kani/CBMC are trusted. The size_of model uses Lean-only PrimitiveRustLayout evidence with twelve supplied primitive instances, including pointer size8 on x86_64. The original generated Funs is unchanged: each of its twelve ground calls statically elaborates to the expected instance dictionary, checked explicitly. This added implicit evidence is not a Rust trait or an in-Lean proof of std layout. The Lean class remains extensible; coverage is the frozen twelve-call closure, not class sealing. Bool lacks an instance in the audited environment, and there is no supplied fallback for arbitrary types. Kani checks the same twelve actual layouts and all primitive single-bit/returned-reference behavior for arbitrary valid values. Connecting Kani Rust and Lean representations is a reviewed bridge, not an in-Lean std layout proof; Rust nightlies differ. Generic slice theorems assume the complete stated observation/update callback contracts, including the final state after returned-reference writeback. They do not prove arbitrary callback implementations. Mapped audits allow only propext, Classical.choice and Quot.sound. The RangeFull supplement executes original public methods and actual std size_of under Kani0.68/CBMC6.11/nightly2026-08-21, default debug x86_64 with64-bit usize/isize. Its compiler, standard and validity/panic semantics are trusted; no source adaptation, model, stub or suppressed UB check is introduced. It is independent of the Lean-only layout evidence and supplies no formal cross-tool equivalence.

Technical limitations

Only twenty-four primitive single-bit methods, twelve width constants and three callback-conditional slice bodies are established. General primitive and slice get_bits/set_bits range contracts remain unproved; the separate RangeFull-only Kani results described here cover closed primitive specializations. A separately Kani-checked example shows signed range behavior differs from ordinary masked updates: 112_i8.set_bits(0..4,1) yields 1, changing high bits outside the range; the unsigned example yields 113. The verified single-bit methods are unaffected. Generic callback side effects, failure/divergence outside the stated contracts, other targets and release extraction are not established. No generic Rust size_of property, panic text or unwinding-state guarantee is claimed. Signed-range diagnostic evidence: https://github.com/nyuichi/rust-crate-proofs/tree/57c4d16e1184f84353db90589bc3cb601f89cb85/batches/2026-11-05-full-public-api/diagnostics/bit-field-signed-range RangeFull denotes the whole primitive word and has no outside bits to preserve; these checks do not imply masked-update behavior for other signed intervals. Arbitrary RangeBounds implementations, bounds callbacks, general intervals, slice BitArray methods, invalid-range panic payload/unwind behavior, other targets or release configuration are not established. The separate signed small-range counterexample remains valid. All27 registered model contracts and their preconditions remain unchanged.

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.