Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^349 The overlay waits for the microphone

An invariant of yap 0.1.0.

Id
yap^349
Kind
invariant
Reads as
proved
Version
0.1.0

All of yap 0.1.0's claims

What it says

As in the original, whose `begin` shows the overlay only once `AudioCapture.start` has returned: the overlay never shows a recording whose microphone hasn't started, so a microphone that fails to start never shows it. Only the host's report that the clip's microphone started (`micStarted`) begins the overlay (`step_begin`); every recording's clip, and the overlay's, is one numbered so far, so a new recording is never the overlay's clip (`OvInv`, `receive_ovInv`, `menuStep_ovInv`).

Evidence

provedinitYap.overlayAfterMic.init
provedstepYap.overlayAfterMic.step
provedreceiveYap.overlayAfterMic.receive
provedreachableYap.overlayAfterMic.reachable
provedreachableAllYap.overlayAfterMic.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.overlayAfterMic
Module
Yap
Source
lean/Yap.lean:268 at v0.1.0
Machine
Yap.machine
Statement
Yap.overlayAfterMic.holds
Statement hash
f0ec228f91f245f9

Ledger

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