Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^1032 Under holdWorld the host sends no clock, wake or reply of its own
An assumption of cairn 0.5.2.
- Id
cairn^1032- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
Once Engine.holdClock and World.holdRequests have returned, every batch Lean hears is exactly the events the caller sent, in order (the driver's clock and reply events among them): the host adds no clock, sends no wake whatever the frame's wake deadline, and runs and answers no request handed over afterwards; a request from before the hold is answered at most once. Lean never hears an empty batch.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check world.hold held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostHoldWorld- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:305atv0.5.2- Statement hash
-
Ledger
cairn^1032 is active in this version's claims.lock. An id never moves or changes meaning.