Claim #3 — One-byte state updates under normally returning receiver callbacks
impl Parser
pub fn advance<R>(self: &mut Self, receiver: &mut R, byte: u8) where R: ReceiverTool: creusot 0.13.0
Overview
For every byte and valid reachable parser state, advance follows the specified transition table and preserves the accumulator/state invariant after callbacks return normally. All unchecked character constructions satisfy the Unicode scalar precondition. Panic freedom additionally requires non-panicking receiver callbacks; their implementations and output histories are outside the proof.
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