Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^314 Every recording ends

An invariant of yap 0.1.0.

Id
yap^314
Kind
invariant
Reads as
proved
Version
0.1.0

All of yap 0.1.0's claims

What it says

A recording is either held down or hands free with its deadline at most ten minutes away; so once the key's release is heard and the clock reads ten minutes on, there is no recording. A release that comes while the microphone is starting waits for the start; if the start is never reported, the recording is given up ten minutes after that release (the original would wait forever: see docs/yap-parity.md). A recording held down has no limit, as in Swift Yap (`step_recInv`, `keyUp_tick_none`, `app_recording_ends`).

Evidence

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

Ledger

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