Claim #1 — Cloning preserves the parser state and accumulator
<utf8parse::Parser as Clone>::clone
impl Clone for Parser
pub fn clone(self: &Self) -> ParserTool: creusot 0.13.0
Overview
The verified clone copies the current parser state and accumulator and preserves the reachable-state invariant without panicking. This is the explicit cfg(creusot) implementation; ordinary builds use the derived implementation.
Preconditions
true
Evidence
What is trusted
From the report
Receiver::codepoint and Receiver::invalid_sequence are abstract calls; their bodies, side effects and event histories are not proved. Normal return is needed for the stated post-call state, and non-panicking callbacks are needed for panic freedom. Verification-only equality implementations for State and Parser are assumed to agree with their state/accumulator models. The external char::from_u32_unchecked contract is assumed to construct the specified character for a valid scalar; the parser proves that scalar precondition at each call. Creusot's core-operation models remain assumptions.
Technical limitations
From the report
The fork changes perform_action to borrow only the accumulator instead of the whole Parser, and replaces derived implementations under cfg(creusot). The source/provenance describes preservation of byte operations and callback order, but the recorded proof does not prove equivalence to the unmodified crates.io release. Receiver effects and full output histories remain unspecified, including behavior after a callback panic. Proving the scalar precondition at one unsafe operation is not a complete Rust undefined-behavior proof. Other feature configurations and targets are outside this recording.
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