Claim #1 — Verification of normalize_line_endings::normalized (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)
normalize_line_endings::normalized
pub fn normalized<impl Iterator<Item = char>: Iterator<Item = char>>(iter: impl Iterator<Item = char>) -> impl Iterator<Item = char>Tool: Aeneas be86ab0f1989d04944292b345b24c435be3ad10a
Preconditions
The underlying iterator is the total, fused finite-character-list model; the observation budget exceeds the input length. The extracted source replaces three character patterns with equality guards.
Evidence
What is trusted
From the report
The Rust compiler, Charon/Aeneas translation, their standard-library models, and the Lean kernel are trusted; the supplementary equivalence result also trusts Kani/CBMC and its Rust compilation/modeling. The input iterator is modeled as consuming one character per successful call and returning None permanently after exhaustion. No additional local axioms are used; the public theorem depends only on Lean's propext, Classical.choice, and Quot.sound.
Technical limitations
From the report
The original crates.io source is retained unchanged, but its character-pattern switches are unsupported by the pinned Aeneas translator. The three guard replacements have a Kani-checked one-step equivalence under the documented two-reply, non-panicking callback model. This is not a generic contextual-equivalence proof for every Rust Iterator implementation, nor a direct arbitrary-length Aeneas proof of the unmodified iterator next body. The original constructor alone is separately body-proved; bounded original iterator Kani behavior does not establish arbitrary-length or arbitrary-callback behavior. The end-to-end Aeneas guarantee remains scoped to the adapted extraction and total fused list iterator model. Arbitrary external iterators, their panics or divergence, and iterators that resume after None are outside the end-to-end theorem. No separate general memory-safety claim is made. The inherited-default supplement is restricted to this concrete fused input and length0..4; the nth index itself is unbounded over usize. It does not establish arbitrary input lengths or Iterator implementations, other defaults, generic contextual equivalence or an original arbitrary-length next theorem. It adds no Aeneas mapping and does not broaden the adapted-source primary theorem. The search supplement is limited to the same finite concrete fused input and pure equality predicate. It does not establish arbitrary callbacks, generic iterators or lengths, internal raw cursor behavior, other inherited APIs or arbitrary-length original next correctness. The adapted-source primary mapping is 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.
Aeneas be86ab0f1989d04944292b345b24c435be3ad10a — version details