Claim #2 — Default creates a parser in the ground state
<utf8parse::Parser as Default>::default
impl Default for Parser
pub fn default() -> ParserTool: creusot 0.13.0
Overview
The verified default returns a parser in State::Ground with accumulator zero and establishes its reachable-state invariant without panicking. It delegates to new; ordinary builds use the derived Default 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