[atiernan]

Path validation P1 (3.5b, .claude/plans/path-validation.md §1.5). It adds time::from_unix_seconds, which turns the current time in Unix seconds into the CertificateTime that validity checks compare against. clazel-x509 stays at tier 0.

Commits

Spec and contract come before any exec code:

• 9822e8b spec: from_unix_seconds
• 52e730a contract
• 0e15905 spec: names the year bound
• 80e9e32 lemmas and known answers
• 276d062 spec: a header reflow only
• dfd492a exec and tests
• fd5d61b mutations

Spec

from_unix_seconds(t) is POSIX.1-2017 XBD §4.16 "Seconds Since the Epoch" read backwards. It is a plain walk:

• it splits t into days and the second of the day;
• it walks year by year from 1970 (using the existing is_leap_year), then month by month (using the existing days_in_month);
• it is None exactly when the year would pass 9999, following RFC 5280 §4.1.2.5's four-digit years.

Second 60 is never produced. The header lists the modelling choices.

Proven

These need no axioms:

• lemma_from_unix_monotone: a <= b and f(b) Some imply f(a) Some and time_le(f(a), f(b)).
• lemma_from_unix_injective.
• lemma_from_unix_none_iff: None iff t > 253402300799.
• lemma_from_unix_valid: a valid calendar time, never second 60.
• Exec from_unix_seconds(u64): uses the 400-year (146,097-day) cycle and walks at most 400 years and 12 months, with saturating arithmetic. It is proven equal to the spec.

Known answers

Each is proven, and also unit-tested:

Unix seconds	Result
0	1970-01-01T00:00:00
951782400	2000-02-29
951868800	2000-03-01
2147483647	2038-01-19T03:14:07
4107542400	2100-03-01 (2100 is not a leap year)
253402300799	9999-12-31T23:59:59
253402300800	None
u64::MAX	None

All were cross-checked with Python's calendar.timegm, and a Python port of the spec matched datetime on 20,000 random values.

Checks done

• Verus: 268 verified, 0 errors for clazel-x509, from a clean cache. Re-run independently of the agent.
• Mutations: cargo xtask mutate clazel-x509 killed all 40 with certificates. Seven are new: dropping the 100 rule, dropping the 400 rule, February's length, the 30-day months, seconds per day, the epoch year and the 9999 bound. The 33 existing mutations are unchanged.
• Other checks: tests, clippy, fmt and cargo xtask check pass.

Limits

• The 9999-bound certificate is weak. It is checked against a constant-level lemma (max_year() == 9999), because compute_only cannot walk 8,030 years. The mutant also breaks lemma_from_unix_none_iff and the 9999 example, but those can't be the certificate.
• No equality proof with the POSIX formula. The spec is not proven equal to POSIX's closed formula. The evidence is the known answers and the Python cross-check. An independent.rs would be the tier-2 route.

CI has not run yet.

🤖 Generated with Claude Code