Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^1005 record reports started once its microphone is running, before any audio, or fails without it
An assumption of cairn 0.5.2.
- Id
cairn^1005- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
A record subscription's first event is started, sent once, only after the microphone's start has returned (the engine is running), and before every audio event of it, with the host's monotonic milliseconds (the clock of key events) read after the return; a microphone that can't start sends failed and never started. So an app that waits for started shows nothing for a microphone that fails, as Yap shows its overlay only once AudioCapture.start has returned.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check subs.record-start held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostRecordStarted- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:104atv0.5.2- Statement hash
-
Ledger
cairn^1005 is active in this version's claims.lock. An id never moves or changes meaning.