Report #21 — CR/LF/CRLF normalization for finite character lists (adapted source)

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

1 verified claim · 0 findings

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

nyuichi · 2026-11-04 14:31 UTC

Revision v5 · v4 · v3 · v2 · v1

Overview

For every finite character list, the Aeneas translation of normalize-line-endings 0.3.0's adapted normalized constructor and Iterator::next returns exactly the list obtained by replacing each CRLF pair and each remaining CR with LF, while preserving other characters. The proof uses a total, fused list iterator and an observation budget greater than the input length, with no fixed input bound. The output contains no CR, is no longer than the input, and is unchanged by another normalization pass. The constructor and next bodies are dependencies of the checked public theorem. Extraction required replacing three character patterns with equality guards. Kani additionally checks one-step equivalence of the actual original and adapted next bodies for both prior-state flags and all possible character replies in a non-panicking two-reply iterator trace model: returned value, adapter state, callback count, and remaining modeled iterator state agree. The Aeneas theorem applies to the adapted extraction. Separate original-source evidence now proves the unchanged normalized constructor directly with official Aeneas: for every translated iterator and Iterator dictionary it returns that iterator and initializes the previous-CR flag to false. This says nothing about later next calls. Independently, Kani checks original iterator outputs for lengths zero through four and every valid Unicode scalar value against an eager CR/LF/CRLF reference: exact output, no CR, nonincreasing length, idempotence, two exhausted None replies, and the initial inherited Iterator size_hint default. The Kani input iterator is total and finite; unwind bound eight retains unwinding assertions (437 successful checks). These original-source supplements are distinct from the one adapted-source machine claim. Further original-source Kani checks execute actual inherited Iterator::nth/count/last defaults and original next on a concrete fused input with0..4 characters drawn from every Unicode scalar. Every usize nth index, including usize::MAX, is covered: nth returns the independent normalized reference element and remaining suffix with persistent EOF; count returns its exact length and last its exact final element. Separate original inherited Iterator::position/find Kani checks cover0..4 input characters and every Unicode scalar target under a concrete pure equality predicate. They return the first normalized position or character and preserve exactly the remaining normalized suffix with persistent EOF.

Findings (0)

No findings reported.

APIs (1)

Functions

pub fn normalized<impl Iterator<Item = char>: Iterator<Item = char>>(iter: impl Iterator<Item = char>) -> impl Iterator<Item = char>

Claim #1

Evidence

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

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/nyuichi/rust-crate-proofs report-21-source-1
git -C report-21-source-1 checkout --detach c62096154ea0e42bc164f2606f1c24fc4194d9c9
git -C report-21-source-1 submodule update --init --recursive --checkout
cd report-21-source-1/normalize-line-endings/0.3.0/aeneas/2026-11-04/proofs

lake build +Proofs

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

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

2026-11-05T08:55:41.128855170+00:00 · 90.9 seconds · Exit code 0

Recorded on the author’s machine.

Check	Result	Claim
Lean checked theorem Proofs.normalized_spec; axioms limited to propext, Classical.choice, Quot.sound `Proofs.normalized_spec`	Passed	Claim #1

Execution details

Started: 2026-11-05T08:55:41.128855170+00:00
Finished: 2026-11-05T08:57:12.037367579+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: normalize-line-endings/0.3.0/aeneas/2026-11-04/proofs
Environment overrides: None recorded
Git repository: https://github.com/nyuichi/rust-crate-proofs
Git commit: c62096154ea0e42bc164f2606f1c24fc4194d9c9

Diagnostics & logs

=== stdout ===
⚠ [2/57] Ran aeneas:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
✔ [3/140] Built AeneasMeta.Simp.RegisterCommand (39s)
✔ [83/268] Built AeneasMeta.BvEnumToBitVec (39s)
✔ [515/909] Built Aeneas.Std.Global (39s)
✔ [516/909] Built AeneasMeta.UtilsCore (40s)
✔ [1575/1801] Built AeneasMeta.OptionConfig (40s)
✔ [1797/1801] Built NormalizationSpec (887ms)
✔ [1798/1801] Built OriginalConstructorGenerated.NormalizeLineEndings (2.0s)
✔ [1799/1801] Built Generated.NormalizeLineEndings (2.0s)
ℹ [1800/1801] Built OriginalConstructorSupplement (2.7s)
info: OriginalConstructorSupplement.lean:6:0: 'OriginalConstructorSupplement.initializes' depends on axioms: [propext, Quot.sound]
ℹ [1801/1801] Built Proofs (2.6s)
info: Proofs.lean:93:0: 'Proofs.normalized_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
Build completed successfully (1801 jobs).

$ lake env lean --stdin (proofs.rs theorem/axiom audit)
proofs.rs:checked:Proofs.normalized_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

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a; Charon 08d7c9d50144bd84848212c24701253585e90d1f; Rust nightly-2026-09-17; Lean 4.35.0. Proofs.normalized_spec is checked by lake build and a transitive axiom audit. Kani 0.68.0 / CBMC 6.11.0 / Rust nightly-2026-08-21 checked 1 equivalence harness with 314 checks and 0 failures. Source archives, adaptation patch, byte-preserving Kani source embedding, generated Lean, translation manifest, and recorded results are included. cargo-proofs 0.4.1 uses environment-CA trust and an audit-local variable rename matching official upstream commit 74acff732c94bc23142913cd03d398b40648fc27 for Lean 4.35 compatibility. The theorem checks and allowed-axiom policy are unchanged. Original nth/count/last supplement:3Kani harnesses,417/355/390 checks (1162 total),0fail, unwind8 with assertions; archive-identical source and manifest/default/x86_64/nightly2026-08-21; evidence/kani-iterator-defaults. Original position/find supplement:480+429=909 Kani checks,0fail, unwind8 with assertions, source/manifest/archive unchanged; nightly2026-08-21/default/x86_64; evidence/kani-iterator-search.

What is trusted

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

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.

Updated 2026-10-16 00:00 UTC

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a — version details

Dependencies (0)

No direct dependencies.

Comments (0)

No comments.