Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^331 The host delivers the ticks it is asked for

An assumption of yap 0.1.0.

Id
yap^331
Kind
assume
Reads as
assumed
Version
0.1.0

All of yap 0.1.0's claims

What it says

After `wakeAt t`, the host sends a `tick` with a time at or after `t`, while the app runs. Ticks may come late, early ones are ignored, and the clock may jump.

Evidence

assumedStated, not proved. The proofs rely on it.
fuzzedNot shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95).

Where it's defined

Declaration
Yap.hostTicks
Module
Yap
Source
lean/Yap.lean:432 at v0.1.0
Statement hash
-

Ledger

yap^331 is active in this version's claims.lock. An id never moves or changes meaning.