Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^313 One recording at a time

An invariant of yap 0.1.0.

Id
yap^313
Kind
invariant
Reads as
proved
Version
0.1.0

All of yap 0.1.0's claims

What it says

The app records exactly while the machine has a recording: one `record` subscription, for its clip. Whatever the host reports, a recording the machine didn't have is the next clip, started when there was none; the menu only ever stops one (`record_sub_iff`, `app_new_recording`, `step_new_recording`).

Evidence

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

Ledger

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