Claim #4 — Verification of httpdate::parse_http_date (with creusot 0.13.0)
pub fn parse_http_date(s: &str) -> Result<std::time::SystemTime, Error>Tool: creusot 0.13.0
Preconditions
true
Evidence
What is trusted
From the report
The proofs reach the Rust standard library through a small set of modeled contracts. These are source-reviewed assumptions, not proofs of the standard library. They matter to a user in three places.
Timestamps
SystemTime is modeled as a nanosecond count with UNIX_EPOCH at zero. duration_since is assumed to return the nonnegative difference when it fits in a Duration, and an error for a negative difference (the error value is left unspecified). Adding a Duration to UNIX_EPOCH is assumed to produce a timestamp equal to the duration's nanosecond count; the proofs only use this with UNIX_EPOCH on the left and a duration within the supported range, and establish both bounds before relying on it. The recorded review of the pinned Rust 1.91.0 and nightly sources finds that the reviewed 64-bit Linux and macOS arm64 targets store SystemTime as a normalized Unix timespec with signed 64-bit seconds, which the bounded epoch addition fits. Clock reads and SystemTime arithmetic outside this pattern are not modeled.
Text
str::is_ascii, str::trim (on ASCII strings, removing bytes 9-13 and 32), str::as_bytes (preserving byte values on ASCII strings), and str::from_utf8 (succeeding and preserving characters on ASCII bytes) are assumed to behave as documented. The formatter's bytes are proved to be ASCII before from_utf8 is applied. These contracts connect the byte-level grammar proofs to the public String results; their implementations remain trusted.
Display
The Formatter model tracks the output already written and uses an "append sink" condition: a successful write_str appends the given text to the output provided the underlying writer faithfully appends successful writes, as a plain buffer does and a writer that inserts indentation or transforms text does not. The pinned Rust 1.91 source forwards the formatter's write_str unchanged to the underlying writer. This explains the boundary but does not establish faithful behavior or panic freedom for an arbitrary user-supplied writer. The output guarantee is relative to whatever the writer already contained; no empty initial buffer is assumed.
Other standard operations (Duration, Result, slices, integers, string views) rely on Creusot's standard library models. The complete list of 41 conditional declarations, including those for traits outside this report's scope, is in the assumptions ledger kept with the evidence.
Technical limitations
From the report
Adapted source
The verified code is a fork of httpdate 1.0.3, not the unmodified crates.io artifact. Before modification, the two runtime files copied from the source Git revision, src/lib.rs and src/date.rs, match the crates.io release byte for byte; the archive SHA-256 and source revisions are recorded with the evidence.
The fork restructures the implementation so intermediate values and relationships can be specified:
- Parsing and validation: a private
RawDateholds syntactically parsed fields. Checked bridges preserve all seven fields when validation constructs a publicHttpDate. - Calendar arithmetic: integer helpers expose the calculations. Validity is checked by a raw whole-second round trip instead of a public
SystemTimeround trip. - Parser control flow: explicit ordered matches and scalar comparisons replace
Result::or_elseand byte-string slice patterns, preserving the original parser order. - Formatting: the
Stringis built from the extracted 29-byte layout rather thanformat!.
Several derived or default trait implementations (Clone, Eq, Ord, Hash, Debug, Error) are also made explicit. Their selected proofs are outside this report's four-API scope.
Relationship to the release
Equivalence between the fork and the release is supported by source review and finite native comparison, not by formal proof. The recorded comparison runs both programs side by side on one representative instant of every supported civil day (2,932,897 days), on boundary and fractional-second instants, on 132,353 additional parser cases covering valid, malformed, and mutated inputs, and on formatting and writer-failure cases, with agreement on all of them. These are comparison counts, not counts of unique input strings. Four small runtime helpers (toint_1, toint_2, toint_4, is_leap_year) are checked byte for byte against the release. Allocation behavior and performance equivalence are not established.
Out-of-range input
Before the Unix Epoch and from year 10000 on, SystemTime-to-date conversion and fmt_http_date panic, in the release as in the fork. Because the From<SystemTime> for HttpDate trait accepts any SystemTime, its unconditional trait obligation is the one open goal in the supporting full-suite run; proving the implementation body on the supported range does not close it, and this report makes no claim for out-of-range timestamps.
Not claimed
Complete crate coverage; a general Rust undefined-behavior proof; behavior with arbitrary writers; and the release's Rust 1.56 minimum version (the fork requires Rust 1.91). The supporting full-suite run is a fresh macOS arm64 execution; 64-bit Linux is covered by the same source review of the standard library, but this run is not a fresh Linux execution and no other platform is claimed.
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