Claim #40 — Verification of <ipnet::IpSubnets as Clone>::clone (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

The selected crate bodies are extracted from the unchanged ipnet 2.12.2 release source. The source inventory and before-and-after checks establish the identity of those inputs; they do not independently prove that translation preserves every Rust behavior. The results depend on Rust-to-LLBC-to-Lean translation and selected standard-library models.

For address ordering, the model compares big-endian numeric values. The pinned Rust IPv4 comparison orders its octets lexicographically; the IPv6 comparison orders eight segments, each formed from a pair of octets. On the checked little-endian target, those orders agree with the corresponding big-endian numbers. The IPv6 constructor model similarly concatenates the big-endian bytes of its eight segments, matching the reviewed source's byte conversion and layout on that target. These are source-based correspondence arguments, not Lean proofs of Rust layout or comparator semantics. The concrete Result::ok model follows the source's variant match for the selected drop-free network and error types; it does not establish behavior for arbitrary destructors. The trailing-zero models reverse fixed-width bits and count leading zeros, matching the reviewed intrinsic's low-zero count, including zero yielding the bit width. These correspondences remain trusted even though the resulting model properties are kernel checked.

The independently pinned Aeneas patch supplies those narrow models and checked shift wrappers; the Charon patch lowers recorded true MIR undefined-behavior checks and represents divergent panic paths using the existing panic model, and selects the IPv6 constructor. This does not establish general abort or unwind equivalence. Checked shift-overflow examples, pinned standard-library source hashes, fresh extraction and the full theorem audit support this configuration but do not prove all Rust/model correspondence. Arithmetic lemmas about unchanged scalar models are kernel proofs about those models, not proofs of the Rust intrinsics. Runtime overflow and undefined-behavior checks were enabled and contract checks disabled. Lean's foundational propext, Classical.choice and Quot.sound are allowed by the transitive axiom audit.