Report #6 — httpdate 1.0.3: correct HTTP-date parsing and bounded formatting

4 verified claims · 0 findings

Recorded by the author; proofs.rs has not re-run it. How to read a report

keiichiw · 2026-10-15 18:00 UTC

Revision v2 · v1

Overview

httpdate parses dates in HTTP headers and formats timestamps as IMF-fixdate. This report covers four API bodies in a verification fork of version 1.0.3. All guarantees depend on the standard-library assumptions below; the relationship to the published crate is described under Technical limitations.

API	Input domain	Guaranteed result
`HttpDate::from_str`	Any input string	A calendar-valid `HttpDate` matching the trimmed input, or rejection as described below
`parse_http_date`	Any input string	The same acceptance behavior, returning the corresponding whole-second `SystemTime`
`fmt_http_date`	`SystemTime` in the supported range	Canonical 29-character IMF-fixdate in GMT, with fractional seconds discarded
`Display for HttpDate`	Valid `HttpDate`	The same canonical text when the write succeeds and the writer is an append sink

Supported timestamp range: UNIX_EPOCH <= t < UNIX_EPOCH + 253402300800 seconds, from 1970-01-01 through the end of 9999-12-31, including fractional seconds. Parsing accepts arbitrary strings for validation; it can only return dates in this range.

Parsing

For every input string, HttpDate::from_str either rejects it or returns a valid date whose seven fields—second, minute, hour, day, month, year, and weekday—match the input after ASCII whitespace is trimmed. parse_http_date accepts the same inputs and returns the corresponding whole-second SystemTime.

Calendar validity: the date is in the supported range, the day exists in its month, leap years follow the Gregorian rule, and the weekday agrees with the date.
Accepted formats: IMF-fixdate, RFC 850, and asctime, tried in that order. Non-ASCII input is rejected; two-digit RFC 850 years map to 1970–2069.
Error completeness: if a trimmed input matches one of the three grammars, it is rejected only when the encoded date is calendar-invalid. A well-formed encoding of a valid date is never rejected.

Compatibility quirk: the RFC 850 separator byte between the year and time is not checked, matching upstream. For example, Sunday, 06-Nov-94x08:49:37 GMT is accepted. This is not a claim of strict RFC conformance.

Formatting

For every SystemTime t in the supported range, fmt_http_date returns the canonical 29-character IMF-fixdate string for t in GMT, truncating fractional seconds. Converting a SystemTime in the supported range to an HttpDate and back returns the original time truncated to whole seconds. Display for HttpDate writes the same 29-character string, under one condition: the guarantee applies only when the write succeeds and the writer behind the Formatter appends what it is given (see What is trusted); nothing is promised about partial output when a write fails.

Panic freedom

For arbitrary parser inputs, timestamps in the supported formatting range, and valid HttpDate values passed to Display, the selected bodies are proved free of panics, including arithmetic overflow and out-of-bounds indexing, given the modeled library contracts. Not covered: allocation failure, aborts, and panics raised by a user-supplied writer. The proofs cover the parsing, calendar, validation, conversion, and formatting helpers these APIs call, together with their supporting lemmas; the application helpers are proved, not assumed.

Findings (0)

No findings reported.

APIs (4)

Functions

pub fn fmt_http_date(d: std::time::SystemTime) -> String

Claim #3

pub fn parse_http_date(s: &str) -> Result<std::time::SystemTime, Error>

Claim #4

Trait implementations

`impl core::fmt::Display for HttpDate`

pub fn fmt(self: &Self, f: &mut Formatter<'_>) -> fmt::Result

Claim #1

`impl core::str::traits::FromStr for HttpDate`

pub fn from_str(s: &str) -> Result<HttpDate, Error>

Claim #2

Evidence

https://github.com/keiichiw/crate-proofs/tree/1bbd58e2f53cc5f5aacdbb0af080a8206350eab9

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/keiichiw/crate-proofs report-6-source-1
git -C report-6-source-1 checkout --detach 1bbd58e2f53cc5f5aacdbb0af080a8206350eab9
git -C report-6-source-1 submodule update --init --recursive --checkout
cd report-6-source-1/httpdate/1.0.3

cargo creusot -p httpdate --span-mode absolute --output-dir verif/submission-d21bnvk5/coma --no-cache '--why3find-arg=--prover=-cvc4,-cvc5' --why3find-arg=-j --why3find-arg=2 --why3find-arg=--fast=1 --why3find-arg=--time=10 --why3find-arg=-d --why3find-arg=2 verif/submission-d21bnvk5/coma/verif/httpdate_rlib/parse_http_date.coma verif/submission-d21bnvk5/coma/verif/httpdate_rlib/fmt_http_date.coma verif/submission-d21bnvk5/coma/verif/httpdate_rlib/date/impl_FromStr_for_HttpDate/from_str.coma verif/submission-d21bnvk5/coma/verif/httpdate_rlib/date/impl_Display_for_HttpDate/fmt.coma

Checks out the recorded source commit from GitHub. Install the report’s tool version before running.

Source on GitHub · SARIF with logs (.json)

Recorded run

Completed · 22 checks passed · 0 failed

2026-10-15T17:44:41.415226+00:00 · 20.9 seconds · Exit code 0

Recorded on the author’s machine.

Check	Result	Claim
vc_as_raw `httpdate::<httpdate::date::HttpDate as std::fmt::Display>::fmt` `httpdate/1.0.3/crate/src/date.rs:633`	Passed	Claim #1
vc_fmt_HttpDate `httpdate::<httpdate::date::HttpDate as std::fmt::Display>::fmt` `httpdate/1.0.3/crate/src/date.rs:633`	Passed	Claim #1
vc_from_utf8 `httpdate::<httpdate::date::HttpDate as std::fmt::Display>::fmt` `httpdate/1.0.3/crate/src/date.rs:633`	Passed	Claim #1
vc_imf_bytes `httpdate::<httpdate::date::HttpDate as std::fmt::Display>::fmt` `httpdate/1.0.3/crate/src/date.rs:633`	Passed	Claim #1
vc_unwrap_ref_str `httpdate::<httpdate::date::HttpDate as std::fmt::Display>::fmt` `httpdate/1.0.3/crate/src/date.rs:633`	Passed	Claim #1
vc_write_str_Formatter `httpdate::<httpdate::date::HttpDate as std::fmt::Display>::fmt` `httpdate/1.0.3/crate/src/date.rs:633`	Passed	Claim #1
vc_as_bytes `httpdate::<httpdate::date::HttpDate as std::str::FromStr>::from_str` `httpdate/1.0.3/crate/src/date.rs:571`	Passed	Claim #2
vc_elim_Err `httpdate::<httpdate::date::HttpDate as std::str::FromStr>::from_str` `httpdate/1.0.3/crate/src/date.rs:571`	Passed	Claim #2
vc_elim_Ok `httpdate::<httpdate::date::HttpDate as std::str::FromStr>::from_str` `httpdate/1.0.3/crate/src/date.rs:571`	Passed	Claim #2
vc_from_raw `httpdate::<httpdate::date::HttpDate as std::str::FromStr>::from_str` `httpdate/1.0.3/crate/src/date.rs:571`	Passed	Claim #2
vc_from_str_HttpDate `httpdate::<httpdate::date::HttpDate as std::str::FromStr>::from_str` `httpdate/1.0.3/crate/src/date.rs:571`	Passed	Claim #2
vc_is_ascii `httpdate::<httpdate::date::HttpDate as std::str::FromStr>::from_str` `httpdate/1.0.3/crate/src/date.rs:571`	Passed	Claim #2
vc_parse_date_bytes `httpdate::<httpdate::date::HttpDate as std::str::FromStr>::from_str` `httpdate/1.0.3/crate/src/date.rs:571`	Passed	Claim #2
vc_trim `httpdate::<httpdate::date::HttpDate as std::str::FromStr>::from_str` `httpdate/1.0.3/crate/src/date.rs:571`	Passed	Claim #2
vc_fmt_http_date `httpdate::fmt_http_date` `httpdate/1.0.3/crate/src/lib.rs:120`	Passed	Claim #3
vc_from_HttpDate `httpdate::fmt_http_date` `httpdate/1.0.3/crate/src/lib.rs:120`	Passed	Claim #3
vc_imf_string `httpdate::fmt_http_date` `httpdate/1.0.3/crate/src/lib.rs:120`	Passed	Claim #3
vc_elim_Err `httpdate::parse_http_date` `httpdate/1.0.3/crate/src/lib.rs:102`	Passed	Claim #4
vc_elim_Ok `httpdate::parse_http_date` `httpdate/1.0.3/crate/src/lib.rs:102`	Passed	Claim #4
vc_from_SystemTime `httpdate::parse_http_date` `httpdate/1.0.3/crate/src/lib.rs:102`	Passed	Claim #4
vc_from_str_HttpDate `httpdate::parse_http_date` `httpdate/1.0.3/crate/src/lib.rs:102`	Passed	Claim #4
vc_parse_http_date `httpdate::parse_http_date` `httpdate/1.0.3/crate/src/lib.rs:102`	Passed	Claim #4

Execution details

Started: 2026-10-15T17:44:41.415226+00:00
Finished: 2026-10-15T17:45:02.319060+00:00
Platform: macos aarch64
Rust compiler: rustc 1.91.0 (f8297e351 2025-10-28) binary: rustc commit-hash: f8297e351a40c1439a467bbbb6879088047f50b3 commit-date: 2025-10-28 host: aarch64-apple-darwin release: 1.91.0 LLVM version: 21.1.2
Working directory: httpdate/1.0.3
Environment overrides: None recorded
Git repository: https://github.com/keiichiw/crate-proofs
Git commit: 1bbd58e2f53cc5f5aacdbb0af080a8206350eab9

Diagnostics & logs

=== stdout ===
Proved (4 files) ✔

=== stderr ===
   Compiling proc-macro2 v1.0.107
   Compiling unicode-ident v1.0.26
   Compiling libc v0.2.190
   Compiling quote v1.0.47
   Compiling getrandom v0.4.3
   Compiling cfg-if v1.0.5
   Compiling syn v2.0.119
   Compiling uuid v1.27.0
   Compiling pearlite-syn v0.13.0
   Compiling creusot-std-proc v0.13.0
    Checking creusot-std v0.13.0
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"std"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"core"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"alloc"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"compiler_builtins"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"libc"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"rustc_std_workspace_core"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"unwind"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"miniz_oxide"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"adler2"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"hashbrown"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"rustc_std_workspace_alloc"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"std_detect"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"rustc_demangle"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"cfg_if"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"addr2line"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"gimli"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"object"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"memchr"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"panic_unwind"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:53Z WARN  creusot::metadata] could not read metadata for crate `"creusot_std_proc"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
    Checking httpdate v1.0.3 (./httpdate/1.0.3/crate)
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"std"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"core"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"alloc"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"compiler_builtins"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"libc"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"rustc_std_workspace_core"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"unwind"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"miniz_oxide"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"adler2"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"hashbrown"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"rustc_std_workspace_alloc"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"std_detect"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"rustc_demangle"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"cfg_if"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"addr2line"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"gimli"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"object"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"memchr"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"panic_unwind"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
[2026-10-15T17:44:54Z WARN  creusot::metadata] could not read metadata for crate `"creusot_std_proc"`: Os { code: 2, kind: NotFound, message: "No such file or directory" }
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 13.08s

Environment

Recorded environment

Component	Supporting full-suite run
Source snapshot	`crate-proofs` commit `9e9100c8b1727568d60a9db388f352eb4a8bf040`, directory `httpdate/1.0.3`
Execution platform	macOS arm64
Native Rust	1.91.0
Creusot	0.13.0, commit `318615be3b8bbc60d1f6d52469ba5c0bdebed4f1`, unmodified source checkout
Translation toolchain	`nightly-2026-06-22`
Provers	Why3, Why3find, and solver identities pinned in the formal manifest

The version-local prover configuration uses per-query CVC5 time limits, affecting proof search rather than the logical statements.

Evidence

Paths below are relative to httpdate/1.0.3/ in the evidence repository.

Evidence	Location
Formal run and independent audit	`verification/evidence/httpdate-run-Nh8aCaki/manifest.json` and `independent-audit.json` in the same directory
Native correspondence, separately bound to the formal run	`verification/correspondence/evidence/correspondence-qZmQ5PXk/manifest.json`
Verified scope and results	`verification/coverage.md`
Standard-library assumptions	`verification/stdlib-assumptions.md`
Release provenance and source-change table	`verification/correspondence/README.md`
Separate API-recording procedure	`verification/proofs-rs-report-review.md`

The full-suite archive includes the application helpers used by the four reported APIs. Native comparison is finite regression evidence, not formal equivalence with the release.

Submission recording is a separate run that retains source positions and checks those four APIs against matching source and contracts. Its source revision and execution details belong to the recorded SARIF. The Creusot importer records panic_contract; the functional guarantees described here are supported by the proof archive, not separately registered functional-correctness or no_ub claims.

Reproduction

From the repository root, in the documented verification environment, reproduce the formal run with:

bash httpdate/1.0.3/scripts/verify.sh

Run the independent native comparison using ordinary Rust/Cargo with:

bash httpdate/1.0.3/scripts/check-correspondence.sh

What is trusted

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

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 RawDate holds syntactically parsed fields. Checked bridges preserve all seven fields when validation constructs a public HttpDate.
Calendar arithmetic: integer helpers expose the calculations. Validity is checked by a raw whole-second round trip instead of a public SystemTime round trip.
Parser control flow: explicit ordered matches and scalar comparisons replace Result::or_else and byte-string slice patterns, preserving the original parser order.
Formatting: the String is built from the extracted 29-byte layout rather than format!.

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

Updated 2026-09-24 05:03 UTC

creusot 0.13.0 — version details

Dependencies (1)

CrateReports

criterion ^0.5 · dev—

Comments (0)

No comments.