Claim #1 — Verification of unindent::unindent (with creusot 0.13.0)
Tool: creusot 0.13.0
Preconditions
true
Evidence
What is trusted
From the report
The proof uses Creusot's standard-library models for arithmetic, slices, vectors, results, characters, and strings. These describe observable values and operations rather than proving the standard library or allocator. In addition, the model assumes two standard UTF-8 encoding facts: an ASCII scalar encodes as its corresponding single byte, and every byte encoding a non-ASCII scalar is at least 128. It models str::as_bytes as the UTF-8 encoding of the string view and String::from_utf8 as succeeding exactly for bytes with a valid encoding witness, preserving those bytes. These are assumptions about standard encoding and conversion, not assumptions that unindentation preserves UTF-8; the application preservation bridge is a separate proof obligation.
Technical limitations
From the report
The executable proof subject is a verification adaptation: it replaces the release's iterator-based processing with indexed margin discovery and a bytewise retention scan. Extraction of the original Split pipeline is unsupported by this track. Finite native comparisons against the release covered 300,617 byte inputs, 299,593 Unicode inputs, and 74,898 input/flag pairs; these comparisons are evidence of agreement on those cases, not an all-input equivalence proof. No formal release-equivalence theorem is established.
The checked output contract is expressed in terms of retained source positions. An independent mathematical review relates it to the separate sequence-of-lines specification, but a machine-checked bridge between those specifications remains open. The generic &T extension is available in native code and excluded from this Creusot selection; behavior of an arbitrary downstream T is not covered. The prior Aeneas report is a separate result tied to its own inputs.
The cargo-proofs 0.4.1 Creusot importer records only panic_contract. The local functional and termination contracts described here are not additional service functional_correctness or no_ub claims.
The models do not establish allocation availability or behavior under external resource exhaustion. Other targets and minimum supported Rust versions are outside this run's scope.
Tool limitations
Verification is relative to the supplied specifications and trusted contracts. Results apply to the compilation target used for verification. The standard-library specifications do not exclude all panics: Vec capacity overflow in operations such as push, insert, and extend is not ruled out, including for vectors of zero-sized types. Out-of-memory failures are also outside the guarantees. The standard vec! macro is unsupported; verified code must use the Creusot replacement where needed. Reference: https://github.com/creusot-rs/creusot/blob/v0.13.0/guide/src/limitations.md