= Module: kairos
:toc: macro
:toclevels: 2
Design notes for the `kairos` module, co-located with its Rust module files.
This is the implementer's view: the type inventory, the concurrency
walk-through, and the invariants a change must not break. Product-level intent lives in
xref:../../docs/prd/0001-kairos-hybrid-logical-clock.adoc[PRD 0001]; the wider
plan is in xref:../../docs/target_arch/index.adoc[the target architecture].
toc::[]
== Responsibility
`kairos` owns the causal stamp and the clock that mints it. It does not own time
itself (that is the `TimeSource` seam) nor any decision made from a stamp (that
is the `metis` layer). One reason to change this module: the stamp format or the
rules for advancing it.
== Type inventory
[cols="1,2,3",options="header"]
|===
| Type | Kind | Role
| `Kairos` | `u128` newtype | The 128-bit causal stamp. Packing in
`Kairos::new` (`stamp/mod.rs:45`); getters in `stamp/mod.rs`; canonical wire
codec `to_bytes`/`from_bytes` in `stamp/wire.rs` (PRD 0002).
| `DecodeError` | enum (`#[non_exhaustive]`) | `from_bytes` structural failure:
`UnknownVersion` / `UnexpectedLength` (`stamp/wire.rs:102`).
| `Clock` | struct | The thread-safe HLC shell: the shared pure fold committed
through an `AtomicU128` compare-and-swap loop (`clock/mod.rs:27`).
| `LocalClock` | struct | The single-threaded HLC shell (S188): the same fold
committed through a `Cell`: no fences, no retries, `!Sync` by construction
(`clock/local.rs:53`). The zero-cost form for wasm and per-shard owned minters.
| `fold::advance` | pure `const fn` (private) | The whole time algebra: one HLC
step over plain machine words, shared by both shells and reached whole by the
checkers (`clock/fold.rs:171`); returns an `Advance` (`clock/fold.rs:32`), the
pair to commit plus the skew observed computing it.
| `KairosRun` | struct | The run-mint reservation receipt (S211, ruling R-33):
the first stamp plus the reserved length, members derived by the fold's own
send-step successor (`clock/run.rs`; construction crate-private, so within
this crate only the minting shells produce one). Affine: neither `Clone`
nor `Copy`, consumed by value at `metis`'s `Rhapsody::weave_run`, so a
reservation spends at most once (the S211 gate review's finding, cured in
the type). `KairosRunIter` is its exact-size borrowing member iterator.
| `fold::advance_run` / `fold::rank_offset` | pure `const fn` (private) | The
run generalization (`clock/fold.rs:112` / `clock/fold.rs:81`): one fold
application reserving `len` send positions, the committed pair the
closed-form offset of the first, Kani-proven equal to the iterated send
against a frozen reading.
| `ClockState` | `u128` newtype (private) | Meaning of the atomic word:
`Option<(physical, logical)>` of the last mint, behind an explicit init tag bit
(`clock/state.rs:23`). Replaces the old `u64::MAX` sentinel.
| `ClockConfig` | struct | Skew warning threshold + backoff strategy (`clock/config.rs:5`).
| `ClockStats` | `Copy` struct | Skew snapshot plus the `peak_attempts`
contention high-water mark (`clock/config.rs:26`).
| `InvalidStationId` | struct | A clock constructor received station zero
(`clock/error.rs:5`).
| `SkewExceeded` | struct | `try_observe` rejection: the observed forward skew and
the bound it exceeded (`clock/error.rs:21`). The clock is left unchanged on this error.
| `TimeSource` | trait (seam) | Physical-time provider, `Send + Sync` (`time.rs:7`).
| `TickCounter` | struct | Deterministic auto-ticking `TimeSource` for tests:
`now` increments on each read (`time.rs:14`).
| `VirtualTimeSource` | struct | Caller-advanced `TimeSource` over a shared
`Arc<AtomicU64>`: `now` reads without moving; `set`/`advance` drive it. `no_std`,
for tests and deterministic simulation (`time.rs:53`).
| `Backoff` | trait (seam) | Per-attempt spin policy; returns `()`, never aborts and
never reads time (spin-count, not wall-clock; `backoff/mod.rs:11`).
| `BackoffStrategy` | enum | Concrete dispatch over the three strategies (`backoff/mod.rs:38`).
| `ConstantBackoff` / `ExponentialBackoff` / `ModelBasedBackoff` | structs | Spin-count
strategies (`backoff/constant.rs:7`/`backoff/exponential.rs:7`/`backoff/model.rs:5`).
| `LcgJitter` | struct (private, `#[cfg(not(rand))]`) | `no_std` jitter PRNG when
`rand` is off; seeds spin-count jitter (`backoff/jitter.rs:10`).
| `ToU16` | trait (seam) | Caller kairotic to `u16` (`stamp/mod.rs:8`).
|===
== Stamp layout
See xref:../../docs/target_arch/core-invariant.adoc#_the_core_invariant_the_kairos_stamp[the
canonical layout diagram]. In short: `physical:u64 | logical:u16 | kairotic:u16
| station_id:u32`, most significant first, so the derived `Ord` is the intended
`(chronos, logical, kairotic, station)` total order. Touching the shift offsets
in `Kairos::new` or the getters is a breaking change to the ordering contract.
The canonical wire encoding (`to_bytes`/`from_bytes`, PRD 0002) is this same packed
value as a version-tagged big-endian 17-byte frame, so byte-wise frame order equals
`Ord`. The in-memory `u128` stays private; the versioned frame is the stable form,
and `from_bytes` is the module's only untrusted-input boundary (it validates frame
length and version, never `station_id`, and never panics).
== Clock operations: one fold, two shells, five operations
The HLC operations are thin wrappers over one shared *pure* fold,
`fold::advance` (`clock/fold.rs:171`, extracted S188 under ruling R-19): given the
last committed `(physical, logical)`, one reading, and an optional remote's
`(physical, logical)`, it returns the next pair and the skew it observed. A
*shell* owns only commitment: `Clock` runs the fold inside an `AtomicU128`
compare-and-swap loop (`advance_from`, `clock/mod.rs:325`), `LocalClock` commits
it with a `Cell` store (`clock/local.rs:205`), and their agreement on any
operation tape is pinned by
`prop_local_clock_agrees_with_atomic_clock_on_any_tape`. On each shell,
`advance` samples the time source once and hands the reading down; a
skew-checking caller (`try_observe`) reads the source, decides, then commits
against that *same* reading by calling `advance_from` directly. The `Clock`
operations:
[horizontal]
`now` (`clock/mod.rs:110`; `LocalClock` mirror `clock/local.rs:112`):: the *send* step. `advance(None)`, wrapped into a `Kairos`.
`now_run` (`clock/mod.rs:159`; `LocalClock` mirror `clock/local.rs:130`):: the *run
mint* (S211, ruling R-33): one reading and one commitment reserving `len`
consecutive send positions. `fold::advance_run` (`clock/fold.rs:112`) computes
the first stamp as `advance(last, reading, None)` and the committed pair as
the closed-form `rank_offset` (`clock/fold.rs:81`) of the first, proven equal
to iterating the send step against the frozen reading; the returned
`KairosRun` (`clock/run.rs`) derives every member by the same rule. The
commitment is the run's *last* member, so later mints dominate the whole
reservation. The recorded skews are the maxima the iterated mints would
have folded (a unit-crossing run leads its one reading; the fold reports
it, the S211 gate review's finding).
`after` (`clock/mod.rs:123`):: *fused receive-and-send*. `advance(Some(remote))`, wrapped
into a `Kairos` that dominates both local state and the remote.
`observe` (`clock/mod.rs:198`):: the pure *receive* step (S20). `advance(Some(remote))`
with the result *discarded*: the state advance is the whole effect, so every later
mint exceeds `remote`. No `Kairos`, no kairotic, because no event is created. Being
a receive event it ticks per call, like the receive half of `after`; it is not an
idempotent merge.
`try_observe` (`clock/mod.rs:239`):: the bounded, trust-aware *receive* (S24). Reads the
time source once, rejects with `SkewExceeded` (clock unchanged) when `remote`'s
forward skew over that reading exceeds the caller's bound, else folds it through
`advance_from` against the same reading. The reject *mechanism* for untrusted
stamps; the bound value and the reject-vs-clamp *policy* stay the caller's.
So minting versus observing is purely whether the caller keeps the fold's return,
and bounded versus unconditional receive is whether the caller pre-checks the skew.
The dominance `observe` provides comes from the fold, not from a returned stamp,
which is what its property test pins.
== Generation walk-through
The time algebra lives whole in `fold::advance` (`clock/fold.rs:171`), a pure,
heap-free `const fn` over machine words: the uninitialized arm
(`clock/fold.rs:177`) adopts the larger of the reading and any remote physical,
seeding logical from a remote at equal time; the initialized arm
(`clock/fold.rs:208`) takes the max of last physical, the (skew-adjusted)
reading, and any remote physical, incrementing logical when physical did not
advance. Both arms roll a ceiling logical (`u16::MAX`) into the next physical
unit (the missing uninit-arm roll was the S86 fold bug, found by proof, see
xref:#proofs[the proof harnesses]), and both report forward/backward skew in
the returned `Advance` rather than recording it themselves; when stats are
folded is the shell's business.
`Clock::advance_from` (`clock/mod.rs:325`) is the thread-safe shell: infallible,
retrying until the compare-and-swap commits. Per attempt:
. The physical reading is taken once up front (by `advance`,
`clock/mod.rs:267`, or by `try_observe` before its skew check) and reused
across retries.
. Load the packed state with `Acquire`, decode with `ClockState::last`, run
`fold::advance`, and fold the returned skews into the stat maxima (per
attempt, before the CAS, exactly as the pre-S188 inline fold recorded them).
. Re-encode the new `(physical, logical)` as a `ClockState`, then
`compare_exchange` with `SeqCst` success / `Acquire` failure ordering.
. On success, record the attempt high-water in `peak_attempts` and return the
committed pair. `now` / `after` then rebuild a `Kairos` from it, the
immutable `station_id` field, and the caller's kairotic; `observe` /
`try_observe` discard it. On CAS failure another thread committed first;
consult `Backoff` (a bounded spin, no time read) and retry. There is no
abort path.
`LocalClock::advance_from` (`clock/local.rs:205`) is the single-threaded shell:
the same fold, one `Cell` store, skew maxima folded in place, no loop; there
is no rival writer to lose a race against. The type is `!Sync` (pinned by a
`compile_fail` doctest), so the compiler keeps it off shared paths.
The fold therefore never mints or stores `logical == u16::MAX` from either arm:
`u16::MAX` is the overflow sentinel that rolls into `physical`, which is what keeps
a mint strictly above a remote at the logical ceiling instead of tying it on
`(physical, logical)` and leaving domination to the kairotic/station tiebreak.
== Concurrency and memory ordering
State is one `AtomicU128` from `portable-atomic`, so the CAS works under `no_std`
and on platforms without native 128-bit atomics. The word encodes a `ClockState`
(an explicit init tag plus the last `(physical, logical)`), not a packed `Kairos`;
the returned stamp is rebuilt from those parts, the `station_id` field, and the
caller's kairotic. The successful CAS uses `SeqCst`; the load and failure path use
`Acquire`. `Clock<TS>` is `Send + Sync`
because every field is, and `TimeSource` carries `Send + Sync` as supertrait
bounds. A concrete source stays inline; `DynClock` opts into a boxed trait
object. Share a clock as `Arc<Clock<TS>>`; the concurrency test does
exactly this across eight threads.
Generation is *lock-free, not wait-free*: a committer is guaranteed each round,
but an individual call is bounded only in practice, by randomized backoff and a
finite contender count. See
xref:../../docs/target_arch/boundaries.adoc#_error_model[the error model] for why that makes
generation infallible rather than fallible.
The example suite (the threaded CAS exercise included, at reduced volume) also runs
under Miri's interpreter with weak-memory emulation (S86, `cargo +nightly miri test
-- --skip prop_`): no undefined behavior and no data race in the atomics protocol.
[#rank-mint]
== The rank-mint sub-contract (S211, ruling R-33)
The clock is also the supplier of the sequence CRDT's ordering material
(`Rhapsody` ranks its siblings by `Kairos`, PRD 0017), and three deep
structures assume its successor behavior: the snapshot codec's chain law
(PRD 0023), the identity plane's inline rank steps (arc 11 phase two), and
the coalescing economics both rest on. This section is the assumption made
contractual, measured by the deterministic `rank_steps` instrument
(`bench/src/bin/rank_steps.rs`, 2026-07-11) across time-source gaps from one
tick to seventeen minutes per keystroke:
* *What a rank consumer may assume of any mint sequence*: consecutive sends
with a non-decreasing source step the rank by the fold's send rule; the
physical component advances by at most the source's real advance. Nothing
else is promised: gaps are the source's business.
* *Wire coalescing is gap-independent to 48 bits.* The snapshot chain law
accepts any physical advance up to `MAX_RANK_STEP` (2^48 - 1; about 78
hours in nanoseconds), so a typed document's wire form stays one run per
chain at every human gap: the instrument measures one snapshot run and
6.009 bytes/char identically at 1 ns and at 17-minute gaps.
* *In-memory inline steps hold to 31 bits.* The identity plane's slot
payload carries physical advances below 2^31 (about 2.1 s in
nanoseconds); a keystroke gap beyond that costs one explicit column
entry, bounded by the count of such pauses, never by characters (the
instrument's 200 ms arm holds the 1/64 page floor exactly; only the
2.5 s-per-keystroke arm goes fully explicit, and its wire form is
unchanged even there).
* *The run mint is gap-immune by construction*: `now_run`'s members step
logical against one frozen reading, so a paste coalesces identically
under every source (the instrument's contrast arm).
The avenue-1 question ("does real time collapse the recorded coalescing
numbers?") is thereby answered NO for the wire and for every realistic
typing cadence in memory; the one degradation is priced and bounded above.
[#hazards]
== Hazards for a future editor
. *Do not "simplify" the field offsets.* They define the wire and ordering
contract.
. *`station_id` is an immutable `Clock` field* (`clock/mod.rs:28`), set once at
construction and packed into every minted stamp by `now` / `after`
(`clock/mod.rs:112` / `clock/mod.rs:125`). It is not in the mutable state word, and the shared
`advance_from` fold never touches it: identity is added only when a position is
wrapped into a `Kairos`, which is why `observe` / `try_observe` (no wrap) carry none.
. *Uninitialized is an explicit tag bit, not a sentinel* (`ClockState`,
`clock/state.rs:23`). The state word holds `Option<(physical, logical)>`; "not yet
minted" is the absent init bit (`clock/state.rs:31`), so no real reading, `u64::MAX`
included, can spoof it. Corollary: a stamp at the *physical* ceiling
(`physical == u64::MAX`) can exhaust its successors, so `after` of a remote at
the very ceiling cannot always be satisfied. That is an inherent limit of the
finite `(physical, logical)` space, not a bug; the `after` property test stays
one below the ceiling for it (`remote_physical`), and the S86 proofs pin the
sharp boundary: strict domination is *proven* for every remote with
`physical() < u64::MAX` (any logical, the ceiling `u16::MAX` included, since the
fold rolls it into physical), and only the physical ceiling row is exempt.
. *Backoff is spin-count, never wall-time* (S12, resolved PRD 0001 gap 1).
`Backoff::backoff` (`backoff/mod.rs:22`) takes no time source; the strategies spin a
bounded `core::hint::spin_loop()` count. Do not reintroduce the stamp
`TimeSource` into the seam: it conflated advancing logical time with measuring a
wait (a `TickCounter` read both ticks and times), and a non-advancing source
(`VirtualTimeSource`) would spin forever. Spin counts are relative contention
knobs, not durations; real wall-time backoff, if ever needed, is a `std` strategy
that reads its own clock, kept off this seam.
== Test map
Tests live under `src/kairos/tests/`: `clock/` for clock examples, `backoff.rs`
for retry-policy examples, `wire.rs` for stamp codec examples, and `properties/`
for the proptest suite. Inside `clock/`, `operations/` splits local minting/identity,
`after`, construction, ceiling, and run examples (`run.rs`, S211: the
frozen-reading mint succession, run-of-one identity, next-mint domination, the
logical-ceiling roll inside a run, one skew observation per reservation, shell
parity); `receive/` splits unbounded `observe`
examples from bounded `try_observe` examples; `stats.rs` holds skew/stat snapshots;
`concurrency.rs` holds the contended CAS example; `shell.rs` holds the
`LocalClock` shell examples (S188: parity of the four operations, the
all-or-nothing bounded receive, first-attempt stats); and `source.rs` holds the
`VirtualTimeSource` example.
Inside `properties/`, `stamp.rs` holds layout and wire properties, `clock.rs` holds clock
monotonicity and receive properties plus the S188 shell-agreement tape
(`prop_local_clock_agrees_with_atomic_clock_on_any_tape`: identical readings and
operations through both shells mint identical stamps, verdicts, and skew maxima,
with a `NowRun` op since S211) and the run law
(`prop_a_run_equals_frozen_individual_mints`: a run and that many individual
mints against one frozen reading commit identical successions and end states,
members chaining by the codec successor rule),
and `support.rs` holds the shared physical-reading generators.
The invariant-to-test mapping is tabulated in
xref:../../docs/prd/0001-kairos-hybrid-logical-clock.adoc#_invariants_and_their_tests[PRD 0001].
Real contention is exercised by `test_concurrency_with_backoff` (eight threads,
uniqueness, and a `peak_attempts` check), `test_backoff_tolerates_unbounded_attempts`
deterministically proves the backoffs never abort and the exponential spin count does
not overflow the shift at high attempt counts (and that an empty `ModelBasedBackoff`
table is a no-op), and `test_exponential_backoff_caps_spins` pins the doubling and the
`max_spins` cap.
Property tests (proptest, a dev-dependency as of S7) guard the layout and
monotonicity invariants: `prop_kairos_fields_round_trip` (pack/unpack is lossless
across full field widths), `prop_kairos_order_matches_field_priority` (the derived
`Ord` is exactly the `(physical, logical, kairotic, station_id)` lexicographic
order), `prop_now_is_monotonic_under_skew` (successive stamps strictly increase
under arbitrary, non-monotonic physical readings, driven by a caller-advanced
`VirtualTimeSource` that sets each reading before the mint that observes it),
and `prop_after_dominates_remote_and_stays_monotonic` (a stamp exceeds any folded-in
remote while the clock's own output stays strictly increasing). The receive rule
(S20) has the analogue `prop_observe_then_now_dominates_remote_and_stays_monotonic`
(after `observe(remote)` the next `now` exceeds `remote`), plus two example tests:
`test_observe_advances_clock_without_minting` (skew is recorded, the mint jumps to
the remote's physical and keeps local identity) and
`test_observe_of_dominated_remote_still_advances` (observe ticks even on an
already-dominated stamp, so it is a receive event, not an idempotent merge).
The bounded receive (S24) adds
`prop_try_observe_admits_within_bound_and_rejection_is_inert` (a remote is admitted
iff its forward skew is within the bound; an admitted one dominates as `observe`
does, a rejected one records no skew and leaves physical on local time) and four
example tests: `test_try_observe_accepts_within_bound`,
`test_try_observe_rejects_beyond_bound_and_leaves_clock_untouched`,
`test_try_observe_bound_is_inclusive` (skew equal to the bound is admitted), and
`test_try_observe_admits_remote_behind_local` (forward-only: a behind-local remote
passes even a zero bound).
The clock-driven properties draw physical readings from a dense low window unioned
with a window at the top of `u64` (`physical_reading` / `remote_physical`): with the
sentinel gone (xref:#hazards[hazard 3], S5), that region is ordinary input.
`test_physical_ceiling_reading_is_not_uninitialized` pins the exact case the old
sentinel mishandled, a `u64::MAX` reading on a fresh clock, and
`test_first_after_rolls_logical_ceiling` pins the S86 fold fix (a fresh clock's
first `after` of a remote at the logical ceiling rolls into physical rather than
tying, the case the domination proof found and sampling had missed).
The wire codec (S11) reuses that harness: `prop_bytes_round_trip` and
`prop_bytes_preserve_order` are the byte-level analogues of the two value-level
properties, `prop_from_bytes_never_panics` fuzzes decode over arbitrary slices, and
`test_to_bytes_layout` freezes the exact 17-byte frame. The full mapping is in
xref:../../docs/prd/0002-kairos-serialization.adoc#_invariants_and_their_tests[PRD 0002].
[#proofs]
== Proof harnesses (S86)
Above the sampled suites sit Kani proof harnesses, co-located under `cfg(kani)`
(`stamp/proofs.rs`, `clock/proofs.rs`) and compiled only by `cargo kani`, so no
normal build, test, clippy, or rustdoc pass ever sees them. Run with
`RUSTFLAGS="--cfg portable_atomic_no_asm" cargo kani --no-default-features`
(the cfg swaps `portable-atomic` onto its asm-free fallback, which Kani can
interpret; under the single-threaded harnesses any correct atomic has the same
sequential semantics, so the fold proofs are unaffected). Since S188 the fold
they prove is the *extracted* `fold::advance`: the harnesses exercise it
through the `Clock` shell (a single-threaded first-attempt CAS is exactly one
fold application), so the proofs cover both shells' shared semantics, and the
whole suite was re-verified over the extraction (20 harnesses, S188).
*Total* proofs (the full symbolic input space): `packing_roundtrips_every_field`
and `order_is_field_lexicographic` discharge the stamp layout and the core
invariant (the derived `Ord` *is* the field-lexicographic order, for every pair of
stamps); `wire_roundtrip_is_total` and `wire_bytes_sort_causally` discharge
PRD 0002 R6 and R2; `clock_state_roundtrips_and_init_tag_is_unforgeable`
discharges the packed-state invariant. *Fold* proofs (single-threaded, symbolic
readings and stamps, sub-physical-ceiling): `now_strictly_increases_under_any_skew`,
`now_strictly_increases_after_arbitrary_observe`,
`after_dominates_previous_on_fresh_clock` (the harness that found the S86
uninitialized-arm bug), `after_dominates_previous_on_warm_clock`,
`observe_then_now_dominates_remote`, `try_observe_rejection_leaves_clock_unchanged`
(all-or-nothing, bit-for-bit), and `try_observe_admission_dominates_remote`.
*Run* proofs (S211, ruling R-33):
`run_mint_equals_iterated_sends_over_a_frozen_reading` (the closed-form
`advance_run` / `rank_offset` against the iterated fold, member by member, no
saturation precondition needed because the saturating carry composes),
`run_members_strictly_ascend_below_the_ceiling`, and
`now_after_a_run_dominates_every_member` (the commitment is the run's last
member). *Bounded* proof: `wire_decode_is_total_and_byte_identical` (decode
totality and byte identity for every input up to the harness buffer). The full
inventory re-verified over the run extension: 24 harnesses, 0 failures
(2026-07-11).
The division of labor: proofs discharge the pure fold and the packed
representations; the threaded tests and Miri cover the CAS loop under real
interleavings; proptest keeps the same laws continuously sampled in the normal
gate. What earns a proof is ruled in `owner-comments.adoc` R-9.