Module clock 

ClockStamp: pure formatting of an injected instant against already-resolved zone offsets, and the one spelling of a moment a person or a model reads: ISO 8601, UTC, to the second. Nothing here samples a clock; the calendar is integer arithmetic so replay and live share one algorithm and no tz database.

Emission (StampGate): Off emits never (A18 zero-byte); the first result of a run emits once; Timestamped tools emit every result; Timeless tools emit only when the granularity bucket changed. The bucket decides how often, never what a stamp says: a stamp always carries the reading it was given.

ClockReading is how a tool face learns what time it is without a clock of its own (crates/runtime/spec/Clock.lean §8-53).

Structs

ClockReading

The moment a run’s driver read its clock last, shared with the tool faces that report the time (crates/runtime/spec/Clock.lean §8-53).

ClockStamp

The stamp a result envelope carries: the reading itself, and the rows of the zones the run was frozen with (none, in a real city: the city refuses [clock] zones, crates/city/Spec.lean §8-31).

StampGate

Decides, per tool result, whether a stamp rides the envelope. One per run, built from the run’s frozen configuration.

UtcSpan

The moments a selection by time keeps: [since, until) in UTC, an absent end left open (crates/runtime/spec/Clock.lean §8-57).

ZoneEntry

One configured zone’s row: the offset it was computed from and the same second in that zone, 2026-05-14T18:31:07+09:00.

Functions

iso

One instant in ISO 8601, UTC, to the second: 2026-05-14T09:31:07Z. The clock line and status both write a moment through this; a reader that parses one back belongs beside it.

parse_iso

The moment raw spells in the one shape iso writes, 2026-05-14T09:31:07Z: UTC, to the second. The two are inverses: parse_iso(&iso(t)) is t with its milliseconds dropped, and iso(parse_iso(s)?) is s.

stamp

Formats one stamp of the reading now and every configured zone. Zones beyond CLOCK_ZONES_MAX are refused, not silently dropped.