Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^348 The host reports the microphone's start or its failure

An assumption of yap 0.1.0.

Id
yap^348
Kind
assume
Reads as
assumed
Version
0.1.0

All of yap 0.1.0's claims

What it says

After `startRecording`, the host starts the microphone and reports, once, that it is running (`started`, with its monotonic clock in milliseconds read after the start returned: the clock of key events) or that it failed (`micFailed`), before any audio of the clip. A start that never returns is never reported; the app then gives the recording up ten minutes after a release waits for it.

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.hostMicStart
Module
Yap
Source
lean/Yap.lean:453 at v0.1.0
Statement hash
-

Ledger

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