Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^350 Keys wait for the microphone

An invariant of yap 0.1.0.

Id
yap^350
Kind
invariant
Reads as
proved
Version
0.1.0

All of yap 0.1.0's claims

What it says

While a recording's microphone is starting, a key going down or up, or another key, leaves the recording as it is: the event waits, and is handled once the host reports the start (or its failure), as the original's main thread handles key events only once `engine.start()` returns (`app_keys_wait`). Only the key's listener failing ends it.

Evidence

provedinitYap.keysWaitForMic.init
provedstepYap.keysWaitForMic.step
provedreceiveYap.keysWaitForMic.receive
provedreachableYap.keysWaitForMic.reachable
provedreachableAllYap.keysWaitForMic.reachableAll
fuzzedNot shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95).
testedNot shown yet: the running app matched the model at every step that exercised it (docs/conformance.md). A CI step will publish it (#95).

Where it's defined

Declaration
Yap.keysWaitForMic
Module
Yap
Source
lean/Yap.lean:276 at v0.1.0
Machine
Yap.machine
Statement
Yap.keysWaitForMic.holds
Statement hash
3f6b71a8c1df4170

Ledger

yap^350 is active in this version's claims.lock, statement 3f6b71a8c1df4170. An id never moves or changes meaning.