Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^915 every ms ticks while started and never after it is stopped
An assumption of cairn 0.5.2.
- Id
cairn^915- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
An every subscription ticks under its id only while it is started and not yet stopped, at most once per period, and the host's running subscriptions are exactly those the frames started and did not stop.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check subs.every held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostEvery- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:70atv0.5.2- Statement hash
-
Ledger
cairn^915 is active in this version's claims.lock. An id never moves or changes meaning.