Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^908 The host's clock is monotonic milliseconds
An assumption of cairn 0.5.2.
- Id
cairn^908- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
Every batch the host sends Lean starts with exactly one clock event; its monotonic milliseconds never decrease from batch to batch and are not ahead of the system's monotonic clock, its wall time is the wall clock and its zone the current UTC offset.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check clock.monotonic held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostClock- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:44atv0.5.2- Statement hash
-
Ledger
cairn^908 is active in this version's claims.lock. An id never moves or changes meaning.